Mathlib cache not working Windows as of 1 hour ago

Stream: general

[Yongyi Chen]

A fresh Lean project with a mathlib dependency on Windows is demanding to build Mathlib even with the cache downloaded, as of 1 hour ago. This doesn't happen on Linux. Might this have to do with a recent Std bump?

[Yongyi Chen]

For some information, the rebuild starts with ProofWidgets.Compat.

[Mario Carneiro]

Does this actually want to build all of mathlib, or does it stop after building about 10 files from ProofWidgets?

[Yongyi Chen]

On WSL it stops after building 10 files from ProofWidgets but on Windows proper it wants to build all of Mathlib.

[Mario Carneiro]

I think if you jump back and forth between windows and WSL you can end up with the wrong cache files

[Yongyi Chen]

You weren't able to repro it on Windows? I'll check again soon. There was some recent github activity

[Mario Carneiro]

I haven't checked

[Mario Carneiro]

I'm also on linux

[Mario Carneiro]

but the issue with having to rebuild ProofWidgets has come up before, and not just on windows

[Mario Carneiro]

also there is a known issue with bouncing between windows and WSL, this is likely to confuse both lake and cache

[Mario Carneiro]

possibly not in the same way

[Yongyi Chen]

Just checked Windows again -- Cleared %USERPROFILE%\.cache\mathlib and ran lake clean before running lake update -- and it still tries to build Mathlib.

[Utensil Song]

Do you see some output related to lake exe cache get?

[Yongyi Chen]

No, lake exe cache get succeeds normally.

[Utensil Song]

Which Lean toolchain are you on?

[Yongyi Chen]

v4.4.0-rc1

[Utensil Song]

I'll try to reproduce on Windows CI (as I plan to set up one for my projects anyway).

[Sebastien Gouezel]

I can confirm that the cache does not work on master, on my windows. The reason is very likely the following: after downloading cache, mathlib has always been rebuilding proofwidgets for me (on this release and on the previous ones). On the previous ones, nothing depended on proofwidgets, so the rebuilding stopped there. Now, proofwidgets is imported by Tactics.common since #8794, so everything needs to be rebuilt as well.

Until the caching of proofwidgets is sorted out, I will see if reverting #8794 makes cache usable on windows again.

[Sebastien Gouezel]

I can confirm that on the commit just before #8794, lake build only rebuilds proofwidgets, while on the commit just after it rebuilds almost everything.

[Mario Carneiro]

I just double checked and this behavior does not replicate on linux

[Mario Carneiro]

it builds the ProofWidgets files but not mathlib

[Sebastien Gouezel]

I confirm that reverting #8794 solves the caching issues for me: After #8968, the build log is only

PS C:\Users\Sebastien\Desktop\mathlib4> lake build
[1309/3924] Building ProofWidgets.Compat
[3990/4006] Building ProofWidgets.Component.Basic
[3991/4006] Building ProofWidgets.Component.MakeEditLink
[3991/4006] Building ProofWidgets.Data.Html
[3991/4006] Building ProofWidgets.Component.Panel.Basic
[3994/4006] Building ProofWidgets.Presentation.Expr
[3994/4006] Building ProofWidgets.Component.PenroseDiagram
[3994/4006] Building ProofWidgets.Component.OfRpcMethod
[3995/4006] Building Mathlib.Tactic.Widget.SelectPanelUtils
[3997/4006] Building ProofWidgets.Component.Panel.SelectionPanel
[3998/4006] Building Mathlib.Tactic.Widget.CommDiag
[3999/4006] Building Mathlib.Tactic.Widget.Conv
[3999/4006] Building Mathlib.Tactic.Widget.Calc
[3999/4006] Building Mathlib.Tactic.Widget.Gcongr
[3999/4006] Building Mathlib.Tactic.Widget.Congrm
[4004/4006] Building Mathlib.Tactic
[4005/4006] Building Mathlib

while before it it also rebuilds Tactic.Common and everything that imports it.

[Sebastien Gouezel]

It could be a good idea to merge #8968 quickly, as several people have been hit by the issue which makes the last master essentially unusable on windows.

[Scott Morrison]

#8968 is now unneeded, as Mario has killed the bad cache files.

[Scott Morrison]

However, this morning I still needed to run lake exe cache get! to regain a usable cache.

[Yongyi Chen]

Fixed for me too.

[Floris van Doorn]

Current master (8a3329c4d7) is still broken for me. Running lake exe cache get! and lake build builds all of mathlib for me (on Windows).

[Mario Carneiro]

What is the first file that builds?

[Floris van Doorn]

Floris@Dell-E MINGW64 ~/projects/mathlib ((8a3329c4d7...))
$ lb
[106/1003] Building ProofWidgets.Compat
[930/4008] Building ProofWidgets.Component.Basic
[931/4008] Building ProofWidgets.Component.Panel.Basic
[931/4008] Building ProofWidgets.Data.Html
[931/4008] Building ProofWidgets.Component.MakeEditLink
[934/4008] Building ProofWidgets.Component.OfRpcMethod
[934/4008] Building ProofWidgets.Component.PenroseDiagram
[934/4008] Building ProofWidgets.Presentation.Expr
[936/4008] Building Mathlib.Tactic.Widget.SelectPanelUtils
[937/4008] Building ProofWidgets.Component.Panel.SelectionPanel
[939/4008] Building Mathlib.Tactic.Widget.Calc
[939/4008] Building Mathlib.Tactic.Widget.Conv
[939/4008] Building Mathlib.Tactic.Widget.Congrm
[942/4008] Building Mathlib.Tactic.Common
[943/4008] Building Mathlib.Control.Fix
[943/4008] Building Mathlib.Data.Nat.Cast.Field
[943/4008] Building Mathlib.Logic.Pairwise
[943/4008] Building Mathlib.Algebra.Field.IsField
[943/4008] Building Mathlib.Data.Nat.ForSqrt
[943/4008] Building Mathlib.Data.Set.Enumerate
[943/4008] Building Mathlib.CategoryTheory.Category.Basic
[943/4008] Building Mathlib.Algebra.Quotient
[943/4008] Building Mathlib.Data.Countable.Defs
[943/4008] Building Mathlib.Control.Bifunctor
[943/4008] Building Mathlib.Order.Heyting.Boundary
[943/4008] Building Mathlib.Data.TypeVec
[943/4008] Building Mathlib.Control.Monad.Basic
[943/4008] Building Mathlib.Data.Int.Units
[943/4008] Building Mathlib.Data.Set.Pointwise.Basic
[943/4008] Building Mathlib.Data.Nat.MaxPowDiv
[943/4008] Building Mathlib.Data.Set.Intervals.UnorderedInterval
[943/4008] Building Mathlib.Algebra.GCDMonoid.Basic
[943/4008] Building Mathlib.Data.Nat.Factorial.Basic
[943/4008] Building Mathlib.Data.List.Basic
[951/4008] Building Mathlib.Combinatorics.Quiver.Covering
[962/4008] Building Mathlib.Data.Int.Associated
[962/4008] Building Mathlib.Data.Set.Intervals.Pi
[962/4008] Building Mathlib.Data.Int.Order.Units
[962/4008] Building Mathlib.Data.Countable.Small
[962/4008] Building Mathlib.Control.Bitraversable.Basic
[962/4008] Building Mathlib.Logic.Equiv.Functor
[962/4008] Building Mathlib.Control.Monad.Cont
[962/4008] Building Mathlib.Algebra.Ring.Equiv
[962/4008] Building Mathlib.Control.Functor.Multivariate
[962/4008] Building Mathlib.Data.Nat.Sqrt
[962/4008] Building Mathlib.Algebra.Bounds
[962/4008] Building Mathlib.Data.Set.Pointwise.Interval
[962/4008] Building Mathlib.Data.Nat.Choose.Basic
[962/4008] Building Mathlib.Tactic.Positivity.Basic
[962/4008] Building Mathlib.CategoryTheory.Category.RelCat
[962/4008] Building Mathlib.CategoryTheory.Category.KleisliCat
[962/4008] Building Mathlib.CategoryTheory.Functor.Basic
[962/4008] Building Mathlib.Tactic.CategoryTheory.Slice
[963/4008] Building Mathlib.Tactic.Widget.CommDiag
[964/4008] Building Mathlib.Data.Set.Pairwise.Basic
[965/4008] Building Mathlib.Algebra.Group.Pi
[967/4008] Building Mathlib.Algebra.CharZero.Lemmas
[967/4008] Building Mathlib.Data.Array.Lemmas
[968/4008] Building Mathlib.Tactic.Sat.FromLRAT
[969/4008] Building Mathlib.SetTheory.Lists
[970/4008] Building Mathlib.Data.List.Card
[971/4008] Building Mathlib.Data.Array.Basic
[972/4008] Building Mathlib.Data.Bool.AllAny
[973/4008] Building Mathlib.Data.List.Lex
[974/4008] Building Mathlib.Data.Stream.Init
[975/4008] Building Mathlib.Data.List.Palindrome
[976/4008] Building Mathlib.Data.List.MinMax
[977/4008] Building Mathlib.Data.List.Infix
[978/4008] Building Mathlib.Data.List.Lemmas
[979/4008] Building Mathlib.Data.Set.List
[980/4008] Building Mathlib.Algebra.Free
[981/4008] Building Mathlib.Data.String.Lemmas
[982/4008] Building Mathlib.Data.List.TFAE
[983/4008] Building Mathlib.Data.Nat.Bitwise
[984/4008] Building Mathlib.CategoryTheory.Functor.Functorial
[985/4008] Building Mathlib.Data.UnionFind
[986/4008] Building Mathlib.Data.Set.Pairwise.Lattice
[987/4008] Building Mathlib.Control.Bitraversable.Lemmas
[988/4008] Building Mathlib.Tactic.CategoryTheory.Reassoc
[989/4008] Building Mathlib.Data.Set.Intervals.Group
[990/4008] Building Mathlib.Order.Chain
[991/4008] Building Mathlib.Order.Antichain
[992/4008] Building Mathlib.Data.List.DropRight
[993/4008] Building Mathlib.Data.List.Forall2
[994/4008] Building Mathlib.GroupTheory.GroupAction.DomAct.Basic
[995/4008] Building Mathlib.GroupTheory.GroupAction.Pi
[996/4008] Building Mathlib.Algebra.Ring.Pi
[997/4008] Building Mathlib.Tactic.TFAE
[998/4008] Building Mathlib.Data.Pi.Lex
[999/4008] Building Mathlib.GroupTheory.Perm.Basic
[1000/4008] Building Mathlib.Data.Seq.Computation
[1001/4008] Building Mathlib.Control.Bitraversable.Instances
[1002/4008] Building Mathlib.CategoryTheory.Iso
[1003/4008] Building Mathlib.CategoryTheory.NatTrans
[1004/4008] Building Mathlib.Order.Zorn
[1005/4008] Building Mathlib.Data.Set.Intervals.OrdConnected
[1006/4008] Building Mathlib.Data.List.EditDistance.Bounds
[1007/4008] Building Mathlib.Order.OmegaCompletePartialOrder
[1008/4008] Building Mathlib.Data.List.BigOperators.Basic
[1009/4008] Building Mathlib.Data.List.Sections
[1010/4008] Building Mathlib.Data.Int.Bitwise
[1011/4008] Building Mathlib.Control.Traversable.Instances
[1012/4008] Building Mathlib.Data.Fin.Tuple.Basic
[1013/4008] Building Mathlib.Order.Extension.Linear
[1014/4008] Building Mathlib.Order.CompleteLatticeIntervals
[1015/4008] Building Mathlib.Data.Set.Intervals.ProjIcc
[1016/4008] Building Mathlib.Data.Set.Intervals.OrdConnectedComponent
[1017/4008] Building Mathlib.Order.UpperLower.Basic
[1018/4008] Building Mathlib.Order.Cover
[1026/4008] Building Mathlib.Data.List.EditDistance.Estimator
[1026/4008] Building Mathlib.CategoryTheory.Functor.Category
[1026/4008] Building Mathlib.Data.Seq.Seq
[1026/4008] Building Mathlib.Data.DList.Instances
[1026/4008] Building Mathlib.Data.Nat.Choose.Bounds
[1026/4008] Building Mathlib.Data.LazyList.Basic
[1027/4008] Building Mathlib.Algebra.Ring.ULift
[1028/4008] Building Mathlib.Algebra.Ring.CompTypeclasses
[1028/4008] Building Mathlib.Algebra.Ring.Prod
[1028/4008] Building Mathlib.RingTheory.RingInvo
[1029/4008] Building Mathlib.Data.Nat.Choose.Central
[1030/4008] Building Mathlib.Algebra.Order.Hom.Basic
[1031/4008] Building Mathlib.Control.ULiftable
[1032/4008] Building Mathlib.Data.Nat.SqrtNormNum
[1033/4008] Building Mathlib.Data.Int.Sqrt
[1034/4008] Building Mathlib.Tactic.Positivity
[1036/4008] Building Mathlib.Algebra.Order.Field.Power
[1037/4008] Building Mathlib.Algebra.GroupWithZero.Bitwise
[1037/4008] Building Mathlib.Data.Nat.Prime
[1038/4008] Building Mathlib.Tactic.NormNum.NatSqrt
[1039/4008] Building Mathlib.Dynamics.FixedPoints.Basic
[1040/4008] Building Mathlib.Algebra.Group.Aut
[1042/4008] Building Mathlib.Algebra.Order.Nonneg.Ring
[1042/4008] Building Mathlib.Data.Int.Lemmas
[1043/4008] Building Mathlib.GroupTheory.Perm.ViaEmbedding
[1045/4008] Building Mathlib.Data.Nat.Pairing
[1046/4008] Building Mathlib.Control.LawfulFix
[1046/4008] Building Mathlib.Order.CompletePartialOrder
[1047/4008] Building Mathlib.Algebra.Order.Pi
[1048/4008] Building Mathlib.Data.Rat.Sqrt
[1049/4008] Building Mathlib.Algebra.Field.Power

[Mario Carneiro]

and what does lake exe cache lookup ProofWidgets/Compat.lean show?

[Floris van Doorn]

Floris@Dell-E MINGW64 ~/projects/mathlib ((8a3329c4d7...))
$ lake exe cache lookup ProofWidgets/Compat.lean
ProofWidgets\Compat.lean: C:\Users\Floris\.cache\mathlib\64617f0e668c9862.ltar
  comment: git=mathlib4@434896e18f8dd831abd4993280b34343729c9c49

[Mario Carneiro]

looks like exactly the same thing happened again

[Mario Carneiro]

@Floris van Doorn the cache should be fixed, try running lake exe cache get! again

[Mario Carneiro]

@Scott Morrison help! Was this commit from you or a scott bot?

[Scott Morrison]

This commit was from me.

[Scott Morrison]

(I think all bots have their own names these days.)