installation with vscode

Stream: new members

[Lysxia]

I've tried to install lean with vscode following those instructions https://leanprover-community.github.io/install/windows.html
I've managed to have gotten elan and mathlib on git bash, then I went and got the vscode extension, which didn't find lean, and installed its own copy of lean somewhere... so how do I either (1) get rid of that and point it to my first lean installation (2) install mathlib so that second installation can find it?

[Lysxia]

Or maybe the problem is not getting mathlib because it seems to know about those modules, but lean seems stuck, the InfoView window always says "loading"

[Kevin Buzzard]

Did you use VS Code's "open folder" functionality to open a correctly-formatted Lean project? If you're not sure, can you send a screenshot of your VS Code with the file explorer open and the infoview saying "loading"?

[Lysxia]

I did. This is what I'm seeing Untitled.png The whole file is marked in orange and I cannot get any type information, it just says "loading..."

[Arthur Paulino]

What happens if you comment out the import ... line?
(I suspect your computer is building mathlib)

[Lysxia]

Ah with the import out it does respond

[Arthur Paulino]

Try $ leanproject get-mathlib-cache in the root directory of the project

[Lysxia]

Looking for testlean oleans for 0f9c1538d
  locally...
  remotely...
('Connection aborted.', ConnectionResetError(10054, 'An existing connection was forcibly closed by
the remote host', None, 10054, None))

[Lysxia]

Is there a progress indicator? Is it supposed to build in the background? I remember mathlib was at least downloaded at the beginning.

[Arthur Paulino]

You can let it build mathlib in the background but it's a rather expensive operation. It takes time, CPU and quite a lot of memory. So we just use leanproject to get cached olean files from Azure.
I had never seen the host closing the connection like that though

[Arthur Paulino]

Lysxia said:

I remember mathlib was at least downloaded at the beginning.

That was probably "just" the source code of mathlib

[Lysxia]

aha, I don't know what changed but after messing around leanproject get-mathlib-cache eventually succeeded.