tutorial errors

Stream: new members

[Adrian]

Hi. I'm trying to use the tutorial but when I open it in VS Code I get a bunch of errors from the Lean extension. Anyone know what could be causing this? It says it ran out of memory but the memory limit in the VS Code extension is set to the default 4096 MB.

Screen-Shot-2021-08-23-at-12.22.03-PM.png

[Kevin Buzzard]

Did you install the tutorial using leanproject? If not then that's your problem.

[Adrian]

Yes I used leanproject get tutorials to install it.

[Bryan Gin-ge Chen]

Do you still have access to the output of leanproject get tutorials or do you mind trying to run it again in another folder? Are there any suspicious looking messages?

[Adrian]

This is the output:

» leanproject get tutorials
Cloning from git@github.com:leanprover-community/tutorials.git
The authenticity of host 'github.com (192.30.255.113)' can't be established.
RSA key fingerprint is SHA256:nThbg6kXUpJWGl7E1IGOCspRomTxdCARLviKw6E5SY8.
This key is not known by any other names
Are you sure you want to continue connecting (yes/no/[fingerprint])? no
Error cloning via SSH, trying HTTPS...
Cloning from https://github.com/leanprover-community/tutorials.git

WARNING: Lean version mismatch: installed version is leanprover-community/lean:3.31.0, but package requires leanprover-community/lean:3.32.1

configuring tuto 0.1
WARNING: leanpkg configurations not specifying `path = "src"` are deprecated.
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 179830, done.
remote: Counting objects: 100% (1453/1453), done.
remote: Compressing objects: 100% (875/875), done.
remote: Total 179830 (delta 995), reused 760 (delta 577), pack-reused 178377
Receiving objects: 100% (179830/179830), 80.95 MiB | 6.10 MiB/s, done.
Resolving deltas: 100% (142878/142878), done.
> git checkout --detach 9945a1624fed215f7d254f060d13a74fec6a102b    # in directory _target/deps/mathlib
HEAD is now at 9945a1624 refactor(analysis/normed_space/{add_torsor, mazur_ulam}): adjust Mazur-Ulam file to use affine isometries (#8661)
Looking for local mathlib oleans
Found local mathlib oleans

Would the WARNING: Lean version mismatch: installed version is leanprover-community/lean:3.31.0, but package requires leanprover-community/lean:3.32.1 cause a problem?

[Bryan Gin-ge Chen]

Yes, that is a problem. You should be using elan though which should take care of the version for you though.

[Bryan Gin-ge Chen]

Just checking, but how did you install lean itself? Did you use the script on this page? https://leanprover-community.github.io/install/macos.html

[Adrian]

I installed lean using nix by running nix-env -iA nixpkgs.lean nixpkgs.mathlibtools. Now I undid that and I am trying to use elan to install lean, but it is not recognizing that I have GMP installed. When I run lean I get dyld: Library not loaded: /usr/local/opt/gmp/lib/libgmp.10.dylib.

[Adrian]

I was hoping not to have to install homebrew but maybe I will have to.

[Bryan Gin-ge Chen]

By the way, if you're using an M1 Mac, there are some posts linked to in this thread which might help. (We really should update our instructions for M1 Macs...)