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.

[Yaël Dillies]

Opening mathlib4 in gitpod currently results in

 HISTFILE=/workspace/.gitpod/cmd-0 history -r; {
elan self update
lake exe cache get

}
 -r; { /workspace/mathlib4 (master) $  HISTFILE=/workspace/.gitpod/cmd-0 history
> elan self update
> lake exe cache get
>
> }
info: downloading component 'lean'
info: installing component 'lean'
info: batteries: cloning https://github.com/leanprover-community/batteries to '././.lake/packages/batteries'
info: Qq: cloning https://github.com/leanprover-community/quote4 to '././.lake/packages/Qq'
info: aesop: cloning https://github.com/leanprover-community/aesop to '././.lake/packages/aesop'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4 to '././.lake/packages/proofwidgets'
info: importGraph: cloning https://github.com/leanprover-community/import-graph to '././.lake/packages/importGraph'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient to '././.lake/packages/LeanSearchClient'
info: plausible: cloning https://github.com/leanprover-community/plausible to '././.lake/packages/plausible'
info: Cli: cloning https://github.com/leanprover/lean4-cli to '././.lake/packages/Cli'
✖ [10/10] Building cache
trace: .> /home/gitpod/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin/leanc -o ././.lake/build/bin/cache ././.lake/build/ir/Cache/Main.c.o.export ././.lake/build/ir/Cache/IO.c.o.export ././.lake/build/ir/Cache/Hashing.c.o.export ././.lake/build/ir/Cache/Requests.c.o.export
info: stderr:
ld.lld: error: unable to find library -lpthread
ld.lld: error: unable to find library -ldl
ld.lld: error: unable to find library -lrt
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/gitpod/.elan/toolchains/leanprover--lean4---v4.14.0-rc1/bin/leanc' exited with code 1
Some required builds logged failures:
- cache
error: build failed

[Yaël Dillies]

Did Lean recently start requiring new libraries lpthread, ldl, lrt?

[Ruben Van de Velde]

I saw someone else flagging a linking issue on zulip yesterday (?)

[Shreyas Srinivas]

Seems likely but this can be fixed in the docker image file

[Sebastian Ullrich]

Thanks, this makes it easier to reproduce than #mathlib4 > lake exe cache get error. It is definitely not intended.

[Yaël Dillies]

There is now lean4#5966 to fix it

[Shreyas Srinivas]

While on the subject of gitpod, do we know how gitpod's plans to switch to their flex setup help/hinder us?

[Shreyas Srinivas]

I believe there is an option to self-host freely. Also their gitpod desktop installation takes care of installing docker (although currently it only works on macOS, they have suggested that windows and linux releases can be expected).

[Markus Himmel]

Yaël Dillies said:

There is now lean4#5966 to fix it

This is now released as 4.14.0-rc2 and the toolchain on mathlib master is updated, so Gitpod is usable again.