Lake new errors

Stream: lean4

[Shreyas Srinivas]

lake new <project name> math as of now ends in the following error. I have tried this twice:

 [5/21] Building Batteries.Data.String.Basic
trace: .> LEAN_PATH=/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/Cli/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/Qq/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/aesop/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/proofwidgets/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/importGraph/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/plausible/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/mathlib/.lake/build/lib/lean:Consensus/.lake/build/lib/lean /home/shreyas/.elan/toolchains/leanprover--lean4---v4.24.0/bin/lean /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/Batteries/Data/String/Basic.lean -o /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Basic.olean -i /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Basic.ilean -c /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.c --setup /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.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=/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/Cli/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/Qq/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/aesop/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/proofwidgets/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/importGraph/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/plausible/.lake/build/lib/lean:/media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/mathlib/.lake/build/lib/lean:Consensus/.lake/build/lib/lean /home/shreyas/.elan/toolchains/leanprover--lean4---v4.24.0/bin/lean /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/Batteries/Data/Array/Match.lean -o /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.olean -i /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.ilean -c /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c --setup /media/shreyas/d6bf7385-dcc0-4d27-adb5-1d1969c9345b/Projects/Consensus/.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:22: Unknown constant `Std.Iterators.PlausibleIterStep.deflate`

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

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

[Anne Baanen]

This looks similar to recent cache issues, which we are trying to fix in this thread: #mathlib4 > Build error in Tactic file

[Shreyas Srinivas]

current toolchain:

active toolchain
----------------

leanprover/lean4:v4.24.0 (resolved from default 'stable')
Lean (version 4.24.0, x86_64-unknown-linux-gnu, commit 797c613eb9b6d4ec95db23e3e00af9ac6657f24b, Release)

[Shreyas Srinivas]

Anne Baanen said:

This looks similar to recent cache issues, which we are trying to fix in this thread: #mathlib4 > Build error in Tactic file

oh okay. But I haven't actually called update or cache yet

[Anne Baanen]

On the other hand, the issues seemed to come from version 4.25.0-rc{1,2}, not 4.24.0. Let me see if I can reproduce them.

[Anne Baanen]

So the precise commands you run are lake new foo math; cd foo; lake build?

[Shreyas Srinivas]

I didn't even get to the second and third commands

[Shreyas Srinivas]

Just lake new Consensus math

[Anne Baanen]

Ah yes, I can reproduce this with lake +v4.24.0 new bar math.

[Shreyas Srinivas]

Also happens with lake +v4.23.0 new Consensus math

[Eric Wieser]

I think that the lake version has to match the mathlib version, otherwise it fails

[Shreyas Srinivas]

Also tried lake +v4.22.0 new Consensus math. Got the same error.

I then checked the generated lean-toolchain:
leanprover/lean4:v4.25.0-rc1

[Eric Wieser]

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

[Shreyas Srinivas]

I am not at build error

[Shreyas Srinivas]

I am really just creating a new project from scratch

[Eric Wieser]

Shreyas Srinivas said:

error: build failed

looks like you are to me

[Shreyas Srinivas]

In any case, that thread speaks about getting version specific toolchains. It doesn't explain the first error

[Shreyas Srinivas]

Screenshot from 2025-10-22 17-35-48.png

[Eric Wieser]

Every toolchain is version-specific

[Eric Wieser]

That screenshot is basically identical to what I posted in the other thread, with a different version number

[Shreyas Srinivas]

This has never been a problem before. lake new <,,,> math has always worked by picking the right toolchain. my default toolchain is v4.24.0

[Shreyas Srinivas]

cache or build might fail

[Shreyas Srinivas]

But not lake new ...

[Shreyas Srinivas]

and lake usually picks the corresponding mathlib toolchain

[Shreyas Srinivas]

Given that it's the entrypoint to creating a project in the first place, I don't see how I can ensure in advance that the toolchains match

[Eric Wieser]

You can't, this is a bug in new ... math, as reported in the other thread

[Kim Morrison]

Oh! The other thread doesn't actually talk about there being a bug, I interpreted that thread as a feature request for lake +v4.22.0 new Foo math to select Mathlib at the v4.22.0 tag.

[Kim Morrison]

But this is serious! I currently get

$ lake new lakenew math
info: downloading mathlib `lean-toolchain` file
info: lakenew: 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 '540c589f9555258461780f6cee59e27234079db9'
info: toolchain not updated; already up-to-date
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '8864a73bf79aad549e34eff972c606343935106d'
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 '451499ea6e97cee4c8979b507a9af5581a849161'
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 '1fa48c6a63b4c4cda28be61e1037192776e77ac0'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '95c2f8afe09d9e49d3cacca667261da04f7f93f7'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'c44068fa1b40041e6df42bd67639b690eb2764ca'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '72ae7004d9f0ddb422aec5378204fdd7828c5672'
info: mathlib: running post-update hooks
✖ [3/21] Building Batteries.Data.Array.Match
trace: .> LEAN_PATH=/home/kim/scratch/lakenew/.lake/packages/Cli/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/Qq/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/aesop/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/importGraph/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/plausible/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/mathlib/.lake/build/lib/lean:lakenew/.lake/build/lib/lean /home/kim/.elan/toolchains/leanprover--lean4---v4.24.0/bin/lean /home/kim/scratch/lakenew/.lake/packages/batteries/Batteries/Data/Array/Match.lean -o /home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.olean -i /home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.ilean -c /home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c --setup /home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.setup.json --json
error: Batteries/Data/Array/Match.lean:1:0: invalid -D parameter, unknown configuration option 'backward.privateInPublic.warn'

If the option is defined in this library, use '-Dweak.backward.privateInPublic.warn' to set it conditionally
error: Lean exited with code 1
✖ [4/21] Building Batteries.Data.String.Basic
trace: .> LEAN_PATH=/home/kim/scratch/lakenew/.lake/packages/Cli/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/Qq/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/aesop/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/proofwidgets/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/importGraph/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/plausible/.lake/build/lib/lean:/home/kim/scratch/lakenew/.lake/packages/mathlib/.lake/build/lib/lean:lakenew/.lake/build/lib/lean /home/kim/.elan/toolchains/leanprover--lean4---v4.24.0/bin/lean /home/kim/scratch/lakenew/.lake/packages/batteries/Batteries/Data/String/Basic.lean -o /home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Basic.olean -i /home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/String/Basic.ilean -c /home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.c --setup /home/kim/scratch/lakenew/.lake/packages/batteries/.lake/build/ir/Batteries/Data/String/Basic.setup.json --json
error: Batteries/Data/String/Basic.lean:1:0: invalid -D parameter, unknown configuration option 'backward.privateInPublic.warn'

If the option is defined in this library, use '-Dweak.backward.privateInPublic.warn' to set it conditionally
error: Lean exited with code 1
Some required targets logged failures:
- Batteries.Data.Array.Match
- Batteries.Data.String.Basic
error: build failed

@Mac Malone, I think the problem here is that lake new is running the Mathlib post-update hooks using an older Lean version than the toolchain specifies in the repository?

Despite the error output from lake new quoted above, once you enter the repository lake update and lake build seem to work as expected.

Can someone confirm they see the same behaviour?

This seems like an urgent problem: the main entry point for creating Lean math projects is broken.

[Mac Malone]

@Kim Morrison Unfortunately, this is sadly not fixable by fixing Lake as the problem is that old Lake versions do not perfom an restart upon downloading the new toolchain. Implementing Eric's feature request will fix in this behavior in future versions (by removing the offending logic), but older toolchains will still break.

[Mac Malone]

Independently, it should be possible to hotfix this in mathlib by prefixing the option with weak to make it backwards-compatible (though this may be insufficient if the newer toolchain really is required to build cache).

[Mac Malone]

Also, since this is a failure in the post-update hook, the project should still be properly created and running lake exe cache get afterwards should work?

[Kim Morrison]

Yes, the project created does work. It's just that users will not know this, and perhaps assume (reasonably) that the error messages from lake new mean that they should give up. :-)

[Mac Malone]

Yeah, this is definitely not ideal, but as a small comfort, at least its not fully broken.

[Mac Malone]

As another potential fix, we could add a check to the Mathlib post-update hook that skips fetching the cache (with instructions) if it detects this toolchain mismatch.

[Kim Morrison]

Does batteries#1479 look right?

[Kim Morrison]

I like the idea of defence in depth and adding a guard to the post-update hook. Is your suggestion just to check whether lean.versionString matches the contents of lean-toolchain appropriately?

[Mac Malone]

The PR looks godd to me! My only concern is whether that is actually sufficient ot avoid any errors in the post-update hook. As for the post-update hook, change that should be fine as quick fix (and should work generally after implementing Eric's suggestion)

[Kim Morrison]

I guess we also need to have a some CI somewhere to detect lake new Foo math not working so we catch this in time next time! I guess this can't actually happen in Mathlib CI, because things only break once master is updated... Any ideas?

[Mac Malone]

With Eric's feature lake new will always be using an fixed old version of mathlib (the one for the toolchain), so that would also complicate testing this. There is a Lake test which tests the Lake templates, but the lake new .. math part is not run in CI because we did not want to performon network interactions in the test suite.

[Mac Malone]

Perhaps we could performa similar test as part of the release process since lake new will be pinned to releases?

[Kim Morrison]

Oh, I'm confused. I don't like the idea that lake new would be using a fixed old version. That's not okay.

I thought Eric's suggestion was to support explicitly overriding the toolchain so lake +v4.22.0 new Foo math would work, but just lake new Foo math would still always give a lean-toolchain file matching current Mathlib master.

[Kim Morrison]

Mac Malone said:

As another potential fix, we could add a check to the Mathlib post-update hook that skips fetching the cache (with instructions) if it detects this toolchain mismatch.

#30956

[Eric Wieser]

My proposal was for lake new math to on most systems track mathlib stable

[Shreyas Srinivas]

To add more data:

1. Yes lake cache works.
2. There are new users joining on the lean discord who have run into this issue

[Kim Morrison]

lake new foo math is now working again.

[Kim Morrison]

I would love to see someone add a check in CI (maybe a scheduled job, along with lean4checker and the Mathlib executable?) that ensures this can't happen again.

[Kim Morrison]

At least that we promptly notice it.