Mathlib lakefile syntax error

Stream: mathlib4

[Gridiron Player]

image.png
Has anybody ever dealt with this error when building a new lean game? Not a lake expert, but there seems to be some syntax error in the mathlib lakefile that I cant find. Maybe a version issue? Idk.

[Rob McQueen]

I'm not a lake/lean expert either, but this is what I'd try:

1. Did you manually edit the lakefile in mathlib? Git seems to think there's local changes. You could try purging .lake and rerunning lake exe cache get
2. Make sure the contents of the lean-toolchain file in your project matches the lean-toolchain file in the mathlib package. This will make sure your version of lean is compatible with that used in mathlib

[Mario Carneiro]

This is a lean version issue when bumping from 4.9.0 to 4.10.0-rc1, and usually happens after lake update in a project depending on mathlib. The fix is to cp .lake/packages/mathlib/lean-toolchain . and then re-run lake update.

[Mario Carneiro]

(i.e. option 2 suggested by Rob McQueen )

[Gridiron Player]

diff .lake/packages/mathlib/lean-toolchain lean-toolchain
1c1
< leanprover/lean4:v4.10.0-rc1

---

leanprover/lean4:v4.7.0

It seems like that the GameSkeleton is not up to date for lean 4.10-rc1. Not sure if that has anything to do with the syntax error though.
https://github.com/hhu-adam/GameSkeleton/blob/main/lean-toolchain