Zulip Chat Archive

Stream: new members

Topic: Issues Setting up VSCode


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 19:41):

Yes

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 19:41):

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

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 19:42):

Did you make the new project with leanproject or leanpkg?

view this post on Zulip Devon Richards (Jan 05 2021 at 19:43):

I set it up with leanproject new.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 19:49):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 19:51):

(deleted)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 19:52):

So there's your problem

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)?

view this post on Zulip Devon Richards (Jan 05 2021 at 19:59):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 20:00):

as of some time earlier today IIRC


Last updated: May 13 2021 at 20:13 UTC