Should mathlib be buildable with leanprover/lean4:v4.22.0?

Stream: general

[Stuart Hungerford]

I'm trying to build a test project that requires mathlib. I've installed elan (on macOS) with homebrew:

❭ which elan
/opt/homebrew/bin/elan

And I've installed a Lean toolchain:

❭ elan show
leanprover/lean4:v4.22.0 (resolved from default 'leanprover/lean4:stable')
Lean (version 4.22.0, arm64-apple-darwin23.6.0, commit ba2cbbf09d4978f416e0ebd1fceeebc2c4138c05, Release)

And added a section to my lakefile.toml:

[[require]]
name = "mathlib"
scope = "leanprover-community"

But building the project gives these errors:

❭ lake build
✖ [82/331] Building Batteries.Tactic.Lint.Basic
trace: .> LEAN_PATH=/Users/stu/projects/numberz/lean/.lake/packages/Cli/.lake/build/lib/lean:/Users/stu/projects/numberz/lean/.lake/packages/batteries/.lake/build/lib/lean:/Users/stu/projects/numberz/lean/.lake/packages/Qq/.lake/build/lib/lean:/Users/stu/projects/numberz/lean/.lake/packages/aesop/.lake/build/lib/lean:/Users/stu/projects/numberz/lean/.lake/packages/proofwidgets/.lake/build/lib/lean:/Users/stu/projects/numberz/lean/.lake/packages/importGraph/.lake/build/lib/lean:/Users/stu/projects/numberz/lean/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/Users/stu/projects/numberz/lean/.lake/packages/plausible/.lake/build/lib/lean:/Users/stu/projects/numberz/lean/.lake/packages/mathlib/.lake/build/lib/lean:/Users/stu/projects/numberz/lean/.lake/build/lib/lean /Users/stu/.elan/toolchains/leanprover--lean4---v4.22.0/bin/lean /Users/stu/projects/numberz/lean/.lake/packages/batteries/Batteries/Tactic/Lint/Basic.lean -o /Users/stu/projects/numberz/lean/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Lint/Basic.olean -i /Users/stu/projects/numberz/lean/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Tactic/Lint/Basic.ilean -c /Users/stu/projects/numberz/lean/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Lint/Basic.c --setup /Users/stu/projects/numberz/lean/.lake/packages/batteries/.lake/build/ir/Batteries/Tactic/Lint/Basic.setup.json --json
error: Batteries/Tactic/Lint/Basic.lean:87:33: Invalid field `foldl`: The environment does not contain `Lean.NameMap.foldl`
  es
has type
  NameMap (Name × Bool)
error: Batteries/Tactic/Lint/Basic.lean:87:33: Invalid field `foldl`: The environment does not contain `Lean.RBMap.foldl`
  es
has type
  RBMap Name (Name × Bool) Name.quickCmp
error: Batteries/Tactic/Lint/Basic.lean:87:33: Invalid field `foldl`: The environment does not contain `Subtype.foldl`
  es
has type
  { t // RBNode.WellFormed Name.quickCmp t }
...

I'm not using VSCode to manage the project or install Lean. Can anyone advise?

[Kim Morrison]

You need to tell us the contents of your lean-toolchain file. The likely cause of your problem is that that is a different toolchain than Mathlib master is using.

[Kim Morrison]

Likely what you are missing is a rev = "v4.22.0" in the require block for Mathlib, and then run lake update again.

[Stuart Hungerford]

The lean-toochain file is:

leanprover/lean4:v4.22.0

[Stuart Hungerford]

Yep that fixed it. Many thanks. The whole infrastructure around Lean is very impressive, congrats to all concerned.