Updating mathlib broke my cache

Stream: new members

[Michael Rothgang]

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]

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

toolchain

cat lean-toolchain
leanprover/lean4:v4.0.0-rc4

lakefile

cat lakefile.lean
import Lake
open Lake DSL

package «sard» {
-- add any package configuration options here
}

require mathlib from git
"https://github.com/leanprover-community/mathlib4.git"

@[default_target]
lean_lib «Sard» {
-- add any library configuration options here
}

lake manifest

$ cat lake-manifest.json
{"version": 5,
"packagesDir": "lake-packages",
"packages":
[{"git":
{"url": "https://github.com/EdAyers/ProofWidgets4",
"subDir?": null,
"rev": "44e6673a20fc0449d003983d1e1f472df40f7107",
"opts": {},
"name": "proofwidgets",
"inputRev?": "v0.0.15",
"inherited": true}},
{"git":
{"url": "https://github.com/mhuisi/lean4-cli.git",
"subDir?": null,
"rev": "21dac2e9cc7e3cf7da5800814787b833e680b2fd",
"opts": {},
"name": "Cli",
"inputRev?": "nightly",
"inherited": true}},
{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
"rev": "e70f8800f70f89b102ad7469128ace674213e1e5",
"opts": {},
"name": "mathlib",
"inputRev?": null,
"inherited": false}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
"rev": "e75daed95ad1c92af4e577fea95e234d7a8401c1",
"opts": {},
"name": "Qq",
"inputRev?": "master",
"inherited": true}},
{"git":
{"url": "https://github.com/JLimperg/aesop",
"subDir?": null,
"rev": "1a0cded2be292b5496e659b730d2accc742de098",
"opts": {},
"name": "aesop",
"inputRev?": "master",
"inherited": true}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
"rev": "524aae5c8000f6e38433ee0ad95bdae3cfa88fee",
"opts": {},
"name": "std",
"inputRev?": "main",
"inherited": true}}]}

[Yaël Dillies]

Have you tried lake exe cache get!?

[Michael Rothgang]

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]

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

[Michael Rothgang]

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

[Damiano Testa]

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]

@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]

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]

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

[Kevin Buzzard]

Std and proofwidgets are quick to build.

[Jireh Loreaux]

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]

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

[Damiano Testa]

@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]

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

[Damiano Testa]

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]

@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]

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]

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

[Damiano Testa]

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.