Gitpod

Stream: lean4

[Jeremy Avigad]

Does anyone have a best practice guideline for using Lean 4 with Gitpod? This used to work:
https://github.com/avigad/lamr
But now it gives the message:

info: downloading component 'lean'
error: binary package was not provided for 'linux'

I can fix it by typing elan self update and then lake build in the terminal and then restarting the server. But if I try adding lean self update to the init portion of the .yml file, it doesn't work.

As a fallback, I suppose I can delete the line that fetches elan and let the Lean 4 extension do it. But it would be nice to do lake build in the init section, because Gitpod will prebuild the image with that and make loading faster.

[Jeremy Avigad]

Update: updating elan in the Dockerfile (instead of the yml file) seems to have done the trick! So, never mind (unless someone has a better solution).

[Sebastian Ullrich]

Any change to the Dockerfile probably would have been sufficient because it would invalidate the cached image. You can also do so manually without editing the file, https://www.gitpod.io/docs/configure/workspaces/workspace-image#manually-rebuild-a-workspace-image

[Bolton Bailey]

Wanting to get a little experience with Lean 4, I recently watched Scott's tutorial on porting things to Lean 4. I started following the instructions but I stopped when it got to the point where I had to actually install Lean 4, because it was telling me I would have to update elan, and I was afraid that would interfere with my Rosetta installation of elan. Is there a way of working on mathlib4 through Gitpod?

[Bolton Bailey]

Is there a reason that video is unlisted by the way @Scott Morrison ? I thought it was a good tutorial on the porting process.

[Scott Morrison]

Only that it seemed likely to quickly become outdated. I don't mind if it is switched to public so people can find it on the leanprover-community YouTube page. I'm away from a computer at that moment but if I remember tomorrow I'll change the setting.

[Matthew Ballard]

I’ve found packing more instructions in the Dockerfile than in the bespoke config files (either GitPod or Codespaces) to generally be better.

[Sebastian Ullrich]

Bolton Bailey said:

because it was telling me I would have to update elan, and I was afraid that would interfere with my Rosetta installation of elan

I'm not aware of anything that could go wrong with that fwiw. You should not need a second elan.