Issues Setting up VSCode

Stream: new members

[Devon Richards]

I just started trying to get lean setup in a Nix environment and installed lean(3.23.0), mathlibtools, elan, and vscode(1.52.1) with the lean extension(0.16.20). I created a new project and added

import topology.basic

#check topological_space

To a source file. Loading the file in VS Code then has the lean server using over 9 GB of RAM, is this expected behavior?

[Kevin Buzzard]

Yes

[Kevin Buzzard]

Actually, sorry, the answer is "depends on how you set up the new project"

[Kevin Buzzard]

Did you make the new project with leanproject or leanpkg?

[Devon Richards]

I set it up with leanproject new.

[Kevin Buzzard]

I strongly suspect your PC is compiling mathlib right now, which can take a long time. If you make a new project with leanproject new my-project and then open the my-project directory using VS Code then you shouldn't have this problem.

[Kevin Buzzard]

The differnce between leanpkg and leanproject is that leanproject downloads fully compiled mathlib binaries for you (like elan downloaded fully compiled lean binaries for you)

[Kevin Buzzard]

Devon Richards said:

I set it up with leanproject new.

In which case, can you send a screenshot of VS Code with the file open?

[Devon Richards]

I would guess you are right since it was using nearly 100% CPU across all cores for a while. LeanFile.png

[Devon Richards]

The server has stopped using CPU, but is still holding onto the RAM, though I'd guess that might be expected behavior if it compiled from scratch.

[Kevin Buzzard]

On the command line what happens if you try lean --make src/chapter0.lean?

[Devon Richards]

it looks like it starts parsing through the mathlib source in the _target directory. This was setup with a nix shell if that changes anything.

[Kevin Buzzard]

I guess also I'd be interested in (a) the contents of leanpkg.toml (b) the commit which _target/deps/mathlib is on (this will be a git repo within your repo) (c) the output of lean --version when run in the project

[Bryan Gin-ge Chen]

(deleted)

[Kevin Buzzard]

It's the "I installed lean 3.23.0" line I'm worried about in the original post

[Devon Richards]

Lean (version 3.23.0, Release) is the version.

[package]
name = "DescriptiveSetTheory"
version = "0.1"
lean_version = "leanprover-community/lean:3.24.0"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "3669cb35c578441812ad30fd967d21a94b6f387e"}

is the toml
3669cb35c578441812ad30fd967d21a94b6f387e is the commit

[Kevin Buzzard]

So there's your problem

[Kevin Buzzard]

You shouldn't be installing any version of lean, I don't really know what you mean by "I installed Lean 3.23.0"

[Kevin Buzzard]

the idea is that elan will take a look at that toml file, observe you need lean 3.24, and get elan to download it automatically for you.

[Devon Richards]

ah, I was just using the version in nixpkgs for the shell. I'll try setting up with elan instead.

[Kevin Buzzard]

I don't know anything about nix or elan but what you need to do is to somehow get it so that it's saying you're using 3.24.0 when you run lean in the directory

[Kevin Buzzard]

The lean on my system is /home/buzzard/.elan/bin/lean which cunningly chooses which actual version of lean to run by searching for the nearest toml file and reading it and using what's in there

[Kevin Buzzard]

Note that now you started compiling Lean by hand with lean --make src/chapter0.lean, your installation is currently corrupt. You should be able to fix this by running leanproject get-mathlib-cache within your project

[Kevin Buzzard]

Right now you have about ten lean 3.23 compiled (olean) files and hundreds of precompiled lean 3.24 olean files

[Bryan Gin-ge Chen]

Would it be possible / useful to have leanproject spit out a warning or error if it sees that running lean gives a different version than what's in the leanpkg.toml (or some other way of detecting issues with lean / elan)?

[Devon Richards]

It did spit out warnings, but it created that leanpkg.toml.

[Kevin Buzzard]

the toml is correct. The problem is that your project has a dependency on mathlib which right now uses lean 3.24.

[Kevin Buzzard]

as of some time earlier today IIRC