Simple getting-started guide?

Stream: general

[David Loeffler]

I'm teaching a Lean mini-course at a workshop in a week's time, so I'm going to need to guide a bunch of people through getting started with Lean and Mathlib – firstly, installing it on their computers.

I was a bit startled to realise that if I follow, verbatim, the instructions under "Creating a Lean project" here, things don't quite work.

Firstly, it tells you to mkdir MyProject when the previous step has already created a MyProject folder. This is a minor glitch. But, much more seriously, when you go on to the next step – creating a file MyProject/Test.lean in VSCode, and importing some of mathlib in it – it starts recompiling mathlib from scratch!

This is clearly going to make for a terrible experience for first-time users of Lean. How can I fix this? Where can I find a set of simple, easily-followable instructions (ideally with the minimum of obscure command-line runes to type) which will get first-time users set up so they can do some simple examples using mathlib?

[Michael Stoll]

This may be related to the discussion here.

[Kevin Buzzard]

When I've been in this situation I've made a repo and told everyone to clone it, and also given instructions on how to actually not even clone it and just use gitpod/codespaces. For example here. I agree that right now this is super-painful.

[Markus Himmel]

The modern recommended way of installing Lean and creating a project is via the VS Code extension using the instructions at https://lean-lang.org/lean4/doc/quickstart.html and the instructions inside VS Code. It is no longer necessary to use the terminal at all to create a Lean project (including mathlib).

[Kevin Buzzard]

The two most common problems in my experience are: Windows users with firewalls which need to be turned off / taught that Lean is not a virus, and some mathematicians just generally being completely incompetent and having already-borked systems. Like Markus I would heavily recommend not using a terminal at all (one issue with terminals is that some Windows users have random terminals and random stuff doesn't work in them, e.g. I think the default Windows command line is not great when it comes to getting Lean working)

[David Loeffler]

Markus Himmel said:

The modern recommended way of installing Lean and creating a project is via the VS Code extension using the instructions at https://lean-lang.org/lean4/doc/quickstart.html and the instructions inside VS Code. It is no longer necessary to use the terminal at all to create a Lean project (including mathlib).

Then I can't help feeling it should be a rather urgent priority to remove the outdated instructions from the prominent place they currently enjoy on the Lean community website.

[David Loeffler]

Markus Himmel said:

The modern recommended way of installing Lean and creating a project is via the VS Code extension using the instructions at https://lean-lang.org/lean4/doc/quickstart.html and the instructions inside VS Code. It is no longer necessary to use the terminal at all to create a Lean project (including mathlib).

Following the "modern recommended way" also seems to result in mathlib being compiled from scratch.

[Markus Himmel]

David Loeffler said:

Following the "modern recommended way" also seems to result in mathlib being compiled from scratch.

Thank you for reporting this. I can reproduce the problem. The extension runs lake exe cache get which finishes successfully, but there seems to be a problem with the cache (lake build also rebuilds mathlib).

[Mauricio Collares]

This is being discussed in https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Updating.20to.204.2E15.2E0 -- it's a bug in Lean v4.16.0-rc1 which affects projects depending on mathlib (but not mathlib itself), and which will probably require a new Lean release to be fixed.