updating `lake exe cache get`

Stream: mathlib4

[Jon Eugster]

With #21666 the first of a couple PRs making changes to cache is going to land. I'd hope there won't be any hick-ups (all changes are properly reviewed and tested by CI as well as manually) but just in case things do break down at some point, I wanted to announce it here: Please report any problems so that they can be quickly fixed or any problematic PRs reversed :)

[Damiano Testa]

As a very small data point, my daily use of lake exe cache get is still normal with the current master.

[Arthur Paulino]

The next tricky thing with Cache is (or was) making it work on projects using mathlib as a dependency. If someone can confirm that works, then there's likely nothing else to fear

[Damiano Testa]

I just cloned the #Carleson project and ran

$ lake update mathlib
info: mathlib: checking out revision 'd321983b9320ffdc8c1d97770e7f99ce46aa8015'
info: toolchain not updated; already up-to-date
info: LeanSearchClient: checking out revision '0c169a0d55fef3763cfb3099eafd7b884ec7e41d'
info: importGraph: checking out revision '461b96f5527089718cb23d3f1fd2960a5d0ff516'
info: proofwidgets: checking out revision '322a050322e97b0a701588d9b1efbe2bee7f8527'
info: batteries: checking out revision 'b18855cb0f9a19bd4d7e21f3e5525272e377f431'
info: mathlib: running post-update hooks
Attempting to download 6115 file(s)
Downloaded: 6115 file(s) [attempted 6115/6115 = 100%] (100% success)
Decompressing 6115 file(s)
Unpacked in 29242 ms
Completed successfully!

[Damiano Testa]

So, this is looking good!

[Damiano Testa]

lake build then started building stuff, but, as far as I could tell, the files being built were all in Carleson.

[Jon Eugster]

There is a CI step which tests this with a sample dowstream project in Mathlib/DownstreamTest. If there is any doubt this test isn't thorough enough, we should probably improve this test setup

[Damiano Testa]

I had forgotten about DownstreamTest!