cache rebuilding oleans

Stream: mathlib4

[Michael Stoll]

I've noticed that since a few days or so, the "build Mathlib" step in CI first builds ProofWidgets after every push even though no changes have been made to it. Is this by design or a bug?

[Yaël Dillies]

I've noticed the same thing when getting cache. I seem to need to build ProofWidgets every time

[Michael Stoll]

Here is the log from the latest CI run for one of my PRs:

Run liskin/gh-problem-matcher-wrap@v3
/usr/bin/bash -o pipefail -c env LEAN_ABORT_ON_PANIC=1 lake build --wfail -KCI
✔ [941/5439] Built ProofWidgets.Compat
✔ [942/5439] Built ProofWidgets.Util
✔ [943/5439] Built ProofWidgets.Component.Basic
✔ [944/5439] Built ProofWidgets.Cancellable
✔ [945/5439] Built ProofWidgets.Component.MakeEditLink
✔ [946/5439] Built ProofWidgets.Component.Panel.Basic
✔ [947/5439] Built ProofWidgets.Data.Html
✔ [948/5439] Built ProofWidgets.Component.HtmlDisplay
✔ [949/5439] Built ProofWidgets.Component.OfRpcMethod
✔ [5365/5439] Built ProofWidgets.Component.PenroseDiagram
✔ [5366/5439] Built ProofWidgets.Presentation.Expr
✔ [5437/5439] Built Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnityInstances
✔ [5438/5439] Built Mathlib
Build completed successfully.

[Kim Morrison]

It's not meant to be like this. :-(

[Kim Morrison]

@Mac Malone, could this be connected to the exit code 3 failures from lake build --no-build that we're seeing on nightly-testing?

[Floris van Doorn]

After upgrading to the latest Mathlib, I have to manually rebuild ProofWidgets after getting the cache:

Floris@Dell-E MINGW64 ~/projects/mathlibc ((efb737da256...))
$ lc
info: batteries: updating repository '.\.\.lake/packages\batteries' to revision 'af731107d531b39cd7278c73f91c573f40340612'
info: Qq: updating repository '.\.\.lake/packages\Qq' to revision '303b23fbcea94ac4f96e590c1cad6618fd4f5f41'
info: aesop: updating repository '.\.\.lake/packages\aesop' to revision '5dfdc66e0d503631527ad90c1b5d7815c86a8662'
info: proofwidgets: updating repository '.\.\.lake/packages\proofwidgets' to revision '1383e72b40dd62a566896a6e348ffe868801b172'
info: importGraph: URL has changed; you might need to delete '.\.\.lake/packages\importGraph' manually
info: importGraph: updating repository '.\.\.lake/packages\importGraph' to revision 'ac7b989cbf99169509433124ae484318e953d201'
info: LeanSearchClient: updating repository '.\.\.lake/packages\LeanSearchClient' to revision '86d0d0584f5cd165353e2f8a30c455cd0e168ac2'
info: plausible: cloning https://github.com/leanprover-community/plausible to '.\.\.lake/packages\plausible'
info: Cli: updating repository '.\.\.lake/packages\Cli' to revision '726b3c9ad13acca724d4651f14afc4804a7b0e4d'
✔ [2/10] Built Cache.IO
✔ [3/10] Built Cache.Hashing
✔ [4/10] Built Cache.Requests
✔ [5/10] Built Cache.Hashing:c.o
✔ [6/10] Built Cache.Main
✔ [7/10] Built Cache.Requests:c.o
✔ [8/10] Built Cache.IO:c.o
✔ [9/10] Built Cache.Main:c.o
✔ [10/10] Built cache
Attempting to download 4354 file(s)
Downloaded: 4354 file(s) [attempted 4354/4354 = 100%] (100% success)
Decompressing 5434 file(s)
Unpacked in 35279 ms
Completed successfully!

Floris@Dell-E MINGW64 ~/projects/mathlibc ((efb737da256...))
$ lb
✔ [941/5446] Built ProofWidgets.Compat
✔ [942/5446] Built ProofWidgets.Util
✔ [943/5446] Built ProofWidgets.Component.Basic
✔ [944/5446] Built ProofWidgets.Cancellable
✔ [945/5446] Built ProofWidgets.Component.MakeEditLink
✔ [946/5446] Built ProofWidgets.Data.Html
✔ [947/5446] Built ProofWidgets.Component.Panel.Basic
✔ [948/5446] Built ProofWidgets.Presentation.Expr
✔ [949/5446] Built ProofWidgets.Component.HtmlDisplay
✔ [950/5446] Built ProofWidgets.Component.OfRpcMethod
✔ [1259/5446] Built ProofWidgets.Component.PenroseDiagram
Build completed successfully.

(lc = lake exe cache get and lb = lake build). This is on Windows.

[Michael Stoll]

See also here.

[Kim Morrison]

@Mac Malone, sorry to bother you, but could you expand on what the +1 means? Is this something that you're fixing / you already understand / others need to be working on too?

[Mac Malone]

@Kim Morrison No worries! (Feel free to bother me. :smile_cat:). By :thumbs_up:, it seems quite possible and will invesitgate it (which I am currently doing now).

[Notification Bot]

2 messages were moved here from #mathlib4 > rebuild ProofWidgets by Ruben Van de Velde.

[Mac Malone]

@Kim Morrison Sorry for a somewhat slow reply, I was otherwise distracted. I have discovered a few problems here.

The first problem is that the oleans for ProofWidgets in the mathlib cache appear to be corrupt (they cause a rebuild). This seems like it could be reason check the cache is failing on nightly-testing as well. That is, the the --no-build failure is not a false positive and the wrong oleans are somehow being uploaded. Perhaps someone more familiar with cache can identify likely reasons for this? If not, I can try to investigate further.

The second problem is that lake exe cache get does not fetch the ProofWidgets cloud release before fetching the cache, thus the cloud release overwrites the cache. This is a by-product of lean4#5641, as lake exe cache no longer fetches the ProofWidgets cloud release as cache does nto depend on it. One possible solution is to include the ProofWidget js in the Mahtlib cache. Another is to have lake exe cache invoke lake build proofwidgets:release before clobbering the cloud release's oleans with the mathlib cache's.

[Sebastian Ullrich]

Is there even any reason to store ProofWidgets .oleans in the Mathlib cache?

[Ruben Van de Velde]

If you don't, you always get the warning "dependencies out of date" when you open a file in vscode, right?

[Damiano Testa]

I also do not know how to reproduce this, nor if it is actually the same issue, but I just pulled the current master and tried downloading the cache, but then lake build was still building. So, I tried this:

$ rm -i -rf .lake/build/lib/Mathlib/*

$ lake exe cache get
No files to download
Decompressing 5483 file(s)
Unpacked in 12424 ms
Completed successfully!

$ lake build
⣿ [?/?] Computing build jobs
⣟ [955/5495] Running Mathlib.Tactic.MinImports (+ 0 more)
⡿ [956/5495] Running Mathlib.Tactic.Linter.MinImports (+ 0 more)
⣻ [957/5495] Running Mathlib.Tactic.Linter (+ 0 more)
⣽ [958/5495] Running Mathlib.Tactic.Common (+ 0 more)
⢿ [959/5495] Running Mathlib.Order.Interval.Set.UnorderedInterval (+ 3 more)
⣽ [959/5495] Running Mathlib.Order.Interval.Set.UnorderedInterval (+ 3 more)^C

[Notification Bot]

A message was moved here from #mathlib4 > cache rebuilding proofwidgets JS by Sebastian Ullrich.

[Sebastian Ullrich]

Sebastian Ullrich said:

Is there even any reason to store ProofWidgets .oleans in the Mathlib cache?

@Kim Morrison @Mac Malone Do you see any downsides of relying on the GitHub/Reservoir cache for all Mathlib dependencies? Caching them in two different systems fighting each other does seem problematic to me. I suppose it slightly increases the latency between dependency release and corresponding Mathlib bump because Reservoir has to run in between.

[Kim Morrison]

It's pretty important to me that an olean cache is available on nightly-testing and lean-pr-testing-NNNN branches, which very often depend on corresponding branches of upstream repositories.

[Kim Morrison]

I suspect that Reservoir can't support that use case yet?

[Kim Morrison]

@Mac Malone, a heads up that we are getting exit code 3 again from lake build --no-build, and this is preventing essential PRs from being merged.

[Kim Morrison]

See for example https://github.com/leanprover-community/mathlib4/actions/runs/12026201798/job/33524709775?pr=19487

[Kim Morrison]

Can someone confirm for me that this is reproducible locally as:

git clone https://github.com/leanprover-community/mathlib4.git
cd mathlib4
git checkout fb766983b642b3588158800b4ee8e3cca235a198
lake exe cache get
lake build --no-build
echo $?

which for me reports an exit code of 3.

[Kim Morrison]

@Mac Malone, could you please treat this as a critical issue? This preventing us merging essential PRs to Mathlib. If we need to cut an rc to get a fix, let's do it.

[Johan Commelin]

I confirm that I also get 3.

[Damiano Testa]

Same here: everything appears to work, but the final exit code is 3.

[Mac Malone]

@Kim Morrison I tested commit fb766983b642b3588158800b4ee8e3cca235a198 and as far as I can tell the cache is simply corrupt. After a lake exe cache get! (which afaik should clobber any Lake-produced cache files), Lake is building multiple dependency files (including those from Plausible and Aesop). Thus, I can only infer that the cached oleans are bad.

[Kim Morrison]

Just quoting a conversation elsewhere for anyone wondering about the conclusion here:

---

Mac Malone: Using Sebastian's info, I think I have found the source of the problem. A lake exe cache lookup Plausible/Gen.lean revealed that the commit which pushed the bad olean was 5b40b8f. The CI for the job was cancelled mid-build, but it still uploaded a cache. Since mathlib was unable to build the proper oleans for batteries, the ones from the Reservoir cache were uploaded instead.

Sebastian Ullrich: Oh that's nefarious. But uploading partial builds is important for Mathlib afaiu. What solution do you suggest?

Mac Malone: Since this is a critical blocker, I think the simplest solution is best at the moment. As such, disabling Lake's cache in the mathlib CI seems the route to go.

Mac Malone: It does not appear there is a way to reconcile Mathlib's / Cache's requirements for the Lake directory with Lake's here without some significant new features / refactoring.

Mac Malone: PR with fixes: mathlib4#19524.

[Edward van de Meent]

Kim Morrison said:

The CI for the job was cancelled mid-build, but it still uploaded a cache. Since mathlib was unable to build the proper oleans for batteries, the ones from the Reservoir cache were uploaded instead.

is there some part in the process here where distinguishing between "complete build" oleans and "partial build" oleans would allow some kind of CI warning at least? something along the lines of "the cache has only a partially compiled project, so let's build it again ourselves and hope things work out better?"

[Edward van de Meent]

i might be misunderstanding what's going on here, so please ignore if my question doesn't make sense