Zulip Chat Archive

Hi everyone, I'm having trouble installing Lean on Ubuntu 22.04.02. I tried installing Lean by calling it through vscode, or installing it through elan directly. Either way, I can't seem to be able to make Lean code compile in VsCode; Lean keeps crashing. Is there some Nix hidden in Elan? I have an issue with Nix on my computer. Could it be related? On another subject, I was willing to try Lean with emacs, but to do that, I am told I should edit the init.el file. Where might I find it? I appreciate any help on the subject!

Patrick Massot (Jun 22 2023 at 19:00):

No, there is no Nix hidden in elan.

Patrick Massot (Jun 22 2023 at 19:01):

In order to help you, we need more information about "I can't seem to be able to make Lean code compile in VsCode; Lean keeps crashing." Could you describe more precisely what you try to do?

Marie Kerjean (Jun 22 2023 at 19:04):

Creating a test.lean file in which I type check id. or eval 1+1.results in Lean crashing and error message :

Lean (version 4.0.0-nightly-2023-06-22, commit 32e93f1dc1b2, Release)
elan 1.4.6 (f3b9c9ab0 2023-06-10)
elan 1.4.6 (f3b9c9ab0 2023-06-10)
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2023-06-22
info: downloading component 'lean'
elan 1.4.6 (f3b9c9ab0 2023-06-10)
info: syncing channel updates for 'nightly'
Watchdog error: cannot find open document 'file:///home/marie/lean/test.lean'
[Error - 8:34:05 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.
info: latest update on nightly, lean version nightly-2023-06-22
info: downloading component 'lean'
info: installing component 'lean'
Lean (version 4.0.0-nightly-2023-06-22, commit 32e93f1dc1b2, Release)
info: installing component 'lean'
Lean (version 4.0.0-nightly-2023-06-22, commit 32e93f1dc1b2, Release)
Watchdog error: cannot find open document 'file:///home/marie/lean/test.lean'
[Error - 8:47:18 PM] The Lean 4 server crashed 1 times in the last 3 minutes. The server will not be restarted. See the output for more information.

Kevin Buzzard (Jun 22 2023 at 19:06):

Hi Marie! I'm not sure you can just work on a random test.lean file -- I think that to get Lean working the file needs to be in a correctly-formatted Lean project. Try making a new Lean project with lake new my_project? The project will have a lakefile in it which might be the information that Lean can't find right now.

Patrick Massot (Jun 22 2023 at 19:08):

The crash is still very weird.

Patrick Massot (Jun 22 2023 at 19:10):

And I thought that if you don't want to use mathlib then you can play outside a project. At least the doc at https://leanprover.github.io/lean4/doc/quickstart.html says so.

Patrick Massot (Jun 22 2023 at 19:10):

Marie, I guess you'll want to use mathlib anyway so you should follow the instructions from https://leanprover-community.github.io/, specifically https://leanprover-community.github.io/install/debian.html

Patrick Massot (Jun 22 2023 at 19:11):

including the last step in those instructions which is to read https://leanprover-community.github.io/install/project.html after installing.

Marie Kerjean (Jun 22 2023 at 19:13):

Another example, when I do lake build I get error: no such file or directory (error code: 2) file: ./lakefile.lean

Patrick Massot (Jun 22 2023 at 19:14):

That one is expected, this is the exact analogue of running make in a directory without a Makefile.

Patrick Massot (Jun 22 2023 at 19:14):

lake means "Lean make`.

Marie Kerjean (Jun 22 2023 at 19:16):

Again another example, typing wget -q https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh && bash install_debian.sh ; rm -f install_debian.sh && source ~/.profile as indicated here gets me an extremely long and weird error message involving Nix and opam (hence my first question).

Sebastian Ullrich (Jun 22 2023 at 19:18):

Sometimes VS Code and Lean get confused about which files they considered opened. It's not clear to me yet when that happens. Does restarting VS Code help anything?

Marie Kerjean (Jun 22 2023 at 19:20):

Sebastian Ullrich said:

Sometimes VS Code and Lean get confused about which files they considered opened. It's not clear to me yet when that happens. Does restarting VS Code help anything?

Sadly it doesn't. In fact, until now I was compiling Lean on a MacOS, and writing here is my last try before just reinstalling my Ubuntu computer to be able to compile Lean on it.

Patrick Massot (Jun 22 2023 at 19:20):

I would be ready to believe Sebastian conspired to make us all use Nix without knowing it, but adding opam to the conspiracy makes it really really implausible.

Patrick Massot (Jun 22 2023 at 19:21):

I guess this question by Sebastian was directed at me who has an otherwise working Lean setup. The answer is no, it doesn't help.

Patrick Massot (Jun 22 2023 at 19:22):

Marie, could you paste your long and weird error message?

Marie Kerjean (Jun 22 2023 at 19:22):

Patrick Massot said:

Marie, could you paste your long and weird error message?

Sure :

sudo apt install -y git curl
[sudo] password for marie:
Reading package lists... Done
Building dependency tree... Done
Reading state information... Done
curl is already the newest version (7.81.0-1ubuntu1.10).
git is already the newest version (1:2.34.1-1ubuntu1.9).
The following packages were automatically installed and are no longer required:
  libboost-context1.74.0 libcpuid15 libdbd-sqlite3-perl libdbi-perl
  libwww-curl-perl
Use 'sudo apt autoremove' to remove them.
0 upgraded, 0 newly installed, 0 to remove and 36 not upgraded.
+ wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
--2023-06-22 21:13:14--  https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
Resolving raw.githubusercontent.com (raw.githubusercontent.com)... 2606:50c0:8002::154, 2606:50c0:8003::154, 2606:50c0:8000::154, ...
Connecting to raw.githubusercontent.com (raw.githubusercontent.com)|2606:50c0:8002::154|:443... connected.
HTTP request sent, awaiting response... 200 OK
Length: 9875 (9,6K) [text/plain]
Saving to: ‘elan-init.sh’

elan-init.sh        100%[===================>]   9,64K  --.-KB/s    in 0,01s

2023-06-22 21:13:14 (973 KB/s) - ‘elan-init.sh’ saved [9875/9875]

+ bash elan-init.sh -y
info: downloading installer
info: updating existing elan installation

+ rm elan-init.sh
++ which code
+ vsc=/snap/bin/code
+ '[' -z /snap/bin/code ']'
+ /snap/bin/code --install-extension leanprover.lean4
Installing extensions...
Extension 'leanprover.lean4' v0.0.103 is already installed. Use '--force' option to update to latest version or provide '@<version>' to install a specific version, for example: 'leanprover.lean4@1.2.3'.
+ . /home/marie/.profile
++ '[' -n '5.1.16(1)-release' ']'
++ '[' -f /home/marie/.bashrc ']'
++ . /home/marie/.bashrc
+++ case $- in
+++ return
++ '[' -d /home/marie/bin ']'
++ '[' -d /home/marie/.local/bin ']'
++ PATH=/home/marie/.local/bin:/home/marie/.nix-profile/bin:/nix/var/nix/profiles/default/bin:/home/marie/.elan/bin:/home/marie/.cargo/bin:/home/marie/.opam/default/bin:/home/marie/.local/bin:/home/marie/.nix-profile/bin:/nix/var/nix/profiles/default/bin:/usr/local/texlive/2023/bin/x86_64-linux:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin
++ test -r /home/marie/.opam/opam-init/init.sh
++ . /home/marie/.opam/opam-init/init.sh
++ . /home/marie/.cargo/env
+++ case ":${PATH}:" in
++ export PATH=/home/marie/.elan/bin:/home/marie/.opam/default/bin:/home/marie/.local/bin:/home/marie/.nix-profile/bin:/nix/var/nix/profiles/default/bin:/home/marie/.elan/bin:/home/marie/.cargo/bin:/home/marie/.opam/default/bin:/home/marie/.local/bin:/home/marie/.nix-profile/bin:/nix/var/nix/profiles/default/bin:/usr/local/texlive/2023/bin/x86_64-linux:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin
++ PATH=/home/marie/.elan/bin:/home/marie/.opam/default/bin:/home/marie/.local/bin:/home/marie/.nix-profile/bin:/nix/var/nix/profiles/default/bin:/home/marie/.elan/bin:/home/marie/.cargo/bin:/home/marie/.opam/default/bin:/home/marie/.local/bin:/home/marie/.nix-profile/bin:/nix/var/nix/profiles/default/bin:/usr/local/texlive/2023/bin/x86_64-linux:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin
bash: /home/marie/.nix-profile/etc/profile.d/nix.sh: No such file or directory

Patrick Massot (Jun 22 2023 at 19:23):

Maybe running only

wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
bash elan-init.sh -y

instead of the whole install script, to narrow it down a tiny bit.

Marie Kerjean (Jun 22 2023 at 19:23):

Patrick Massot said:

Maybe running only
wget https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh
bash elan-init.sh -y
instead of the whole install script, to narrow it down a tiny bit.

This restricted instruction works as I already have elan

Patrick Massot (Jun 22 2023 at 19:24):

Do you already see the weird things with . /home/marie/.profile?

Patrick Massot (Jun 22 2023 at 19:25):

I think everything comes from the content of your .profile that has nothing to do with Lean.

Marie Kerjean (Jun 22 2023 at 19:25):

Don't waste too much on this issue, I'll just continue on MacOS, this must be a very specific issue due to my computer which I'll reinstall at some point

Patrick Massot (Jun 22 2023 at 19:25):

As you can see, the last step of https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/install_debian.sh is to source your .profile to make sure to update your PATH

Marie Kerjean (Jun 22 2023 at 19:25):

Patrick Massot said:

I think everything comes from the content of your .profile that has nothing to do with Lean.

Yes, this is where I have a Nix issue.

Patrick Massot (Jun 22 2023 at 19:26):

This Nix issue should have no impact on your use of Lean. I think you installed Lean just fine.

Patrick Massot (Jun 22 2023 at 19:27):

Did you try creating a Lean project as described in https://leanprover-community.github.io/install/project.html ?

Marie Kerjean (Jun 22 2023 at 19:27):

Patrick Massot said:

This Nix issue should have no impact on your use of Lean. I think you installed Lean just fine.

Ok, I'll keep trying (but it worked fine with mathcomp :cry: )

Patrick Massot (Jun 22 2023 at 19:27):

I mean creating or using an existing one.

Patrick Massot (Jun 22 2023 at 19:28):

For instance running:

git clone https://github.com/leanprover-community/mathematics_in_lean.git
cd mathematics_in_lean
lake exe cache get
code .

Patrick Massot (Jun 22 2023 at 19:30):

and then, using the VSCode file explorer on the left of your screen to open a Lean file in the MIL folder (and I really mean "using the file explorer", not going to the File menu and clicking "Open file").

Marie Kerjean (Jun 22 2023 at 19:31):

Patrick Massot said:

Did you try creating a Lean project as described in https://leanprover-community.github.io/install/project.html ?

No, I was following these instructions https://github.com/leanprover-community/mathlib4 and these https://leanprover.github.io/lean4/doc/quickstart.html. I'll try your last instructions.

Marie Kerjean (Jun 22 2023 at 19:38):

Patrick Massot said:

For instance running:

git clone https://github.com/leanprover-community/mathematics_in_lean.git

cd mathematics_in_lean

lake exe cache get

code .

Now this seems to be effectively installing mathlib4 (and thus taking a bit of time). I'll keep you updated, thank you very much!

Kevin Buzzard (Jun 22 2023 at 19:41):

Hopefully it's downloading compiled binaries (around 3000 files?) from the internet.

Marie Kerjean (Jun 22 2023 at 20:27):

Patrick Massot said:

Did you try creating a Lean project as described in https://leanprover-community.github.io/install/project.html ?

It works, thanks! I should have tried to start a project directly, thanks again for your time!

Patrick Massot (Jun 22 2023 at 20:42):

No problem! I'm sorry the situation is so confusing. Things have always been more complicated than we wished, but the Lean 3 to Lean 4 transition is especially difficult (as with any major update in a complicated software). Hopefully this will be over soon.

Last updated: Dec 20 2023 at 11:08 UTC

Stream: new members

Topic: Elan issue on Ubuntu

Marie Kerjean (Jun 22 2023 at 18:58):

Patrick Massot (Jun 22 2023 at 19:00):

Patrick Massot (Jun 22 2023 at 19:01):

Marie Kerjean (Jun 22 2023 at 19:04):

Kevin Buzzard (Jun 22 2023 at 19:06):

Patrick Massot (Jun 22 2023 at 19:08):

Patrick Massot (Jun 22 2023 at 19:10):

Patrick Massot (Jun 22 2023 at 19:10):

Patrick Massot (Jun 22 2023 at 19:11):

Marie Kerjean (Jun 22 2023 at 19:13):

Patrick Massot (Jun 22 2023 at 19:14):

Patrick Massot (Jun 22 2023 at 19:14):

Marie Kerjean (Jun 22 2023 at 19:16):

Sebastian Ullrich (Jun 22 2023 at 19:18):

Marie Kerjean (Jun 22 2023 at 19:20):

Patrick Massot (Jun 22 2023 at 19:20):

Patrick Massot (Jun 22 2023 at 19:21):

Patrick Massot (Jun 22 2023 at 19:22):

Marie Kerjean (Jun 22 2023 at 19:22):

Patrick Massot (Jun 22 2023 at 19:23):

Marie Kerjean (Jun 22 2023 at 19:23):

Patrick Massot (Jun 22 2023 at 19:24):

Patrick Massot (Jun 22 2023 at 19:25):

Marie Kerjean (Jun 22 2023 at 19:25):

Patrick Massot (Jun 22 2023 at 19:25):

Marie Kerjean (Jun 22 2023 at 19:25):

Patrick Massot (Jun 22 2023 at 19:26):

Patrick Massot (Jun 22 2023 at 19:27):

Marie Kerjean (Jun 22 2023 at 19:27):

Patrick Massot (Jun 22 2023 at 19:27):

Patrick Massot (Jun 22 2023 at 19:28):

Patrick Massot (Jun 22 2023 at 19:30):

Marie Kerjean (Jun 22 2023 at 19:31):

Marie Kerjean (Jun 22 2023 at 19:38):

Kevin Buzzard (Jun 22 2023 at 19:41):

Marie Kerjean (Jun 22 2023 at 20:27):

Patrick Massot (Jun 22 2023 at 20:42):