Build error on `lake +leanprover/lean4:v4.22.0 new foo math`

Stream: lean4

[Eric Wieser]

$ lake --version
Lake version 5.0.0-src+797c613 (Lean version 4.24.0)

$ lake +leanprover/lean4:v4.22.0 new foo math
info: downloading mathlib `lean-toolchain` file
info: foo: no previous manifest, creating one from scratch
info: leanprover-community/mathlib: cloning https://github.com/leanprover-community/mathlib4
info: leanprover-community/mathlib: checking out revision 'b758e7655e75c5182dc07bf1855fa553b6befc7f'
info: toolchain not updated; already up-to-date
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '7607162f5a1c1eb23c23027629a418b3a160670e'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '2ed4ba69b6127de8f5c2af83cccacd3c988b06bf'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'e5c37730d22634ee0169c164f25dac49918ed951'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision 'fb8ed0a85a96e3176f6e94b20d413ea72d92576d'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision 'cbe864cd5177966c9e005418cfdc1fb36db62e13'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '593aa51c4aa07ee81e9233b53e1f61a5b4d9f761'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '5bd478197f2e5d2a4fde527cf3581d83f49baa9b'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'f75f4926aff7ba19949e16c19094d7298806b1a6'
info: mathlib: running post-update hooks
✖ [6/21] Building Batteries.Data.String.Basic
trace: .> LEAN_PATH=~/foo/.lake/packages/Cli/.lake/build/lib/lean:~/foo/.lake/packages/batteries/.lake/build/lib/lean:~/foo/.lake/packages/Qq/.lake/build/lib/lean:~/foo/.lake/packages/aesop/.lake/build/lib/lean:~/foo/.lake/packages/proofwidgets/.lake/build/lib/lean:~/foo/.lake/packages/importGraph/.lake/build/lib/lean:~/foo/.lake/packages/LeanSearchClient/.lake/build/lib/lean:~/foo/.lake/packages/plausible/.lake/build/lib/lean:~/foo/.lake/packages/mathlib/.lake/build/lib/lean:foo/.lake/build/lib/lean ~/.elan/toolchains/leanprover--lean4---v4.22.0/bin/lean ~/foo/.lake/packages/batteries/Batteries/Data/String/Basic.lean -o ~/foo/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Basic.olean -i ~/foo/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Basic.ilean -c ~/foo/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.c --setup ~/foo/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.setup.json --json
error: Batteries/Data/String/Basic.lean:28:12: unknown constant 'String.Pos.Raw'
error: Batteries/Data/String/Basic.lean:31:29: unknown constant 'String.Pos.Raw.next'
error: Batteries/Data/String/Basic.lean:34:30: Invalid field notation: Type of
  c
is not known; cannot resolve field `toUInt8`
warning: Batteries/Data/String/Basic.lean:35:4: unused `termination_by`, function is not recursive
error: Lean exited with code 1
✖ [9/21] Building Batteries.Data.Array.Match
trace: .> LEAN_PATH=~/foo/.lake/packages/Cli/.lake/build/lib/lean:~/foo/.lake/packages/batteries/.lake/build/lib/lean:~/foo/.lake/packages/Qq/.lake/build/lib/lean:~/foo/.lake/packages/aesop/.lake/build/lib/lean:~/foo/.lake/packages/proofwidgets/.lake/build/lib/lean:~/foo/.lake/packages/importGraph/.lake/build/lib/lean:~/foo/.lake/packages/LeanSearchClient/.lake/build/lib/lean:~/foo/.lake/packages/plausible/.lake/build/lib/lean:~/foo/.lake/packages/mathlib/.lake/build/lib/lean:foo/.lake/build/lib/lean ~/.elan/toolchains/leanprover--lean4---v4.22.0/bin/lean ~/foo/.lake/packages/batteries/Batteries/Data/Array/Match.lean -o ~/foo/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.olean -i ~/foo/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.ilean -c ~/foo/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c --setup ~/foo/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.setup.json --json
error: Batteries/Data/Array/Match.lean:64:43: unknown identifier 'Std.Stream'
error: Batteries/Data/Array/Match.lean:85:30: unknown identifier 'Std.Stream'
error: Batteries/Data/Array/Match.lean:93:35: unknown identifier 'Std.Stream'
error: Batteries/Data/Array/Match.lean:130:23: Unknown identifier `Std.Iterators.PlausibleIterStep.deflate`

Note: Inferred this identifier from the expected type of `.deflate`:
  PlausibleIterStep fun step => ∃ step', modifyStep m it step' = step
error: Batteries/Data/Array/Match.lean:130:23: Unknown identifier `Subtype.deflate`

Note: Inferred this identifier from the expected type of `.deflate`:
  PlausibleIterStep fun step => ∃ step', modifyStep m it step' = step
error: Lean exited with code 1
Some required builds logged failures:
- Batteries.Data.String.Basic
- Batteries.Data.Array.Match
error: build failed

[Eric Wieser]

It looks like lake +leanprover/lean4:v4.22.0 new ignores the version I specify and uses the latest lean:

$ cat foo/lean-toolchain
leanprover/lean4:v4.25.0-rc1

[Eric Wieser]

Without math it works fine:

$ lake +leanprover/lean4:v4.22.0 new bar
$ cat bar/lean-toolchain
leanprover/lean4:v4.22.0

[Mac Malone]

This is because the math template uses the toolchain of mathlib. One might hope that Lake could make use of the fact that you explicitly specified a toolchain to do something smarter here. Unfortunately, Lake receives this toolchain information from elan via ELAN_TOOLCHAIN, which does not distinguish between an explicitly speciifed toolchain version and an implicit one.

[Eric Wieser]

I think I understand why I end up with the wrong version, but why does the build crash? It looks like I have a mixture of versions?

[Eric Wieser]

I wouldn't expect the explicit specification of tool chain to be relevant; rather I'd expect this to always choose a mathlib version matching my toolchain version

[Eric Wieser]

That is, I would expect lake new ... math to fetch the v{leanVersionNumber} tag of mathlib

[Kim Morrison]

Seems like a reasonable feature request / contribution?

[Eric Wieser]

I guess this will only work for 4.26.0 onwards though, in the best case

[Mac Malone]

Eric Wieser said:

That is, I would expect lake new ... math to fetch the v{leanVersionNumber} tag of mathlib

With elan now auto-updating stable toolchains and reliable tagging of Mathlib versions, I think this would be reasonable. Previously, many users definitely wanted Mathlib to determine their toolchain and not vice versa.