How to use VSCode Extension?

Stream: new members

[Daniel Donnelly]

I'm new to Lean and to VSCode. I installed it through View > Extensions in vscode. Not sure even what extension to put for a Lean file. Can anyone provide me with a few "Hello word" steps for VSCode environment?

[Patrick Massot]

Did you read https://github.com/leanprover-community/mathlib/blob/master/README.md?

[Daniel Donnelly]

Thx! :)

[Patrick Massot]

The suggestion of cloning the perfectoid spaces repository in the docs is kind of joke, you should rather have a look at https://github.com/PatrickMassot/lean-tutorials as a first project to clone

[Daniel Donnelly]

Oh yea, that Fields Medalist's discovery

[Daniel Donnelly]

I will read over those now

[Daniel Donnelly]

pasted image

[Daniel Donnelly]

Does that mean it's busy, because it's not displaying anything : /

[Mario Carneiro]

the orange bar means it's busy, but the usual cause is that mathlib is not compiled. Someone else here can tell you how to download the precompiled mathlib files

[Daniel Donnelly]

Cool thx

[Chris Hughes]

https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/index.md

[Chris Hughes]

Under caching compilation.

[Chris Hughes]

And checkout the lean-3.4.2 not master

[Patrick Massot]

Chris, you shouldn't point beginners to this page. As its title indicate, it's meant for people who want to contribute to mathlib. The correct page, with link from the installation page is https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md

[Patrick Massot]

And indeed he shouldn't have to wait for orange bars to disappear if he followed the instruction (and maybe he also need to use a decent OS...)

[Daniel Donnelly]

pasted image
How does one enter in stuff like double-bolded R?

[Patrick Massot]

Did you clone the repository?

[Daniel Donnelly]

Not for this install. I installed using elan

[Patrick Massot]

Because if you open the file in VS Code and put the mouse cursor over a funny symbol then you'll get a tootip popup explaining how to type it (and what it means if it currently means something to Lean)

[Patrick Massot]

It will be much easier for everybody if you follow instructions on https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md and then https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md#working-on-an-existing-package (replacing the perfectoid project with the tutorial one)

[Daniel Donnelly]

So I shouldn't have installed elan from VScode automatically?

[Patrick Massot]

Hopefully this is fine

[Daniel Donnelly]

I already have Python installed, like 5 versions of it, so that shouldn't be the issue

[Daniel Donnelly]

"Run git config --global core.autocrlf input in Git Bash
Alternatively, you can set it to false. If it is set to true, you might run into issues when running update-mathlib or cache-olean --fetch."

[Daniel Donnelly]

Maybe that one

[Patrick Massot]

But you should still install supporting scripts as described in https://github.com/leanprover-community/mathlib/blob/master/docs/install/windows.md#get-scripts

[Daniel Donnelly]

because update-mathlib was not found

[Daniel Donnelly]

Yes, did that

[Daniel Donnelly]

So should I reconfigure get with that bool flag set oppositely?

[Daniel Donnelly]

*git

[Patrick Massot]

This git flag is irrelevant here

[Patrick Massot]

It's role is to make sure you can contribute to projects using standard line endings

[Patrick Massot]

You need to be able to fire up git bash and have access to the update-mathlib command

[Daniel Donnelly]

Yes, I'm getting update-mathlib not found even though that "curl..." line seemed all successful

[Patrick Massot]

maybe typing source $HOME/.profile will help.

[Patrick Massot]

I have no access to a Windows machine

[Patrick Massot]

And unfortunately most people who fight to install Lean then forget about it and don't go back to fix documentation

[Daniel Donnelly]

$ source $HOME/.profile

FruitfulApproach@DESKTOP-T49RGUJ MINGW64 /c/mylean/my_project (lean-3.4.2)
$ update-matholib
bash: update-matholib: command not found

[Patrick Massot]

there is a typo

[Patrick Massot]

it's not matholib but mathlib

[Daniel Donnelly]

$ update-mathlib
/usr/bin/env: ‘python3’: No such file or directory

[Patrick Massot]

Ok, it found update-mathlib but not python

[Daniel Donnelly]

Is python3 supposed to be the exe name or the folder?

[Patrick Massot]

I have no idea how python works on Windows

[Patrick Massot]

Can you type python3 in git bash ?

[Daniel Donnelly]

Nope

[Daniel Donnelly]

Here's what I have installed:

[Daniel Donnelly]

06/20/2017 08:32 AM <DIR> Python
01/04/2018 11:03 AM <DIR> Python34
12/13/2017 06:02 PM <DIR> Python35-32
04/15/2019 10:14 PM <DIR> Python36-32
05/10/2019 11:05 PM <DIR> Python37
07/31/2019 12:52 AM <DIR> Python37-32

[Daniel Donnelly]

On C:\ root

[Daniel Donnelly]

'python' works though

[Patrick Massot]

And does it run python3?

[Daniel Donnelly]

$ python
Python 3.7.3 (v3.7.3:ef4ec6ed12, Mar 25 2019, 21:26:53) [MSC v.1916 32 bit (Intel)] on win32

[Patrick Massot]

Good

[Patrick Massot]

Can you try python $HOME/.mathlib/bin/update-mathlib?

[Daniel Donnelly]

$ python $HOME/.mathlib/bin/update-mathlib
Info: No github section found in 'git config', we will use GitHub with no authentication
Querying GitHub...
Downloading nightly...

[Daniel Donnelly]

Thanks for your help!

[Patrick Massot]

Can you check that _target/deps/mathlib/src/algebra now contains .olean files?

[Daniel Donnelly]

Where's that located?

[Patrick Massot]

Inside the top level folder of your project

[Patrick Massot]

c/mylean/my_project probably

[Patrick Massot]

What drives me crazy is we do have a couple of Windows users that are expert Lean users, and that Windows installation page still doesn't work

[Daniel Donnelly]

Yeah it has those .olean files. Those are the compiled ones?

[Patrick Massot]

Yes

[Patrick Massot]

Note that source $HOME/.profile shouldn't be needed next time you log in. The only remaining issue is update-mathlib not finding python

[Daniel Donnelly]

I don't know why they'd use "python3", when python.exe has no 3 in it

[Patrick Massot]

You should now be able to clone the tutorial repo and then follow instructions in https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md#working-on-an-existing-package to get a first_proofs.lean that becomes (almost) immediately responsive in VScode

[Daniel Donnelly]

Cool, I will do this tomorrow morning. :D

[Mario Carneiro]

I recall the python being changed to python3 based on some other installation kerfuffle

[Patrick Massot]

Mario, you use Windows, right? Do you use update-mathlib at all?

[Mario Carneiro]

no

[Mario Carneiro]

I realize your comment above about expert lean users not writing documentation is probably directed at me

[Patrick Massot]

You're not the only one

[Mario Carneiro]

but I'm really bad at this stuff

[Mario Carneiro]

I'm just happy that it works and try not to mess with the setup

[Daniel Donnelly]

Kerfuffle, haha

[Patrick Massot]

What is crazy is not what any individual is doing, we all have good reasons. It's the fact the community cannot do it

[Mario Carneiro]

I don't even know how installation works these days. The information I got from my own experience is very out of date

[Patrick Massot]

I know this problem. When I wrote installation instructions for Linux I used a virtual machine in order to get a really fresh setup. And it took me several hours, with at least 20 VM resets, before getting the instructions and scripts right

[Patrick Massot]

And I suspect the situation is much worse on Windows, because every piece of the puzzle has to fight for survival in a hostile environment.

[Mario Carneiro]

The scripting situation is horrible on every OS

[Mario Carneiro]

there is a bootstrapping problem because no technology is sufficiently universal to be found on all target machines

[Mario Carneiro]

so far, I think the most reliable host has been vscode; it exists on all supported platforms and executes the same stuff

[Daniel Donnelly]

I could write an automated installer, but not sure how to do all that stuff in VScode (from a python script). I could however say to the user "click on the terminal in VScode so we know where it's at;" and later "Now don't touch the mouse or keyboard for a minute."

[Daniel Donnelly]

I have experience doing automated stuff with a PyQt5 app

[Patrick Massot]

Scott tried to get VScode to install stuff, and it's very unreliable

[Patrick Massot]

One can install VScode extension from command line, this is what the Debian installation script does

[Mario Carneiro]

but as soon as it starts executing command line instructions things go bonkers because you don't know where anything is, what the paths look like, and so on

[Mario Carneiro]

debian installation is great... if only that existed everywhere

[Daniel Donnelly]

Just try 100 different regexes of different paths :)

[Daniel Donnelly]

It doesn't have to work 100% of the time. If it makes the life of 80% of the new users better, then it's worth it

[Mario Carneiro]

it's the 20% that poke their heads in here

[Mario Carneiro]

so we get some skewed data

[Daniel Donnelly]

Good night, all!

[Daniel Donnelly]

:hug: