lake build issues

Stream: new members

[Alex]

I had the same error message when trying to add mathlib to an existing project. I copied from an example project lakefile require mathlib from git "https://github.com/leanprover-community/mathlib4"@"master". I tried to clean and update, but it wouldn't go away.
I then tried making a new project like it says here https://leanprover-community.github.io/install/project.html#creating-a-lean-project and it worked. I think the main difference is the corresponding, autogenerated, line doesn't reference any branch:

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

[Utensil Song]

When adding mathlib to an existing project, in the lakefile, mathlib has to be added before other dependencies that also uses Std4 .

[Alex]

Mathlib is the only dependency in my buildfile. I made both the new project and old one lakefiles the same other than the name, but I still get the error on the old one, but not the new.

[155/3357] Building Mathlib.Tactic.Spread
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:./lake-packages/std/build/lib:./build/lib LD_LIBRARY_PATH=./lake-packages/mathlib/build/lib /home/user/.elan/toolchains/leanprover--lean4---4.0.0/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 `/home/user/.elan/toolchains/leanprover--lean4---4.0.0/bin/lean` exited with code 1

I see that it includes Std, but the lakefile only references Lake and DSL before mathlib.

[Mauricio Collares]

Your toolchain (as determined by the lean-toolchain file) must match mathlib's.

[Utensil Song]

Yes, the latest mathlib is already using v4.2.0-rc1, and since v4.1.0, there's a breaking change about occs: https://github.com/leanprover/lean4/releases

[Kyle Miller]

@Alex Make sure your lean-toolchain has the same contents as lake-packages/mathlib/lean-toolchain (This is what Mauricio is saying, but I'm just adding the filename to look at)

[Alex]

@Kyle Miller Am I supposed to edit the lean-toolchain files directly? I thought you were supposed to edit just the lakefile.
The problem was that I accidentally deleted the root lean-toolchain. I added the 4.1.0 one and didn't get the error, even though the mathlib lean-toolchain is 4.2.0. I'll set them both to 4.2.0.

[Kyle Miller]

Yeah, I don't believe lake itself ever manages the lake-toolchain file. I usually copy the mathlib one into my project root.

[Utensil Song]

Alex said:

Kyle Miller Am I supposed to edit the lean-toolchain files directly? I thought you were supposed to edit just the lakefile.
The problem was that I accidentally deleted the root lean-toolchain. I added the 4.1.0 one and didn't get the error, even though the mathlib lean-toolchain is 4.2.0. I'll set them both to 4.2.0.

Setting it to 4.1.0 will solve only that specific error. Toolchain inconsistency with Mathlib for a project depending on Mathlib could lead to less obvious issues (e.g. see #6928 for how the difference between 4.2.0-rc1 and 4.1.0 subtly impacts Mathlib proofs). So it's generally advisable to keep them consistent.

It would be really nice if lake can check toolchain inconsistency in general, and allow libraries like mathlib to declare the requirement of such consistency so lake can give errors instead of warnings accordingly.

[Alex]

Is it really ok to make sure all the lean-toolchain to the same version even if that's different than the one in git? I feel like it's not because lake update aborts because of uncommitted changes and because lake build also warns about them.
I set all the math-required packages to 4.2.0: aesop, Cli, mathlib, proofwidgets, Qq, and std. I hope this is ok.

[Yaël Dillies]

4.2.0 is not out yet, right?

[Matthew Pocock]

I just hit this when doing a lake update. My toolchain is leanprover/lean4:v4.0.0-rc4. My lakefile.lean dependency is

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

The toolchain in that git repo is leanprover/lean4:v4.2.0-rc1

It would be nice if the tooling did a toolchain sanity check that the toolchain of the libs isn't a significantly different one from the project, and gave options to fix things where they don't match.

[Bolton Bailey]

See previous discussion here