Issues with my setup and Mathlib 4.17

Stream: general

[Alex Gu]

Hi,

I am trying to set up a Lean environment in Mathlib 4.17. I ran lake +leanprover/lean4:nightly-2024-04-24 new mathlib-4-17 math, then added the version to "https://github.com/leanprover-community/mathlib4.git" @ "v4.17.0", and then did lake build && lake update.

I'm getting the error here:

✖ [2/12] Building Cache.Lean
trace: .> LEAN_PATH=/home/gua/lean/mathlib-4-17/.lake/packages/Cli/.lake/build/lib/lean:/home/gua/lean/mathlib-4-17/.lake/packages/batteries/.lake/build/lib/lean:/home/gua/lean/mathlib-4-17/.lake/packages/Qq/.lake/build/lib/lean:/home/gua/lean/mathlib-4-17/.lake/packages/aesop/.lake/build/lib/lean:/home/gua/lean/mathlib-4-17/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/gua/lean/mathlib-4-17/.lake/packages/importGraph/.lake/build/lib/lean:/home/gua/lean/mathlib-4-17/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/gua/lean/mathlib-4-17/.lake/packages/plausible/.lake/build/lib/lean:/home/gua/lean/mathlib-4-17/.lake/packages/mathlib/.lake/build/lib/lean:/home/gua/lean/mathlib-4-17/.lake/build/lib/lean /home/gua/.elan/toolchains/leanprover--lean4---v4.23.0-rc2/bin/lean /home/gua/lean/mathlib-4-17/.lake/packages/mathlib/Cache/Lean.lean -o /home/gua/lean/mathlib-4-17/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Lean.olean -i /home/gua/lean/mathlib-4-17/.lake/packages/mathlib/.lake/build/lib/lean/Cache/Lean.ilean -c /home/gua/lean/mathlib-4-17/.lake/packages/mathlib/.lake/build/ir/Cache/Lean.c --setup /home/gua/lean/mathlib-4-17/.lake/packages/mathlib/.lake/build/ir/Cache/Lean.setup.json --json
error: Cache/Lean.lean:7:0: object file '/home/gua/.elan/toolchains/leanprover--lean4---v4.23.0-rc2/lib/lean/Lean/Util/Paths.olean' of module Lean.Util.Paths does not exist
error: Lean exited with code 1
Some required targets logged failures:
- Cache.Lean
error: build failed

I tried various things like deleting the .lake file, lake clean, re-installing, etc, but could not fix the issue. Any guidance would be appreciated. Thanks!

[Ruben Van de Velde]

Why v4.17.0?

[Alex Gu]

Trying to reproduce some results on PutnamBench, and the official repo is in 4.17 :smile:

[Alex Gu]

but I guess the issue is that new versions of the toolchain are not compatible with older versions of mathlib?

[Jon Eugster]

make sure the lean-toolchain of your project is set to v4.17.0, too. And then you need to ensure all required packages in the lakefile are set to that specific version, maybe deleting the lake-manifest.json or calling lake update (after you fixed all the versions).

If that doesn't work, post the content of your lean-toolchain and your lakefile.lean (or .toml), at least the part about the required dependencies.

[Jon Eugster]

(I see you're currently using v4.23.0-rc2 instead of v4.17.0)