ImperialCollegeLondon/FLT cache

Stream: FLT

[Kevin Buzzard]

After a lake exe cache get I got

info: mathlib: checking out revision '401dce0e8e36a1011330773466b2c6c1b3683a29'
info: batteries: checking out revision '795ab4977cc1b41273258b736585b9b3def9081c'
Project repository: ImperialCollegeLondon/FLT
Attempting to download 6748 file(s) from ImperialCollegeLondon/FLT cache
Downloaded: 0 file(s) [attempted 6748/6748 = 100%] (0% success)
Attempting to download 6748 file(s) from leanprover-community/mathlib4 cache
Downloaded: 6748 file(s) [attempted 6748/6748 = 100%] (100% success)
Decompressing 6748 file(s)

What is this development, and will it one day save me from having to build FLT locally on every device after a mathlib bump?

I find that most of my time nowadays is spent on "feature branches", where I spend several days working on a part of the project in a WIP PR, then when everything is ready I change the PR from WIP, check the diffs to make sure nothing weird happened and then merge after CI is working. Is there also a possibility that I won't have to build FLT locally on every device when switching machines in such a workflow?

[Yaël Dillies]

See #mathlib4 > `lake update` now slowly tries to download repository cache

[Kim Morrison]

Yes, I'm not sure exactly what the timeline yes, but Mac is working hard on bringing cache to all repositories that want to use it.