Easy way to install lean4/mathlib4

Stream: Lean for teaching

[Miguel Marco]

I plan to use lean in a general topology course i will teach after september, and I am considering if i should go with lean3 or 4. I only need very basic things from mathlib, so i think that won't be a problem.

My biggest worry about using version 4 involves the installation instructions to give to my students. WIth lean3 i can just tell them to download the tryleanbundle, uncompress it, and that is basically it.

The instructions on the web for installing lean4 also seem very easy: install vscode, install the lean4 extension, and open a new lean4 file. But when i tried it, they failed: apparently one needs to add a lean-toolchain file (that is not mentioned in the documentation). And when you make it work, you find that you don't have mathlib4 installed: so you need to go through several other commands to create a lake project, make sure you tell elan and lake to use compatible versions, ask lake to download mathlib, and then also to download the compiled olean files... sounds like too confusing for a general audience of math students (who might not be familiar with the command line, just to mention a first obstacle).

So, is there a simpler way to get a working lean4/mathlib4 environment? I would need something that is not much more complicated than the trylean option.

[Kevin Buzzard]

The three methods I know for getting Lean 4 projects to students are detailed in the README of this Lean 4 project. The last two involve running Lean on an external machine. The first example is supposed to make it as easy as possible to run locally; when I am teaching a course I never upgrade mathlib during the course because I'm worried this will just break students' set-ups.

[Miguel Marco]

Thanks. Gitpod and codespaces would require the students to get an account, right? I would also prefer to avoid it if possible.

I think that, considering the available options now, I will stick to lean3 through the trylean bundle.