lake update issue

Stream: lean4

[Patrick Massot]

Trying to run lake update in an old project returns:

lake update
updating lake-packages/mathlib to revision 08334f552c6d6d6d8ae7ea02ac6dd2d88f51e083
error: ./lake-packages/mathlib/lakefile.lean:30:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean:53:2: error: 'weakLeanArgs' is not a field of structure 'Lake.LeanLibConfig'
error: ./lake-packages/mathlib/lakefile.lean: package configuration has errors

It looks like the Lean version of the project is too old to know about weakLeanArgs.

[Patrick Massot]

The project is on nightly-2023-06-20.

[Patrick Massot]

Updating the project lean-toolchain before running lake update will probably fix this, but I wanted to point out this isn't super user-friendly.

[Mac Malone]

@Patrick Massot Yeah, the underlying issue here is that Lake should parse and compare the lean-toolchains of projects and only permit a certain range.

[Patrick Massot]

Well, I didn't want to stay on a version without weakLeanArgs. It sounds like lake missed the point when it should have called the golden instruction cp lake-packages/mathlib/lean-toolchain ..

[Mac Malone]

@Patrick Massot The problem is that Lake itself is too old, so it needs error out and be rerun within a newer lean-toolchain. It could give an informative error about this, though. Technically, it could also copy the new toolchain, but it would need some help from the user to know which package to take the toolchain from (since there could easily be another dependency which needs an even newer toolchain in the general case).

[Kayla Thomas]

I have also been getting this error. I ran elan update and elan default leanprover/lean4:stablebeforehand. I haven't tried to do any updates for a while and was trying to update both Lean and the mathlib in my project. I'm not sure I understand what I need to do to fix it.

[Julian Berman]

@Kayla Thomas does running precisely the 4 steps in this comment work:

https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Updating.20using.20lake.20again/near/393929855

[Kayla Thomas]

@Julian Berman It did. Thank you!

[Kayla Thomas]

Do I need to do anything in addition to that? Did that update mathlib?

[Kayla Thomas]

I guess by reading the comment, it did.