building lean on CentOS

Stream: general

[Sebastian Ullrich]

@Damiano Testa We're building against glibc 2.27 from 2018 and you're saying that's still too new? :scream:

[Damiano Testa]

This is the error that I get:

mathlib4 (master)$ lake build
info: downloading component 'lean'
176.3 MiB / 176.3 MiB (100 %)  81.2 MiB/s ETA:   0 s
info: installing component 'lean'
/local/localhome/maskal/.elan/toolchains/leanprover--lean4---nightly-2022-11-26/bin/lake: /lib64/libm.so.6: version `GLIBC_2.27' not found (required by /local/localhome/maskal/.elan/toolchains/leanprover--lean4---nightly-2022-11-26/lib/libLLVM-15.so)
/local/localhome/maskal/.elan/toolchains/leanprover--lean4---nightly-2022-11-26/bin/lake: /lib64/libc.so.6: version `GLIBC_2.18' not found (required by /local/localhome/maskal/.elan/toolchains/leanprover--lean4---nightly-2022-11-26/lib/libc++abi.so.1)

[Damiano Testa]

The IT person who tried to help me seemed somewhat ashamed that this was the state of affairs and said that he is trying to update the system, but gave me a timeline of 6 months (and gave me the impression that this was very optimistic).

[Sebastian Ullrich]

Phew. What OS is this?

[Damiano Testa]

I think CentOS: is a university-managed linux computer that I use

[Damiano Testa]

Btw, I have no issues with my home computers, but there I can take care of installing whatever I want.

[Damiano Testa]

I also had a similar issue with git, where the local version was over 10 years old, before I asked it to be updated...

[Riccardo Brasca]

Wow, I think I have to stop to complain about computers in my university :dizzy:

[Sebastian Ullrich]

@Damiano Testa If you really want to run Lean on there, you could compile it from source, upload it as a release of a fork of the lean4 repo and then tell elan to use that release (you/lean4:therelease in lean-toolchain)

[Damiano Testa]

Sebastian, I would be happy to try this, but I would definitely need more guidance!

[Damiano Testa]

Should I follow the first steps here?
https://leanprover.github.io/lean4/doc/make/index.html

[Sebastian Ullrich]

Yes, that would be the first step!

[Damiano Testa]

Is there a workaround for this also?

/lean4/build/release (master)$ cmake ../..
CMake Error at CMakeLists.txt:1 (cmake_minimum_required):
  CMake 3.11 or higher is required.  You are running version 2.8.12.2


-- Configuring incomplete, errors occurred!

[Sebastian Ullrich]

Ah no, that is a problem...

[Damiano Testa]

(also, I would move this discussion to #general, but I can only rename the thread, not the stream.)

[Damiano Testa]

I have absolutely no idea if this is in any way reasonable, but maybe I could ask to get CMake updated? Or is this something like updating glibc?

[Notification Bot]

16 messages were moved here from #Geographic locality > Warwickshire, UK by Mario Carneiro.

[Gabriel Ebner]

For anybody who's curious like me: CentOS 7 is still supported until 2024 and ships with glibc 2.17.

$ podman run --rm docker.io/centos:7 ldd --version
ldd (GNU libc) 2.17

[Damiano Testa]

I hope that this does not mean that I have to wait until 2024 to be able to use Lean4 on the computer in my office...

[Jireh Loreaux]

Why not just ssh in to your home machine?

[Ruben Van de Velde]

Maybe in 2024 they'll install ssh on his office computer :)

[Damiano Testa]

Jireh, I usually do not leave my home computer on. Also, would I be able to use VSCode remotely?

[Matthew Ballard]

There is also an official VS Code Server now

[Jireh Loreaux]

Yes, you can use VS Code over ssh. You could set up your home machine to wake on network access. Then you could leave it sleeping when you're not using it.

[Jireh Loreaux]

If you do this, I suggest only allowing public key authentication, disabling root access, and opening a nonstandard port on your router. The latter prevents dumb bots trying port 22 nonstop, which can be super annoying.

[Damiano Testa]

Thank you all for the suggestions! I'll try some of these out!

[Shreyas Srinivas]

Is there a gitpod setup for lean?

[Shreyas Srinivas]

Does gitpod support using lean on it?

[Shreyas Srinivas]

Perhaps one of the cloud development environments that vscode in the browser could help?

[Matthew Ballard]

If you don’t want to expose your machine directly to the public, Tailscale is very convenient. Apparently it has CentOS 7 installation instructions too.

[Kevin Buzzard]

@Damiano Testa you know you can just run Lean (fast) through a browser? Some people with slow laptops even use this method because it's quicker than using lean on their own computers. See the "play online using gitpod" link here https://github.com/ImperialCollegeLondon/formalising-mathematics-2023 to see how some of my students are doing Lean in my course.

[Eric Wieser]

Shreyas Srinivas said:

Is there are gitpod setup for lean?

The mathlib and mathlib4 repos are already configured for a nice gitpod experience

[Arthur Paulino]

Eric Wieser said:

The mathlib and mathlib4 repos are already configured for a nice gitpod experience

Is cache still failing for gitpod on mathlib4?

[Damiano Testa]

Kevin, the setup for your course is really great! When I last used gitpod, I did not think that it was a good replacement for a computer, but the link that you sent changed my mind! I will take inspiration from it, thanks!

[Gabriel Ebner]

Arthur Paulino said:

Eric Wieser said:

The mathlib and mathlib4 repos are already configured for a nice gitpod experience

Is cache still failing for gitpod on mathlib4?

No after upgrading the Ubuntu version it works fine now. A common story. :smile: