Lean is moving too fast

Lean's motto currently seems to be "move fast and break things". For many years Lean was frozen on 3.4.2 and the only thing in active development was its maths library mathlib. I didn't care that CoCalc's mathlib was old because I could just clone a modern mathlib and use that instead.

Now a community fork of Lean has taken place and we're currently up to 3.10. A tool has been developed called elan which manages which version of Lean to use with a given Lean repository (it looks at the leanpkg.toml of the Lean project and runs the appropriate version of Lean).

CoCalc's default situation is to have a fixed version of Lean and a fixed version of mathlib. This works fine for basic stuff, but nothing is backwards compatible and sometimes it's painful when modern features are missing (mathlib is continually adding tactics, even tactics which beginners might want to use).

On my own PC I use some tooling called leanproject, developed by Patrick Massot. When I want to work on a Lean project (mine or someone else's) I pull it with leanproject and when I open it, it runs with the correct version of Lean (which could be 3.4.2, 3.5.1, 3.6, 3.7, 3.8...) and the correct version of mathlib (with all the mathlib binaries pulled from some Azure cloud storage). The Lean community doesn't really see why CoCalc can't use the same system. leanproject is here https://github.com/leanprover-community/mathlib-tools and instructions on how a general user installs elan are here https://github.com/leanprover-community/mathlib/blob/master/docs/install/linux.md . I appreciate that CoCalc is different to a single-user install, but I am wondering whether it should be possible to override the default Lean installation on CoCalc. On the box I'm typing on I have over ten versions of Lean installed, in ~/.elan/toolchains .

sagemathinc / cocalc

Lean is moving too fast #4563