Zulip Chat Archive
Stream: PR reviews
Topic: mathlib4#1419 gitpod config
Eric Wieser (Jan 10 2023 at 13:21):
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 (Jan 10 2023 at 15:36):
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 (Jan 10 2023 at 16:15):
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 (Jan 10 2023 at 17:29):
+1 this will also make it easier to debug the lake cache issue on gitpod
Gabriel Ebner (Jan 10 2023 at 18:41):
I have no idea what's wrong with curl on the default gitpod container.
Gabriel Ebner (Jan 10 2023 at 18:41):
Apparently it randomly saves empty files.
Gabriel Ebner (Jan 10 2023 at 18:41):
The curl log doesn't contain any errors as far as I can tell.
Gabriel Ebner (Jan 10 2023 at 18:42):
Using --parallel-max 10
doesn't help either.
Gabriel Ebner (Jan 10 2023 at 18:42):
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 (Jan 10 2023 at 18:42):
And those can be unpacked fine..
Gabriel Ebner (Jan 10 2023 at 18:43):
Only fix is to disable --parallel
completely.
Gabriel Ebner (Jan 10 2023 at 18:43):
Or to upgrade the ubuntu version. mathlib4#1457
Gabriel Ebner (Jan 10 2023 at 18:50):
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 (Jan 11 2023 at 20:14):
Gitpod works for me now. Thank you, Arthur, Eric and Gabriel!
Last updated: Dec 20 2023 at 11:08 UTC