Bug: Why does GitHub workflow build Mathlib?

[AtticusKuhn]

Take a look at the GitHub workflow logs, for example,
https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867

Here is an excerpt of the output:

9m 11s
Run lake -R exe cache get # download cache of mathlib docs.
info: mathlib: cloning https://github.com/leanprover-community/mathlib4 to '././.lake/packages/mathlib'
info: Cli: cloning https://github.com/mhuisi/lean4-cli.git to '././.lake/packages/Cli'
info: doc-gen4: cloning https://github.com/leanprover/doc-gen4 to '././.lake/packages/doc-gen4'
info: LeanSAT: cloning https://github.com/leanprover/leansat.git to '././.lake/packages/LeanSAT'
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: MD4Lean: cloning https://github.com/acmepjz/md4lean to '././.lake/packages/MD4Lean'
warning: ././.lake/packages/MD4Lean/lakefile.lean:[1](https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867#step:4:1)4:18: warning: `Lake.inputFile` has been deprecated
warning: ././.lake/packages/MD4Lean/lakefile.lean:27:18: warning: `Lake.inputFile` has been deprecated
info: BibtexQuery: cloning https://github.com/dupuisf/BibtexQuery to '././.lake/packages/BibtexQuery'
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic to '././.lake/packages/UnicodeBasic'
✔ [6/17] (Optional) Fetched proofwidgets:optRelease
✔ [9/17] Built Cache.IO
✔ [10/17] Built Cache.Hashing
✔ [11/17] Built Cache.Requests
✔ [12/17] Built Cache.Hashing:c.o
✔ [13/17] Built Cache.Main
✔ [14/17] Built Cache.Requests:c.o
✔ [1[5](https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867#step:4:6)/17] Built Cache.IO:c.o
✔ [16/17] Built Cache.Main:c.o
✔ [17/17] Built cache
  % Total    % Received % Xferd  Average Speed   Time    Time     Time  Current
                                 Dload  Upload   Total   Spent    Left  Speed

  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0
  0     0    0     0    0     0      0      0 --:--:-- --:--:-- --:--:--     0

100 1054k  100 1054k    0     0  3[6](https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867#step:4:7)55k      0 --:--:-- --:--:-- --:--:-- 3655k

installing leantar 0.1.13
Attempting to download 4866 file(s)

Downloaded: 1 file(s) [attempted 1/4866 = 0%]
Downloaded: 243 file(s) [attempted 243/4866 = 4%]
Downloaded: 519 file(s) [attempted 519/4866 = 10%]
Downloaded: 806 file(s) [attempted 806/4866 = 16%]
Downloaded: 1082 file(s) [attempted 1082/4866 = 22%]
Downloaded: 1356 file(s) [attempted 1356/4866 = 2[7](https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867#step:4:8)%]
Downloaded: 1638 file(s) [attempted 1638/4866 = 33%]
Downloaded: 1904 file(s) [attempted 1904/4[8](https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867#step:4:9)66 = 39%]
Downloaded: 2148 file(s) [attempted 2148/4866 = 44%]
Downloaded: 2388 file(s) [attempted 2388/4866 = 4[9](https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867#step:4:10)%]
Downloaded: 2659 file(s) [attempted 2659/4866 = 54%]
Downloaded: 2929 file(s) [attempted 2929/4866 = 60%]
Downloaded: 3208 file(s) [attempted 3208/4866 = 65%]
Downloaded: 3484 file(s) [attempted 3484/4866 = 71%]
Downloaded: 3757 file(s) [attempted 3757/4866 = 77%]
Downloaded: 4044 file(s) [attempted 4044/4866 = 83%]
Downloaded: 4313 file(s) [attempted 4313/4866 = 88%]
Downloaded: 4591 file(s) [attempted 4591/4866 = 94%]
Downloaded: 4855 file(s) [attempted 4855/4866 = 99%]
Downloaded: 4866 file(s) [attempted 4866/4866 = [10](https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867#step:4:11)0%] (100% success)
Decompressing 4866 file(s)
Unpacked in [11](https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867#step:4:12)074 ms
Completed successfully!
warning: ././.lake/packages/MD4Lean/lakefile.lean:14:18: warning: `Lake.inputFile` has been deprecated
warning: ././.lake/packages/MD4Lean/lakefile.lean:27:18: warning: `Lake.inputFile` has been deprecated
✔ [510/4643] Built SSA.Core.Util.ConcreteOrMVar
✔ [530/4643] Built SSA.Core.HVector
✔ [532/4643] Built SSA.Core.Framework.Dialect
✔ [534/4643] Built SSA.Projects.InstCombine.LLVM.SimpSet
✔ [535/4643] Built Batteries.Control.Lemmas
✔ [536/4643] Built SSA.Projects.InstCombine.ForStd
✔ [539/4643] Built Batteries.Data.BinaryHeap
✔ [540/4643] Built Batteries.Lean.Delaborator
✔ [541/4643] Built Batteries.Lean.IO.Process
✔ [542/4643] Built Batteries.Lean.HashMap
✔ [543/4643] Built Batteries.Tactic.Instances
✔ [544/4643] Built Batteries.Tactic.NoMatch
✔ [545/4643] Built Batteries.Test.Internal.DummyLabelAttr
✔ [546/4643] Built SSA.Core.EffectKind
✔ [560/4643] Built Batteries.Util.Pickle
✔ [561/4643] Built Batteries.Data.BitVec.Lemmas
✔ [562/4643] Built SSA.Core.MLIRSyntax.Transform.NameMapping
✔ [564/4643] Built Batteries.Classes.Cast
✔ [566/4643] Built Batteries.Tactic.Case
✔ [567/4643] Built Batteries.Data.BinomialHeap.Lemmas
✔ [568/4643] Built Batteries.Data.Bool
✔ [569/4643] Built Batteries.Lean.System.IO
✔ [570/4643] Built Batteries.Data.Option.Lemmas
✔ [571/4643] Built Batteries.Lean.Json
✔ [572/46[43](https://github.com/opencompl/lean-mlir/actions/runs/10177448324/job/28148970867#step:4:44)] Built Batteries.Data.RBMap.Depth
✔ [573/4643] Built Cli.Basic
✔ [574/4643] Built Batteries.Lean.Util.EnvSearch

As you can see, it seems that lake is building "Batteries". Later on, it also builds "Aesop" and "Mathlib". I believe that this slows down the GitHub workflow significantly. I also believe that this is a bug, as Lean should not be building these files, but instead getting them from the cache.

[AtticusKuhn]

I have one theory, which is maybe we should use

lake exe cache get!

instead of

lake exe cache get

[AtticusKuhn]

By the way, "Compile mlirnatural Executable 🧐" takes up 58% of the total runtime of the github workflow, so this could possibly speed up the GitHub workflow significantly.

[tobiasgrosser]

Right, the same is true for our builds. In some way the cache does not work as expected. I often see on my laptop more recompiling as needed. It might be worth debugging this. Part of the reason for this might be supportInterpreter = true in the lakefile.toml.