lake exe cache get not producing a useful cache on gitpod

Stream: mathlib4

[Eric Wieser]

I'm repeatedly finding that the following doesn't work:

• Open gitpod on a random branch
• Let lake exe cache get run. Everything works fine.
• git checkout some-other-branch
• pkill lake; pkill lean
• lake exe cache get (succeeds)
• Open a file that is definitely cached on the branch
• VSCode starts building random files in Std

[Eric Wieser]

Even lake exe cache clean!; lake exe cache get! still leaves me with a bad cache

[Eric Wieser]

Is this caused by switching branch changing the lean toolchain? (and vscode-lean4 caching the old version of lean?)

[Marc Huisinga]

Are you explicitly restarting the server using the corresponding VS Code command after checking out? Does that help?

[Eric Wieser]

Yes, if I didn't do that then it wouldn't build anything at all!

[Ruben Van de Velde]

Does it work locally? I'm only managing to get a cache with

rm -rf lake-packages/
rm -rf build/
rm -rf ~/.cache/mathlib
killall lean
lake exe cache clean!
lake exe cache get

recently

[Eric Wieser]

Ah, I bet those rms are the important bit (though I assume it's better to do them after the killall)

[Ruben Van de Velde]

I don't know if all of those lines are load-bearing, but most of them seem to be

[Damiano Testa]

I usually skip the third line of Ruben's process (rm ~/.cache/mathlib) and, so far, it worked for me.

[Eric Wieser]

From the other thread, it seems like lake exe cache clean is useless and lake clean does the job

[Damiano Testa]

Maybe ever removing packages/build can be skipped with lake clean?

[Damiano Testa]

I'll try to remember to experiment, next time I have problems with the cache.

[Damiano Testa]

Going back to this, I had something broken again in the cache and the following worked:

# end of previous `lake build` that was really building
[557/3776] Building Mathlib.Data.Nat.Basic
[558/3776] Building Mathlib.Algebra.Ring.MinimalAxioms
[559/3776] Building Mathlib.Algebra.Field.Defs
^C
$ lake clean
$ lake exe cache get
info: [0/6] Fetching proofwidgets cloud release
info: [1/9] Building Cache.IO
info: [2/9] Compiling Cache.IO
info: [2/9] Building Cache.Hashing
info: [3/9] Compiling Cache.Hashing
info: [3/9] Building Cache.Requests
info: [5/9] Compiling Cache.Requests
info: [5/9] Building Cache.Main
info: [7/9] Compiling Cache.Main
info: [9/9] Linking cache
No files to download
Decompressing 3778 file(s)
unpacked in 8067 ms
$ lake build
# no output, took about a second

So, lake clean seems to take care of the rms and lake exe cache clean!! This is great!

[Scott Morrison]

Yes, cache is badly broken for me today and requires a lake clean between most branch switches. If someone is able to investigate that would be great.

[Mario Carneiro]

It needs to be updated for 4.1.0

[Mario Carneiro]

there are new build files that need to go in the cache files

[Scott Morrison]

Sorry, I don't understand.

[Mario Carneiro]

currently we only store .olean in the ltar files, we need to also package all the new files lake is making now

[Mario Carneiro]

#7291