Run MIL in ubuntu 18.04

Stream: new members

[Shanghe Chen]

Hi I am trying to run MIL in a environment with os Ubuntu 18.04 (I cannot change the os but it has more powerful cpu and larger memory. It seems the prebuilt Lean is too new for this distribution. Any way to handle this?

[Shanghe Chen]

I checked that in this env I can build mathlib in 40minutes, much faster than my laptop, that’s why I want to use it:) And it seems werid that I can successfully build mathlib’s master but got a 'no Glibc 2.28' when running lake exec cache get in MIL though. It seems the bundle clang is too new for ubuntu 18.04

[Patrick Massot]

I think there is no way you could convince Lean devs to spend any time working on supporting such an ancient system. Did you try using GitPod instead?

[Shanghe Chen]

Yeah thank you for the advice :laughing: I finally got a docker container ran on it with ubuntu 20.04. And I am trying to using code-server inside it, which is something like a vscode editor inside a browser

[Shanghe Chen]

I checked some old topics too. It does be very hard to do something new on ubuntu 18.04 https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Ubuntu.20.2F.20VS.20Code