lake exe cache get after lake build

Stream: lean4

[Floris van Doorn]

Sometimes I run lake build accidentally and it starts building Mathlib + prerequisites. If I then run lake exe cache get, this cache is not actually usable. Only lake exe cache get! will get me a working cache.

• Is this the same on Linux?
• Why does this happen / is this fixable?

Here is an example shell session displaying this (the first two occurrences of lake build are interrupted):

Floris@Dell-E MINGW64 ~/projects/mathlib ((c138fdc9e6e...))
$ git checkout origin/master
Updating files: 100% (2947/2947), done.
Previous HEAD position was c138fdc9e6e chore: no need to pass autoParam to simp or dsimp (#15968)
HEAD is now at 4591e55bbcc feat(CategoryTheory): simps for `conjugateEquiv` plus computable `conjugateIsoEquiv` (#17108)

Floris@Dell-E MINGW64 ~/projects/mathlib ((4591e55bbcc...))
$ lake build
info: batteries: updating repository '.\.\.lake/packages\batteries' to revision '6d5e1c81277e960372c94f19172440e39b3c5980'
info: Qq: updating repository '.\.\.lake/packages\Qq' to revision '2c8ae451ce9ffc83554322b14437159c1a9703f9'
info: aesop: updating repository '.\.\.lake/packages\aesop' to revision 'a895713f7701e295a015b1087f3113fd3d615272'
info: proofwidgets: updating repository '.\.\.lake/packages\proofwidgets' to revision 'eb08eee94098fe530ccd6d8751a86fe405473d4c'
info: importGraph: URL has changed; you might need to delete '.\.\.lake/packages\importGraph' manually
info: importGraph: updating repository '.\.\.lake/packages\importGraph' to revision 'fb7841a6f4fb389ec0e47dd4677844d49906af3c'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '.\.\.lake/packages\LeanSearchClient'
✔ [4/5125] (Optional) Fetched proofwidgets:optRelease
✔ [8/5125] Built Batteries.Lean.HashSet
✔ [9/5125] Built Batteries.Tactic.Lint.Basic
✔ [10/5125] Built Batteries.Tactic.OpenPrivate
✔ [11/5125] Built Batteries.Util.LibraryNote
✔ [12/5125] Built Batteries.Tactic.Lint.TypeClass
✔ [13/5125] Built Batteries.Tactic.Unreachable
✔ [14/5125] Built Batteries.CodeAction.Attr
✔ [15/5125] Built Batteries.Lean.Position
✔ [16/5125] Built Batteries.Lean.NameMapAttribute
✔ [17/5125] Built Batteries.Lean.Expr
✔ [18/5125] Built Batteries.Data.Nat.Gcd
✔ [19/5125] Built Batteries.Lean.Float
✔ [20/5125] Built Batteries.Data.Rat.Basic
✔ [21/5125] Built Batteries.Data.String.Basic
✔ [22/5125] Built Batteries.Tactic.SeqFocus
✔ [23/5125] Built Batteries.Util.ExtendedBinder
✔ [24/5125] Built Batteries.Tactic.Init
✔ [25/5125] Built Batteries.Data.Sum.Basic
✔ [26/5125] Built Batteries.Tactic.Classical
✔ [27/5125] Built Batteries.Linter.UnreachableTactic
✔ [28/5125] Built Batteries.Lean.Syntax
✔ [29/5125] Built Aesop.Check
✔ [30/5125] Built Aesop.Nanos
✔ [31/5125] Built Batteries.Data.Array.Init.Lemmas
✔ [32/5125] Built Batteries.Data.Array.Basic
✔ [33/5125] Built Aesop.Rule.Name
✔ [34/5125] Built Aesop.Percent
✔ [35/5125] Built Batteries.Lean.Meta.Basic
✔ [36/5125] Built Batteries.Lean.MonadBacktrack
✔ [37/5125] Built Batteries.Data.List.Init.Lemmas
✔ [38/5125] Built Batteries.Lean.PersistentHashSet
✔ [39/5125] Built Batteries.Lean.Meta.Expr
✔ [40/5125] Built Batteries.Lean.PersistentHashMap
✔ [41/5125] Built Batteries.Lean.Meta.Inaccessible
✔ [42/5125] Built Batteries.Lean.Meta.UnusedNames
✔ [43/5125] Built Batteries.Lean.Meta.AssertHypotheses
✔ [44/5125] Built Aesop.Search.Expansion.Simp
✔ [45/5125] Built Aesop.Constants
✔ [46/5125] Built Batteries.Control.ForInStep.Basic
✔ [47/5125] Built Batteries.Lean.TagAttribute
✔ [48/5125] Built Batteries.Util.ProofWanted
✔ [49/5125] Built Batteries.Lean.Except
✔ [51/5125] Built Batteries.Tactic.Exact
✔ [52/5125] Built Batteries.WF
✔ [53/5125] Built Batteries.Classes.Order
✔ [54/5125] Built Batteries.CodeAction.Basic
✔ [55/5125] Built Batteries.Tactic.Lint.Misc
✔ [56/5125] Built Qq.SortLocalDecls
✔ [57/5125] Built Batteries.Lean.Meta.Clear
✔ [58/5125] Built Aesop.RuleSet.Name
✔ [60/5125] Built Aesop.Script.Tactic
✔ [61/5125] Built Aesop.Script.GoalWithMVars
✔ [62/5125] Built Aesop.ElabM
✔ [63/5125] Built Aesop.Util.Tactic
✔ [64/5125] Built Aesop.Frontend.Basic
✔ [65/5125] Built Aesop.Exception
✔ [66/5125] Built Qq.ForLean.ToExpr
✔ [67/5125] Built Qq.Typ
✔ [68/5125] Built Qq.ForLean.Do
✔ [69/5125] Built Batteries.Lean.Meta.InstantiateMVars
✔ [70/5125] Built Aesop.RuleTac.FVarIdSubst
✔ [71/5125] Built Aesop.Script.OptimizeSyntax
✔ [72/5125] Built Aesop.Util.UnionFind
✔ [73/5125] Built Qq.ForLean.ReduceEval
✔ [74/5125] Built Batteries.Lean.NameMap
✔ [76/5125] Built Aesop.Options.Public
✔ [77/5125] Built Batteries.Lean.Meta.SavedState
✔ [78/5125] Built Batteries.Data.Nat.Basic
✔ [79/5125] Built Batteries.Data.Array.Match
✔ [80/5125] Built LeanSearchClient.Basic
✔ [81/5125] Built Batteries.Tactic.Congr
✔ [82/5125] Built Batteries.Data.Fin.Basic
✔ [83/5125] Built Batteries.Tactic.Lint.Frontend
✔ [84/5125] Built Batteries.Control.Lemmas
✔ [85/5125] Built Batteries.Util.Cache
✔ [86/5125] Built Batteries.Lean.HashMap
✔ [87/5125] Built Batteries.Data.FloatArray
✔ [88/5125] Built Batteries.Lean.System.IO


Floris@Dell-E MINGW64 ~/projects/mathlib ((4591e55bbcc...))
$ lake exe cache get
✔ [10/18] Built Cache.IO
✔ [11/18] Built Cache.Hashing
✔ [12/18] Built Cache.Requests
✔ [13/18] Built Cache.Hashing:c.o
✔ [14/18] Built Cache.Main
✔ [15/18] Built Cache.Requests:c.o
✔ [16/18] Built Cache.Main:c.o
✔ [17/18] Built Cache.IO:c.o
✔ [18/18] Built cache
Attempting to download 5113 file(s)
Downloaded: 5113 file(s) [attempted 5113/5113 = 100%] (100% success)
Decompressing 5113 file(s)
Unpacked in 42377 ms
Completed successfully!

Floris@Dell-E MINGW64 ~/projects/mathlib ((4591e55bbcc...))
$ lake build
✔ [726/5125] Built Qq.Macro
✔ [727/5125] Built Mathlib.Tactic.Eval
✔ [728/5125] Built Qq.Delab
✔ [729/5125] Built Qq.MetaM
✔ [730/5125] Built Mathlib.Tactic.Nontriviality.Core
✔ [731/5125] Built Mathlib.Tactic.Nontriviality


Floris@Dell-E MINGW64 ~/projects/mathlib ((4591e55bbcc...))
$ lake exe cache get!
Attempting to download 5113 file(s)
Downloaded: 5113 file(s) [attempted 5113/5113 = 100%] (100% success)
Decompressing 5113 file(s)
Unpacked in 45896 ms
Completed successfully!

Floris@Dell-E MINGW64 ~/projects/mathlib ((4591e55bbcc...))
$ lake build
Build completed successfully.

[Damiano Testa]

I have observed this also on Linux: sometimes, lake exe cache get; lake build does actually build from somewhere. Usually, removing the cache and redownloading fixes it.

[Damiano Testa]

I usually assume that the reason is that some oleans got corrupted in the download...

[Floris van Doorn]

I think it's the interaction between the built oleans and the downloaded ones. I consistently have this problem after a partial lake build, but almost never without it.

[Daniel Weber]

I also observed this, usually what I do is checkout to master, git pull, download the cache, checkout back to the branch and merge master and that usually fixes it

[Floris van Doorn]

Or maybe interrupting a lake build creates a corrupted .olean file that lake exe cache get recognizes as "correct", so doesn't replace it?

[Damiano Testa]

I never got to the bottom of it, but since removing the old cache and re-downloading is almost always successful, I never investigated it further.

[Arthur Paulino]

Is this consistent? I mean, does it happen everytime you interrupt lake build?

Edit: I just read that you mentioned that you consistently have this issue after a partial lake build

[Arthur Paulino]

I think it's unlikely that you're getting corrupted olean files because that would require you to interrupt the process while writing the file to your file system. And the bottleneck of lake build shouldn't be there.

I'm not saying it's impossible, but it wouldn't be my first line of investigation. Especially given that this behavior is consistent.

[Floris van Doorn]

Yes, I've had this many times, and I think it's consistent. The place where the build continues after lake exe cache get seems random-ish. Please reproduce my above steps to see whether it also consistently happens for you.

[Sebastian Ullrich]

I can't reproduce on Linux in 1/1 tries

$ lake build
info: batteries: updating repository '././.lake/packages/batteries' to revision '6d5e1c81277e960372c94f19172440e39b3c5980'
info: aesop: updating repository '././.lake/packages/aesop' to revision 'a895713f7701e295a015b1087f3113fd3d615272'
info: importGraph: updating repository '././.lake/packages/importGraph' to revision 'fb7841a6f4fb389ec0e47dd4677844d49906af3c'
info: LeanSearchClient: updating repository '././.lake/packages/LeanSearchClient' to revision '2ba60fa2c384a94735454db11a2d523612eaabff'
⡿ [192/5127] Running Mathlib.Tactic.Linter.Lint (+ 9 more)^C
 ✘ $ time lake exe cache get
Attempting to download 5115 file(s)
Downloaded: 5115 file(s) [attempted 5115/5115 = 100%] (100% success)
Decompressing 5115 file(s)
Unpacked in 3262 ms
Completed successfully!
lake exe cache get  26.45s user 15.05s system 127% cpu 32.548 total
$ lake build
Build completed successfully.

Could you try running diff -r on a broken and working copy of .lake?

[Floris van Doorn]

On two copies of Mathlib that I've both been using for a few years, this produces 30+MB of output (and counting). Not sure how much that is old files that are not being cleaned up. Shall I send it, or shall I create 2 fresh clones of Mathlib and do the diff?

[Sebastian Ullrich]

Ah, this could be due to history in all the .gits and other "orphan" files. Two fresh clones would be best I'd say.

[Floris van Doorn]

Here is the output (and the precise commands used to produce this output):
https://gist.github.com/fpvandoorn/a4599b27d2b632c435cd66e409236f19

[Floris van Doorn]

It seems that a bunch of hashes are different.

[Kevin Buzzard]

(My 2c is that I use Linux and I've not seen problems of this nature for quite some time)

[Sebastian Ullrich]

Floris van Doorn said:

It seems that a bunch of hashes are different.

Thanks, and indeed one of the files is notable in containing e.g. 2^64 which points to lean#5144

[Filippo A. E. Nuccio]

I actually get a similar problem when I work on mathlib PR's. If I download the cache for one, finish working on it, and then switch and download it for the other, high chances (not 100%, something between 90% and 95%) are that I need a lake exe cache get! to start working on the second one. Is this related?

[Kevin Buzzard]

I've never seen this (I mean, recently) and I do this sort of thing too. Are you on Windows? I'm on Ubuntu.

[Filippo A. E. Nuccio]

Yes, on Win.