Zulip Chat Archive

Stream: new members

Topic: Updating mathlib broke my cache

Michael Rothgang (Sep 18 2023 at 09:19):

For my project, I temporarily switched to a branch of mathlib --- which has now been deleted, hence git would complain.
I tried to switch to mathlib again, but now my cache is broken. (lake exe cache get) says all files are up to date, but opening VS Code makes it rebuild all of std. How do I fix this? Any help is appreciated.

Michael Rothgang (Sep 18 2023 at 09:19):

Details: project is at https://github.com/fpvandoorn/sard, updating commit is this. Configuration is:



lake manifest

Yaël Dillies (Sep 18 2023 at 09:20):

Have you tried lake exe cache get!?

Michael Rothgang (Sep 18 2023 at 09:20):

I'll be happy to learn how I'm "supposed" to do it --- but AIUI, such documentation hasn't been updated to Lean 4 yet.

Michael Rothgang (Sep 18 2023 at 09:20):

I'm sure I have, trying again just to be sure...

Michael Rothgang (Sep 18 2023 at 09:24):

Nope, doesn't help: when opening VS Code, on the first imports line Lean still says it's building std.

Damiano Testa (Sep 18 2023 at 09:30):

Btw, I can confirm that my usual git pull; lake exe cache get!; lake build yoga is broken now. This is what I get after pulling the current master and running lake exe cache get!; lake build:

info: std: URL has changed; deleting './lake-packages/std' and cloning again
info: cloning https://github.com/leanprover/std4 to ./lake-packages/std
Attempting to download 3767 file(s)
Downloaded: 3767 file(s) [attempted 3767/3767 = 100%] (100% success)
Decompressing 3767 file(s)
unpacked in 9527 ms
[808/3765] Building Mathlib.Data.Stream.Init
[808/3765] Building Mathlib.Algebra.Free
[808/3765] Building Mathlib.Data.List.Card
... etc ...

Kevin Buzzard (Sep 18 2023 at 10:25):

@Michael Rothgang Try lake exe cache clean (or lake exe cache clean! if this is not a syntax error, I forget) and then lake exe cache get!

Michael Rothgang (Sep 18 2023 at 12:07):

Did that, also doesn't help: lake build output starts with

[1/19] Building Std.Tactic.Unreachable
[1/19] Building Std.Lean.TagAttribute
[1/79] Building Std.Lean.Command
[1/79] Building Std.Tactic.OpenPrivate
[2/1546] Building Std.Util.TermUnsafe
[3/1563] Building Std.Tactic.ByCases
[4/1563] Building Std.Tactic.SeqFocus
[5/1563] Building Std.Lean.Name
[6/1563] Building Std.Lean.Position
[7/1563] Building Std.Lean.Parser

Kevin Buzzard (Sep 18 2023 at 18:15):

I am never too worried about building Std, but does it start building mathlib at some point?

Kevin Buzzard (Sep 18 2023 at 18:15):

Std and proofwidgets are quick to build.

Jireh Loreaux (Sep 18 2023 at 23:37):

Kevin, do you mean you never worry about compiling Std? Building is different. And if Std needs building, then Mathlib will too. (Unless somehow only Std oleans are wrong)

Kevin Buzzard (Sep 18 2023 at 23:41):

Oh I've never really understood the difference :-) I just know that sometimes lake build outputs some stuff but finishes quickly

Damiano Testa (Sep 19 2023 at 07:11):

@Michael Rothgang did you solve this issue? For me, this worked:

# in the `mathlib4` dir, on master, but should work also in a branch
# erase files that will be downloaded again later
rm -rf build/
rm -rf lake-packages/

# in case you want the latest current branch
git pull
# remove existing caches, in case they are corrupt
lake exe cache clean!

# with the cache, it also re-downloads what you deleted, takes some time to download the cache
# may build and compile some `Cache` stuff
lake exe cache get

# basically does nothing!
lake build

Kevin Buzzard (Sep 19 2023 at 07:22):

After clean! is there any difference between get and get!?

Damiano Testa (Sep 19 2023 at 07:23):

I do not think so. I think (though I am not sure) that clean! removes all caches, while get! only removes the current one and re-downloads it. I may be wrong.

Michael Rothgang (Sep 19 2023 at 07:56):

@Damiano Testa Thanks for asking. I've found a solution now - but it's different.
When running lake build, building std would always fail after around 600 files. The error (mentioning the occs parameter) pointed towards the solution: my Lean toolchain was too old for the mathlib version. Manually changing the lean-toolchain file to match mathlib fixed it.

Michael Rothgang (Sep 19 2023 at 07:57):

Is there a way to detect and warn about this situation? (I would've expected an error message - perhaps I'm spoiled from Rust :joy: )

Michael Rothgang (Sep 19 2023 at 07:57):

In general, what's the proper way to update the mathlib version my project depends on? Just running lake update mathlib?

Damiano Testa (Sep 19 2023 at 08:03):

Great that you resolved your issue!

Also, I had missed that you had a problem with a project depending on mathlib. I think that my solution only applies to working directly on the Mathlib repo, not on a project.

Last updated: Dec 20 2023 at 11:08 UTC