mathlib really too big

Stream: general

[Yaël Dillies]

I just got this exotic new error:

Looking for mathlib oleans for ae21d38615
  locally...
  remotely...
  Found remote mathlib oleans
Using matching cache
  ae21d38615: 100%|██████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████████| 77.3M/77.3M [00:04<00:00, 18.9MB/s]
[Errno 75] Value too large for defined data type: '/home/gitpod/.mathlib/tmpfy0npetj' -> '/home/gitpod/.mathlib/ae21d3861523c5b1f39598c5174d120cad2873a1.tar.xz'

Has mathlib grown too big for us, mere mortals?

[Yaël Dillies]

It might only be a problem with the specific gitpod workspace I was using :thinking:

[Yaël Dillies]

All my Lean setups are broken right now :sad: Gitpod because of the above errors and my local VScode because of

elan self update
←[1minfo: ←[0mchecking for self-updates
←[31m←[1merror: ←[0mfailed to parse latest release tag

[Mauricio Collares]

For the last error, you're probably using elan 1.4.1 and the GitHub server change is now preventing elan updates from working too. Reinstalling elan from scratch (curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh) should help.

[Yaël Dillies]

Indeed, uninstalling and reinstalling elan fixed it.

[Eric Wieser]

"Value too large for defined data type" just bit me for something unrelated on gitpod (accessing github credentials), so I think this is a gitpod problem

[Eric Wieser]

No need to reinstall from scratch, use elan self update

[Mauricio Collares]

The second error was the output of elan self update, I think

[Mauricio Collares]

The problem fixed in 1.4.2 is that GitHub changed its releases page, which is scraped to determine available versions/tags. GH probably does staged rollouts, because this was only a problem for the Lean 4 repo at first, then it reached Lean 3 and now elan.

[Kevin Buzzard]

So now when I have 30 undergraduates arriving at my workshop with broken setups the canonical response is "reinstall elan"?

[Mauricio Collares]

Yes, with the caveat that the Lean macOS install script uses brew, so elan should be updated using brew in this case

[Yaël Dillies]

Can't we setup dedicated Gitpod commands on workspace opening on the project repos?

[Mauricio Collares]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.22dev.20container.22.20v.20gitpod.20v.20local.20Lean/near/300056315 is the thread to follow wrt having an updated elan by default in Gitpod workspaces (tl;dr: #16590 needs review). This is orthogonal to the other GItpod errors you were seeing earlier, which were due to a Gitpod server issue that's now fixed (once you restart your workspace).

[Yaël Dillies]

Indeed I'm on eu67 for all workspaces now.

[Riccardo Brasca]

Kevin Buzzard said:

So now when I have 30 undergraduates arriving at my workshop with broken setups the canonical response is "reinstall elan"?

Forgetting about this specific problem, in your experience is using gitpod a good choice for a course about Lean? I am going to teach a minicourse and I don't want to waist time in fighting installation problems.

[Kevin Buzzard]

I bit the bullet and got their local installations working for my workshop this week. I'm going to try gitpod in October

[Bhavik Mehta]

I tried getting a group set up today, and it was more annoying than I expected