lake exe cache get problems?

Stream: general

[Alex Kontorovich]

Has anyone had the following experience? I merged master with a branch, waited a while, opened VSCode, and refreshed dependencies. Lean says it's compiling starting with file [1800/2400]. I think, wait, that's going to take forever. So I close VSCode, and lake exe cache get. Then I open VSCode and refresh dependencies again. Now Lean says it's compiling starting with file [300/2400]. :( Did I do something wrong??

[Damiano Testa]

Assuming that the cache is remotely available, these issue typically get resolved after lake exe cache clean or, sometimes rm -rf .lake (think hard about issuing this last command!).

[Damiano Testa]

Of course, running lake exe cache get afterwards!

[Alex Kontorovich]

Got it, thanks!

[Kevin Buzzard]

with this sort of situation, if my branch is just a few files changed from master and nothing too low-level, I checkout master, do lake exe cache get there, and then checkout the branch and then hopefully it just has to compile the files I changed.

[Yaël Dillies]

Kevin, this technique helped in Lean 3 where we didn't have a granular cache, but in Lean 4 this is exactly the same as running lake exe cache get on the branch

[Kevin Buzzard]

Even if the branch has just been merged with master locally and not pushed, using any one of the three ways that git can merge branches?

[Yaël Dillies]

Yes, because all that matters is the state of the files, not how you got there

[Yaël Dillies]

cache is git-agnostic

[Eric Wieser]

Yaël Dillies said:

Kevin, this technique helped in Lean 3 where we didn't have a granular cache, but in Lean 4 this is exactly the same as running lake exe cache get on the branch

While the end result is the same, Kevin's approach can be much faster; lake exe cache get is far slower on a missing cache than a present one.

[Mario Carneiro]

I wish I knew why :(

[Mario Carneiro]

It is literally the network request (i.e. azure) which takes longer to return 404 than 200

[Sebastian Ullrich]

Is it caching? The variation of failing requests is likely much higher than succeeding ones as any change results in completely different hashes downstream

[Mario Carneiro]

in that case, wouldn't you expect running it a second time to be fast?

[Mario Carneiro]

I mean, it shouldn't be a difficult test to run it in a loop and see if the server eventually decides it's worth caching

[Sebastian Ullrich]

I haven't tried. Maybe they just don't do negative caching

[Mario Carneiro]

I suppose that makes sense, you don't want to be on the hook as a caching service if you are serving cached 404s when the file is hot off the press

[Eric Wieser]

Can we teach cache to create empty files or something for "this file was unbuildable", so that that information is cached positively?

[Mario Carneiro]

wouldn't it be lake creating those files?

[Eric Wieser]

I think either would work, though maybe only lake has the info needed to create them

[Mario Carneiro]

cache can't tell the difference between good files and bad, outdated files