mathlib4#1419 gitpod config

Stream: PR reviews

[Eric Wieser]

Are we happy to merge this? It's a lot more pleasant than spinning up a clean gitpod install and having to install the Lean4 extension and elan manually.

[Yaël Dillies]

The new caching system makes it that I don't need gitpod as much as before (downloading times are much shorter), but yes I am happy for this to be merged.

[Eric Wieser]

It's unfortunate that lake exe cache doesn't work on gitpod, but that is probably something we can fix later once we work out whether it's a curl issue or a lake exe cache issue.

[Gabriel Ebner]

+1 this will also make it easier to debug the lake cache issue on gitpod

[Gabriel Ebner]

I have no idea what's wrong with curl on the default gitpod container.

[Gabriel Ebner]

Apparently it randomly saves empty files.

[Gabriel Ebner]

The curl log doesn't contain any errors as far as I can tell.

[Gabriel Ebner]

Using --parallel-max 10 doesn't help either.

[Gabriel Ebner]

This is really random. If you remove the empty files, then curl will manage to download some more files (and some more empty files). If you repeat this a few times, you get all files.

[Gabriel Ebner]

And those can be unpacked fine..

[Gabriel Ebner]

Only fix is to disable --parallel completely.

[Gabriel Ebner]

Or to upgrade the ubuntu version. mathlib4#1457

[Gabriel Ebner]

I can repro the empty files issue in a fresh ubuntu 20.04 container. Let's bump the minimum curl version. mathlib4#1459

[Heather Macbeth]

Gitpod works for me now. Thank you, Arthur, Eric and Gabriel!