## Stream: new members

### Topic: Issues Setting up VSCode

#### Devon Richards (Jan 05 2021 at 19:41):

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?

Yes

#### Kevin Buzzard (Jan 05 2021 at 19:41):

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

#### Kevin Buzzard (Jan 05 2021 at 19:42):

Did you make the new project with leanproject or leanpkg?

#### Devon Richards (Jan 05 2021 at 19:43):

I set it up with leanproject new.

#### Kevin Buzzard (Jan 05 2021 at 19:43):

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 (Jan 05 2021 at 19:43):

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 (Jan 05 2021 at 19:44):

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 (Jan 05 2021 at 19:46):

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

#### Devon Richards (Jan 05 2021 at 19:48):

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 (Jan 05 2021 at 19:49):

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

#### Devon Richards (Jan 05 2021 at 19:50):

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 (Jan 05 2021 at 19:50):

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

(deleted)

#### Kevin Buzzard (Jan 05 2021 at 19:52):

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

#### Devon Richards (Jan 05 2021 at 19:52):

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 (Jan 05 2021 at 19:52):

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 (Jan 05 2021 at 19:53):

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 (Jan 05 2021 at 19:54):

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

#### Kevin Buzzard (Jan 05 2021 at 19:54):

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 (Jan 05 2021 at 19:55):

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 (Jan 05 2021 at 19:56):

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 (Jan 05 2021 at 19:56):

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 (Jan 05 2021 at 19:59):

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 (Jan 05 2021 at 19:59):

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

#### Kevin Buzzard (Jan 05 2021 at 20:00):

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

#### Kevin Buzzard (Jan 05 2021 at 20:00):

as of some time earlier today IIRC

Last updated: May 13 2021 at 20:13 UTC