Errors when using old Lean version

Stream: general

[Markus de Medeiros]

I want to use Lean 4.21.0 in a new project with that version of mathlib. In a completely fresh project with the configuration below, lake build works:

lake build output

markusde@mac myProject % lake build
info: mathlib: cloning https://github.com/leanprover-community/mathlib4
info: mathlib: checking out revision '377c35f5df452d352c03f82784efd629d4f27f41'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'c37191eba2da78393070da8c4367689d8c4276e4'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '6c62474116f525d2814f0157bb468bf3a4f9f120'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '4241928fd3ebae83a037a253e39d9b773e34c3b4'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '96c67159f161fb6bf6ce91a2587232034ac33d7e'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '0a136f764a5dfedc4498e93ad8e297cff57ba2fc'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '1ef3dac0f872ca6aaa7d02e015427e06dd0b6195'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision 'e96b5eca4fcfe2e0e96a1511a6cd5747515aba82'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision 'c682c91d2d4dd59a7187e2ab977ac25bd1f87329'
Build completed successfully.

But when I add import Mathlib to Basic.lean, I get a ton of errors:

Representative error

error: Lean exited with code 1
✖ [70/7017] Building Batteries.Tactic.OpenPrivate
trace: .> LEAN_PATH= ... --json
error: Batteries/Tactic/OpenPrivate.lean:1:0: invalid -D parameter, unknown configuration option 'linter.unusedSimpArgs'

Here is my lakefile (lean-toolchain isleanprover/lean4:v4.21.0). Am I missing something in my configuration?

lakefile.toml

name = "myProject"
version = "0.1.0"
keywords = ["math"]
defaultTargets = ["MyProject"]

[leanOptions]
pp.unicode.fun = true # pretty-prints fun a ↦ b
autoImplicit = false

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

[[lean_lib]]
name = "myProject"

[Kim Morrison]

Change "version" to "rev" in the require block.

[Markus de Medeiros]

This did not fix it, and the errors are the same. I even deleted my .lake/ directory and ran lake build again to be sure.

[Kim Morrison]

Is there a repository we could clone to observe the problem?

[Markus de Medeiros]

It is a completely new project but I could put it on github if that would help

[Markus de Medeiros]

https://github.com/markusdemedeiros/IrisLeanMath

[Mac Malone]

@Markus de Medeiros Did you run lake update after changing version to rev?

[Markus de Medeiros]

I didn't! Thanks, let me try.

[Markus de Medeiros]

Yep, it works now, thanks Kim and Mac! I also had to change the rev to "v4.21.0".

[Patrick Massot]

Could you please upvote https://github.com/leanprover/lean4/issues/6482 if you think this is a completely unnecessary trap for new users?