Trouble setting up Lean and mathlib

Stream: new members

[Jard]

Hi everyone! I am currently trying to set up Lean, particularly, I want to use "mathematics in Lean" as I would like to incorporate Lean into my Mathematics bachelor thesis. I have followed the instructions in the book, installed VSCode, retrieved the MIL files and made a copy called my_files. Then, when trying to use import MIL.Common, I get the following error message:

`/home/jard/.elan/toolchains/leanprover--lean4---v4.16.0-rc2/bin/lake setup-file /home/jard/my_files/MIL/C01_Introduction/S02_Overview.lean Init MIL.Common --no-build --no-cache` failed:

stderr:
info: [root]: lakefile.lean and lakefile.toml are both present; using lakefile.lean
warning: mathlib: repository '././.lake/packages/mathlib' has local changes
✖ [3/6] Running Mathlib.Tactic
error: no such file or directory (error code: 2)
  file: ././.lake/packages/mathlib/././Mathlib/Tactic.lean
✖ [4/6] Running Mathlib.Util.Delaborators
error: no such file or directory (error code: 2)
  file: ././.lake/packages/mathlib/././Mathlib/Util/Delaborators.lean
✖ [5/6] Running MIL.Common
error: ././././MIL/Common.lean: bad import 'Mathlib.Tactic'
error: ././././MIL/Common.lean: bad import 'Mathlib.Util.Delaborators'
✖ [6/6] Running imports (/home/jardnijholt/my_files/MIL/C01_Introduction/S02_Overview.lean)
error: /home/jardnijholt/my_files/MIL/C01_Introduction/S02_Overview.lean: bad import 'MIL.Common'
Some required builds logged failures:
- Mathlib.Tactic
- Mathlib.Util.Delaborators
- MIL.Common
- imports (/home/jard/my_files/MIL/C01_Introduction/S02_Overview.lean)
error: build failed

I then googled my problem, which suggested in my terminal using lake +leanprover/lean4:nightly-2023-02-04 new my_files math followed by cd my_files and lake update. As an error to this, I got

trace: ././lake/packages/mathlib> git fetch --tags --force origin
trace: stderr:
fatal: bad object c70e655848b6d1264eae421382d84fdb0b5cce68
error: https://github.com/leanprover-community/mathlib4 did not send all necessary objects
error: external command 'git' exited with code 1

Now, I am not the most computer savvy person, and am not sure what would be the best way to proceed. Is there anyone that can help me out?

[Niels Voss]

Did you just clone the repository recently, or is it an old version? And did you make changes to it and update it, or is it the same state as the GitHub repository?

The reason I ask is because the error message suggests that you have both a lakefile.lean and a lakefile.toml in your folder, which is a problem. Can you confirm if this is the case? If so, can you run git status and post the output here?

[Jard]

I assume with cloning the repository you mean running `git clone https://github.com/leanprover-community/mathematics_in_lean.git` , in which case, I did this morning. I then made a copy of that file, just in the files of my computer, using ctrl+c and ctrl+v. It seems this copying introduced the toml file. Should I have copied it differently?

I did run git status:

jard@penguin:~$ git status
fatal: not a git repository (or any of the parent directories): .git
jard@penguin:~$ cd my_files
jard@penguin:~/my_files$ git status
On branch master
Your branch is up to date with 'origin/master'.

Changes not staged for commit:
  (use "git add <file>..." to update what will be committed)
  (use "git restore <file>..." to discard changes in working directory)
        modified:   .gitignore
        modified:   lean-toolchain

Untracked files:
  (use "git add <file>..." to include in what will be committed)
        .github/workflows/
        MyFiles.lean
        MyFiles/
        lakefile.toml
        my_files/

no changes added to commit (use "git add" and/or "git commit -a")

[Niels Voss]

That's sort of a weird directory structure. From what it looks to me, you copied the files from mathematics in Lean into the new repository you just created with lake new, so now you basically have two different projects in the same directory. If this is what happened, can you go back to the original repository you cloned MIL to, and try running that project? I assume that this is what you tried initially, so I'm curious what errors you got.

Out of curiosity, why did you choose to copy the MIL folder instead of just working on the cloned repo?

[Jard]

I originally copied the folder because the Mathematics in Lean book recommended so:
"1. Each section in this book has an associated Lean file with examples and exercises. You can find them in the folder MIL, organized by chapter. We strongly recommend making a copy of that folder and experimenting and doing the exercises in that copy. This leaves the originals intact, and it also makes it easier to update the repository as it changes (see below). You can call the copy my_files or whatever you want and use it to create your own Lean files as well."

I now used the lake update on the originally retrieved file and it now gives me Imports are out of date and must be rebuilt; use the "Restart File" command in your editor. but when i click "Restart file", it crashes my laptop. I suppose that is more an issue with my laptop than with lean itself, though.

Thank you a lot for your help!

[Ruben Van de Velde]

Try lake exe cache get before lake build

[Jard]

Unfortunately, that still gives me the same error ("The window terminated unexpectedly (reason: 'killed', code: '9')"
is the full error)

[Niels Voss]

I think when the instructions said to copy MIL, they meant the folder inside the repository, not the repository itself. So if your directory structure was

mathematics-in-lean
| MIL
  | ...
| lakefile.lean

Then you should try to make it like

mathematics-in-lean
| MIL
  | ...
| my-files
  | ...
| lakefile.lean

If that is what you did, then I misread your message

[Jard]

I have made the file paths as you proposed, and I think I might be getting somewhere! I get a new error I have not gotten yet, at least. When trying to run lake build, I now get

ℹ [2/2485] Replayed MIL.C01_Introduction.S01_Getting_Started
info: ././././MIL/C01_Introduction/S01_Getting_Started.lean:1:0: "Hello, World!"
✖ [2445/2485] Building MIL.Common
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/jardnijholt/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././MIL/Common.lean -R ./././. -o ././.lake/build/lib/MIL/Common.olean -i ././.lake/build/lib/MIL/Common.ilean -c ././.lake/build/ir/MIL/Common.c --json
error: Lean exited with code 139
Some required builds logged failures:
- MIL.Common
error: build failed

Any further ideas on how to fix this? I so appreciate all the help I have gotten here over the past day.

[Kevin Buzzard]

Just delete everything and start again, this time following the instructions to the letter?

[Jard]

I have deleted everything twice now, and the same error keeps popping up (about the imports being out of date). Could it simply be that my laptop cannot handle lean? I have been using this guide: https://leanprover-community.github.io/install/project.html#working-on-an-existing-project

[Kevin Buzzard]

Hmm. Error code 139 seems to indicate some kind of segfault?

Try this. First, disable your antivirus, if you're on Windows. Then remove the relevant version of Lean from your system (in case this is what is corrupt)

elan uninstall leanprover/lean4:v4.13.0

And then just do the absolute basics to install the repo:

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

And post the output of everything, except stop the moment one of these commands gives you any kind of error message (because we want to know the first thing that goes wrong, not the last thing). Then reenable your antivirus :-)

[Kevin Buzzard]

(just to be clear, I just tried this and works fine for me, so the problem is almost certainly at your end).

Re "could it be my laptop" -- how much RAM do you have? If 4G then "yes", if 8 then "maybe", if 16 or more then "probably not"

[Jard]

I did as you described and got

jardnijholt@penguin:~$ elan uninstall leanprover/lean4:v4.13.0
info: uninstalling toolchain 'leanprover/lean4:v4.13.0'
info: toolchain 'leanprover/lean4:v4.13.0' uninstalled
jardnijholt@penguin:~$ git clone https://github.com/leanprover-community/mathematics_in_lean.git
Cloning into 'mathematics_in_lean'...
remote: Enumerating objects: 2488, done.
remote: Counting objects: 100% (127/127), done.
remote: Compressing objects: 100% (68/68), done.
remote: Total 2488 (delta 93), reused 59 (delta 59), pack-reused 2361 (from 3)
Receiving objects: 100% (2488/2488), 45.35 MiB | 13.07 MiB/s, done.
Resolving deltas: 100% (1648/1648), done.
jardnijholt@penguin:~$ cd mathematics_in_lean/
jardnijholt@penguin:~/mathematics_in_lean$ lake exe cache get
info: downloading https://github.com/leanprover/lean4/releases/download/v4.13.0/lean-4.13.0-linux_aarch64.tar.zst
225.1 MiB / 225.1 MiB (100 %)  10.9 MiB/s ETA:   0 s
info: installing /home/jardnijholt/.elan/toolchains/leanprover--lean4---v4.13.0
info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to '././.lake/packages/mathlib'
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '././.lake/packages/LeanSearchClient'
info: plausible: cloning https://github.com/leanprover-community/plausible to '././.lake/packages/plausible'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
Attempting to download 5370 file(s)
Downloaded: 5370 file(s) [attempted 5370/5370 = 100%] (100% success)
Decompressing 5370 file(s)
Unpacked in 53543 ms
Completed successfully!
jardnijholt@penguin:~/mathematics_in_lean$ lake build
ℹ [2/2485] Built MIL.C01_Introduction.S01_Getting_Started
info: ././././MIL/C01_Introduction/S01_Getting_Started.lean:1:0: "Hello, World!"
✖ [2445/2485] Building MIL.Common
trace: .> LEAN_PATH=././.lake/packages/batteries/.lake/build/lib:././.lake/packages/Qq/.lake/build/lib:././.lake/packages/aesop/.lake/build/lib:././.lake/packages/proofwidgets/.lake/build/lib:././.lake/packages/Cli/.lake/build/lib:././.lake/packages/importGraph/.lake/build/lib:././.lake/packages/LeanSearchClient/.lake/build/lib:././.lake/packages/plausible/.lake/build/lib:././.lake/packages/mathlib/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH= /home/jardnijholt/.elan/toolchains/leanprover--lean4---v4.13.0/bin/lean -Dpp.unicode.fun=true -DautoImplicit=false -DrelaxedAutoImplicit=false ././././MIL/Common.lean -R ./././. -o ././.lake/build/lib/MIL/Common.olean -i ././.lake/build/lib/MIL/Common.ilean -c ././.lake/build/ir/MIL/Common.c --json
error: Lean exited with code 139
Some required builds logged failures:
- MIL.Common
error: build failed

My laptop does only have 4gb of RAM. I did however monitor memory usage through the task manager, and nothing seemed to spike

[Julian Berman]

Try to collect a crash dump and tell us what it shows perhaps. Here's some instructions for how: https://jvns.ca/blog/2018/04/28/debugging-a-segfault-on-linux/

[Vlad Tsyrklevich]

perhaps a rabbit hole, but if you only have 4gb of RAM, it may be worth checking if you have swap space configured to extend the amount of usable memory

[Kevin Buzzard]

Although it might not be the cause of this problem, my instinct is that unfortunately you will have a thoroughly miserable time trying to use Lean 4 on a machine with only 4gb of RAM. I would recommend that you use one of the online solutions for working on Mathematics In Lean, for example codespaces or gitpod (which I believe is about to be retired). This is what I tell my students who have machines with only 4gb.

[Julian Berman]

(Also from a technical perspective I'd note that just because you don't see memory spiking doesn't mean that nothing's going wrong there, it's possible something is trying to allocate a bunch of memory and being told no and not handling that, or something. The crash dump might say. But as Kevin says even if it works, it's unlikely to work very well -- I have 8GB and that's pushing it already.)

[Jard]

Thanks for all the help; I will try it on my PC that hopefully has more ram tomorrow!

[Jard]

My PC has 8GB of RAM and I just got lean set up and running. Thank you everyone for the help and the welcoming atmosphere, I will soon make an actual introductory topic for myself (as I think we are supposed to in this channel, after looking around a little bit more)