lake build issues with GlimpseOfLean

Stream: new members

[Kaden Uhlig]

I'm trying to learn Lean with GlimpseOfLean, but I can't get the install working. I've searched around in Zulip and tried a few different solutions, but can't seem to get anything that works.

Specifically, I'm doing the following:

git clone https://github.com/PatrickMassot/GlimpseOfLean.git
cd GlimpseOfLean
lake exe cache clean!

At this point, I get an error about the lake-manifest.json file:

warning: improperly formatted manifest: incompatible manifest version `4`
error: dependency 'mathlib' of 'glimpseOfLean' not in manifest, use `lake update` to update

So I do so, it seems to work (clones all the dependencies into lake-packages), and I try lake exe cache clean! again. That also seems to work, although I get warnings about unused linker input files (I can post the output if it's relevant).

Finally, I run lake build and get this partway through:

error: > LEAN_PATH=./lake-packages/proofwidgets/build/lib:./lake-packages/Cli/build/lib:./lake-packages/mathlib/build/lib:./lake-packages/Qq/build/lib:./lake-packages/aesop/build/lib:./build/lib:./lake-packages/std/build/lib LD_LIBRARY_PATH=:/opt/cuda/targets/x86_64-linux/lib:./lake-packages/mathlib/build/lib /usr/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./lake-packages/mathlib/././Mathlib/Tactic/NthRewrite.lean -R ./lake-packages/mathlib/./. -o ./lake-packages/mathlib/build/lib/Mathlib/Tactic/NthRewrite.olean -i ./lake-packages/mathlib/build/lib/Mathlib/Tactic/NthRewrite.ilean -c ./lake-packages/mathlib/build/ir/Mathlib/Tactic/NthRewrite.c
error: stdout:
./lake-packages/mathlib/././Mathlib/Tactic/NthRewrite.lean:36:26: error: 'occs' is not a field of structure 'Lean.Meta.Rewrite.Config'
error: external command `/usr/bin/lean` exited with code 1

I've tried messing around with lean-toolchain and changing it to match lake-packages/mathlib/lean-toolchain, deleting and regenerating the lake-manifest.json file, and all sorts of combinations of the above. Any ideas on how I can get this working? I'd really just love to try learning a bit of Lean, but I've spent two hours getting the LSP working (in Neovim, so there it's perhaps my own fault for introducing complexity and not just going with VSCode or emacs) and don't really want to spend another two hours mucking around on my own trying things out :)

[Kyle Miller]

Oh no, I was going to suggest copying lake-packages/mathlib/lean-toolchain to lean-toolchain, but then you mentioned you already did that.

Just to check, do the following steps cause an error for you?

git clone https://github.com/PatrickMassot/GlimpseOfLean.git
cd GlimpseOfLean
cp lake-packages/mathlib/lean-toolchain lean-toolchain
lake exe cache get

[Kaden Uhlig]

Yeah :sweat_smile: I saw your message about that, haha. Unfortunately those commands do cause an error, but mostly because lake-packages doesn't exist right after cloning the repo

[Kyle Miller]

Oh right, the cp doesn't work.

[Ruben Van de Velde]

That sounds like a chicken and egg situation

[Kyle Miller]

You could do lake exe cache get first (which won't work) and then do cp, and then try again.

[Kaden Uhlig]

I am 90% sure I already tried that (or rather, noted what was in the file, cloned, changed it to that, and then did the other steps), but on the off chance I didn't, here goes :)

[Kyle Miller]

Maybe I'll try this locally myself before giving you more suggestions. I can tell you that I do have a working copy of GlimpsOfLean on my work computer that I could check tomorrow.

[Ruben Van de Velde]

glimpse master depends on https://github.com/leanprover-community/mathlib4/tree/a3b66ecb2f91d93379698626e7ec98a28b893b4d , so the lean-toolchain should look like https://github.com/leanprover-community/mathlib4/blob/a3b66ecb2f91d93379698626e7ec98a28b893b4d/lean-toolchain

[Kyle Miller]

Thanks. That means lean-toolchain is correct for GlimpseOfLean

[Kaden Uhlig]

That'd be nice. I'm probably going to go to bed soon anyway, and won't have time for this until tomorrow evening, so I'm not in too much of a hurry.

With running lake exe cache get first, I get this error:

warning: improperly formatted manifest: incompatible manifest version `4`
error: dependency 'mathlib' of 'glimpseOfLean' not in manifest, use `lake update` to update

[Julian Berman]

Kaden Uhlig said:

I've spent two hours getting the LSP working (in Neovim, so there it's perhaps my own fault for introducing complexity and not just going with VSCode or emacs)

Not relevant to your question of course but I'd love to know what got you stuck in setting things up.

[Ruben Van de Velde]

The next thing I'd try would be manually changing "4" to "5" in lake-manifest.json

[Kaden Uhlig]

@Julian Berman Issues fully in my own, overgrown and convoluted config – nothing wrong with your delightful plugin, haha

[Kyle Miller]

@Kaden Uhlig These do work for me:

git clone https://github.com/PatrickMassot/GlimpseOfLean.git
cd GlimpseOfLean
lake exe cache get

[Kyle Miller]

Do you have any sort of lean toolchain override configured?

[Kyle Miller]

Ruben Van de Velde said:

The next thing I'd try would be manually changing "4" to "5" in lake-manifest.json

I would be wary of doing this, but it's worth a shot since it won't break anything, and if it works, great!

[Ruben Van de Velde]

Kyle Miller said:

Kaden Uhlig These do work for me:

git clone https://github.com/PatrickMassot/GlimpseOfLean.git
cd GlimpseOfLean
lake exe cache get

Did you get the manifest version message while doing that?

[Kyle Miller]

No I don't, that's what I mean by it working

[Kyle Miller]

@Kaden Uhlig What do you get when you do lake --version?
Here's mine:

~/Projects/GlimpseOfLean(master) % lake --version
Lake version 4.1.0-pre (Lean version 4.0.0-nightly-2023-06-20)

Note that 2023-06-20 matches the lean-toolchain file

[Kaden Uhlig]

kuhlig lean $ rm -rf GlimpseOfLean/
kuhlig lean $ git clone https://github.com/PatrickMassot/GlimpseOfLean.git
Cloning into 'GlimpseOfLean'...
remote: Enumerating objects: 307, done.
remote: Counting objects: 100% (19/19), done.
remote: Compressing objects: 100% (10/10), done.
remote: Total 307 (delta 14), reused 9 (delta 9), pack-reused 288
Receiving objects: 100% (307/307), 89.23 KiB | 2.62 MiB/s, done.
Resolving deltas: 100% (152/152), done.
kuhlig lean $ cd GlimpsOfLean
kuhlig lean $ lake exe cache get
warning: improperly formatted manifest: incompatible manifest version `4`
error: dependency 'mathlib' of 'glimpseOfLean' not in manifest, use `lake update` to update

Do you have any sort of lean toolchain override configured?

Not that I know of.

The next thing I'd try would be manually changing "4" to "5" in lake-manifest.json

Unfortunately already tried that :)

[Kaden Uhlig]

I'm trying for the life of me to remember/find out how I installed lean, to double check that I didn't do something odd. It was a couple(?) months ago, and I can't find anything at all in my .bash_history, which is odd

[Kyle Miller]

Could you do lake --version? I think this would be the best thing for diagnosis right now

[Kaden Uhlig]

Lake version 5.0.0-src (Lean version 4.0.0, commit a7efe5b60e86b26fefd4795b46d66af369b97329)

[Kyle Miller]

Hmm, I don't know how toolchain selection works well enough to really help, but as a test, could you do ~/.elan/bin/lake --version? Maybe that will pick up on the right version.

[Kaden Uhlig]

It does look like I installed lean through the AUR, not through elan, which might be an issue

[Kyle Miller]

Yes, that will be an issue, especially if it comes first in your PATH before the one in ~/.elan/bin. If my previous suggestion gives a sensible result, you can do ~/.elan/bin/lake exe cache get and then figure out how to fix your PATH later :smile:

[Kaden Uhlig]

Kyle Miller said:

Hmm, I don't know how toolchain selection works well enough to really help, but as a test, could you do ~/.elan/bin/lake --version? Maybe that will pick up on the right version.

I'll try uninstalling lean with my package manager than installing it through elan real quick. Maybe that will clear things up.

[Kyle Miller]

Could you do my suggestion first quick?

[Kaden Uhlig]

I don't even have the ~/.elan directory haha

[Kyle Miller]

Ok, carry on :smile:

[Kaden Uhlig]

Wonderful – with lean installed through elan and not the package manager, everything works out of the box. Sorry for all the trouble, but thanks for such quick help!

[Kevin Buzzard]

We really should attempt to remove these prepackaged lean installations because they cause far more harm than good. Which package manager was it?

[Kevin Buzzard]

Literally no project works if you don't install exactly the right way

[Utensil Song]

It's a surprise that AUR has pre-packaged Lean 4 4.0.0.rc4-1 :astonished:

[Utensil Song]

The only useful pre-packaged Lean stuff might be the brew one for Mac, as elan can't be installed via curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh on Mac M1 etc. and has to go through brew install elan-init.

[Chris Wong]

An operating system package manager aims to maintain compatibility with the rest of the operating system. That's the wrong problem to solve for a programming project, where the goal is to maintain compatibility with other people working on the project, not your own OS

[Chris Wong]

Filed a docs PR: https://github.com/leanprover-community/leanprover-community.github.io/pull/369