Updating mathlib4: "No such file aesop/lakefile.lean"

Stream: new members

[Martin C. Martin]

I'm trying to update my mathlib4 using these instructions, you can see my lakefile and friends here. lake update gives the following error:

mathlib: updating repository './lake-packages/mathlib' to revision 'bf077b111ca30b6793deafddf07fd8949cb92a3a'
std: updating repository './lake-packages/std' to revision 'fb56324020c8e4f3d451e8901b290dea82c072ae'
Qq: URL has changed; deleting './lake-packages/Qq' and cloning again
cloning https://github.com/leanprover-community/quote4 to ./lake-packages/Qq
cloning https://github.com/leanprover-community/aesop to ./lake-packages/aesop
Cli: URL has changed; deleting './lake-packages/Cli' and cloning again
cloning https://github.com/leanprover/lean4-cli to ./lake-packages/Cli
proofwidgets: URL has changed; deleting './lake-packages/proofwidgets' and cloning again
cloning https://github.com/leanprover-community/ProofWidgets4 to ./lake-packages/proofwidgets
error: no such file or directory (error code: 2)
  file: ./lake-packages/aesop/lakefile.lean

How can I fix this? Should I just blow away my project and start over? It's currently a single source file (outside of mathlib4) so that would be easy enough.

[Gareth Ma]

Try removing lake-packages and run lake exe cache get

[Gareth Ma]

Also use a newer version of Lean by updating your lean-toolchain file. You can see the version that Mathlib uses here, which is leanprover/lean4:v4.2.0-rc4 currently.

[Martin C. Martin]

That worked, thanks!

[Adomas Baliuka]

I've read several times on Zulip that using lake update (with nothing after) is discouraged and I've broken projects doing this before. So I'm quite surprised to find it recommended in the linked page above. What am I missing?

[Ruben Van de Velde]

I think that page is written assuming mathlib is your only dependency

[Ruben Van de Velde]

If you run lake update mathlib, does that catch any updates to mathlib's version of std4 (for example) too?

[Yaël Dillies]

It used to be discouraged, but hasn't been for the past month.

[Martin C. Martin]

So discouraging people from using lake update is now discouraged?

[Yaël Dillies]

I would discourage you from framing it like that, but yes :upside_down:

[Kevin Buzzard]

To put it less confusingly, it now works much better :-)