long rebuilding after `lake exe cache get`

Stream: lean4

[Bolton Bailey]

On #21567, I'm told I need to run shake. To do this, I'd like to get the cache first, so that I don't have to wait to build mathlib on my own computer. But it seems I am not getting the cache for the build of my branch, since when I lake build afterwards, it has thousands of files left to go.

• When my code compiles, but the CI Build check fails due to a shake problem, does a cache get created?
• If not, could it be made to?
• In general, is there a way of seeing what cache was pulled / am I misinterpreting things here?

~/Desktop/mathlibcontribution/mathlib4 BoltonBailey/split-set-insert ............... INT 2m 27s 23:49:32
> lake exe cache get
No files to download
Decompressing 6048 file(s)
Unpacked in 438 ms
Completed successfully!                                                                             /1.7s

~/Desktop/mathlibcontribution/mathlib4 BoltonBailey/split-set-insert .......................... 23:49:42
> lake build
⣟ [1955/6059] Running Mathlib.Data.List.Perm.Lattice (+ 11 more)^C                                  /7.5s

[Damiano Testa]

The cache should have been uploaded as soon as the earlier build step finished, whether it was successful or not.

[Damiano Testa]

Have you tried removing the .lake dir (or just the trace for Import graph.imports) and download the cache again?

[Bolton Bailey]

I would be reluctant to remove .lake, since it would require recloning all the dependencies, and I have been having problems doing that consistently. By now it rebuilt on my laptop, but I can try this next time it happens though, thanks.

[Ruben Van de Velde]

My first try would be lake exe cache get! with exclamation mark

[Kevin Buzzard]

My first try would be removing .lake, it currently has a high chance of fixing everything in my experience. If this is causing you problems then this sounds like a separate question.

[Mauricio Collares]

If you'd like to help with testing, there are two commands you can try:

1) rm .lake/packages/importGraph/.lake/build/lib/ImportGraph/Imports.trace
2) for file in `grep -Rl "simp\?.*says" Mathlib`; do rm -v .lake/build/lib/${file%.lean}.trace; done

Ideally, you'd run lake exe cache getand lake build after each of the two commands, to see if it was useful. Thanks!

[Mauricio Collares]

If neither works, please back up .lake and upload it somewhere, and please mention the exact mathlib commit you're testing. Deleting .lakeafterwards is fine, but fixing the underlying bug is much harder if everyone just goes for the quick workaround!

[Bolton Bailey]

Yes, sorry, I'd love to get to the bottom of it, but it wasn't my priority last night and to my ironic frustration, lake exe cache get ; lake build now works fine.