Cache doesn't work in Ona

Stream: mathlib4

[Yaël Dillies]

Since gitpod was retired yesterday, I am trying to use its successor, ona, to little avail so far. Many non-lean things are going wrong (I can't seem to push to other people's forks, I can't find the Make pull requests suggestions button anymore, it keeps on asking me to log into github, etc...), but there is one crucial lean thing that I can't seem to be able to do anymore: download cache.

[Yaël Dillies]

Here's a tentative repro:

1. Go to https://app.gitpod.io/ai, create an account, verify your credit card, sell your soul, whatever...
2. Create a repo from URL with url https://github.com/leanprover-community/mathlib4
3. Run git remote add yael https://github.com/yael/mathlib4; git fetch yael; git checkout yael/more_grw_gcongr (this is the branch from #30508, which I chose because it changes a lot of files, and therefore prominently displays the cache issue).
4. Download the cache for an advanced file (eg MeasureTheory.Measure.WithDensity) any way you want, eg lake exe cache get or command palette + fetching imports for that file.
5. Issue: No cache was downloaded

[Shreyas Srinivas]

doesn't ona/gitpod use devcontainers these days?

[Shreyas Srinivas]

I don't recall the cache ever getting downloaded on codespaces which also uses devcontainers

[Shreyas Srinivas]

I had to do that by hand

[Yaël Dillies]

What do you mean "by hand"? I am also doing it "by hand", ie running lake exe cache get myself, and I would expect that to work but it doesn't.

[Yaël Dillies]

In fact, trying the above on another branch works just fine. Maybe the issue is with my branch more_grw_gcongr? Can somebody try?

[Shreyas Srinivas]

Oh okay. That's a different issue then

[Yury G. Kudryashov]

What's the output of lake exe cache get?

[Junyan Xu]

I've encountered failures to create the GitHub codespace on some branches (e.g. #30144) with older mathlib (a few weeks outdated), which I think may be related. On more recent master, I'm not seeing the first two info lines and the codespace is created successfully, so something probably changed with the devcontainer/gitpod configuration in the last few weeks. (Why does "gitpod" show up when creating a GitHub codespace?) It's wild it ran out of space, as the successfully created codespaces only take less than 10GB each, a lot less than the 32GB limit.

lake exe cache get!
info: downloading https://releases.lean-lang.org/lean4/v4.24.0-rc1/lean-4.24.0-rc1-linux.tar.zst
438.4 MiB / 438.4 MiB (100 %)  84.0 MiB/s ETA:   0 s
info: installing /home/gitpod/.elan/toolchains/leanprover--lean4---v4.24.0-rc1
info: plausible: cloning ********/leanprover-community/plausible
info: plausible: checking out revision '9f492660e9837df43fd885a2ad05c520da9ff9f5'
...
Current branch: binRec_npow
Using cache (Azure) from origin: ********
Attempting to download 7271 file(s) from leanprover-community/mathlib4 cache
Downloaded: 1463 file(s) [attempted 7271/7271 = 100%, 1 KB/s]]]
Attempting to download 7271 file(s) from ******** cache
Downloaded: 7271 file(s) [attempted 7271/7271 = 100%, 356 KB/s]
Decompressing 7271 file(s)
/home/gitpod/.cache/mathlib/0b1d21d7dc7b2f02.ltar: No space left on device (os error 28)
/home/gitpod/.cache/mathlib/2f55c087f3e4aa12.ltar: No space left on device (os error 28)
/home/gitpod/.cache/mathlib/2aac45608b6c25da.ltar: No space left on device (os error 28)
...

[Yaël Dillies]

The cache seems to work now. But the ona environments seem to be generally unstable: After some time (in hours), github authentication fails in weird ways and I cannot push to my repos anymore!