cache adoption by std4

Stream: std4

[Arthur Paulino]

As of now, cache is limited to mathlib4 and to the projects that use it as a dependency (to download mathlib4 cache). We've had some discussions in the past and Mario said that it would be good to have this functionality available for std4 as well. So I thought of having the Cache code placed at std4 instead. So mathlib4 would inherit it. There are, of course, some gotchas:

• Cache would also require a configuration file (cache-manifest.json or smth) that would contain, among other information, the URL of the host endpoint
• We would need another Azure blob to store std4 cache
• mathlib4 wouldn't be able to use std4 cache files as I originally intended
• Running cache for the first time without a configuration file set would prompt a smart menu to configure one. This would be useful for projects that use mathlib4

What do you think? @Gabriel Ebner @Mario Carneiro

[Sebastian Ullrich]

mathlib4 wouldn't be able to use std4 cache files as I originally intended

Why is that?

[Gabriel Ebner]

:+1: for moving to std4

[Gabriel Ebner]

Running cache for the first time without a configuration file set would prompt a smart menu to configure one

I think that's overkill, or at least a very very low priority task. Copy-pasting a config file is peanuts compared to setting up an azure bucket.

[Arthur Paulino]

Sebastian Ullrich said:

mathlib4 wouldn't be able to use std4 cache files as I originally intended

Why is that?

Because of non-matching toolchains. See Gabriel's comment here

[Gabriel Ebner]

Also lake cache hashes mathlib4's lakefile. Presumably std4 would hash std4's lakefile so they'd have different hashes.

[Gabriel Ebner]

(Longer term we want better hashes. But emphasis on longer term.)

[Arthur Paulino]

Theoretically cache could hash std4 files in mathlib4 as it would do from within std4 itself so the hashes would match, But it doesn't seem to be worth the effort?

[Arthur Paulino]

Actually that strategy fails due to incompatible toolchains

[Arthur Paulino]

Gabriel Ebner said:

Running cache for the first time without a configuration file set would prompt a smart menu to configure one

I think that's overkill, or at least a very very low priority task. Copy-pasting a config file is peanuts compared to setting up an azure bucket.

Oh I wasn't aiming to set an azure bucket. I just wanted to provide a way for the user to say which config file should be copied:

2 cache config files were detected. Which one do you want to copy?
(1) lake-packages/mathlib4/cache-config.json
(2) lake-packages/std4/cache-config.json
>

More ideas are welcome

[Arthur Paulino]

Gabriel Ebner said:

:+1: for moving to std4

I will start this refactor in the mathlib4 repo itself because it already has enough infra for testing (a bucket and pushed files). Once it's working nicely, I can factor it out to std4

[Arthur Paulino]

I finally found some time to work on this. Let's see how things go

[Arthur Paulino]

Sorry for the delay. Too many interruptions
!4#2509
cc @Gabriel Ebner

[Arthur Paulino]

Actually, I'm gonna X-post this on #mathlib4 > lake exe cache get