create new project depending on mathlib; 0 terminal

Stream: general

[Kevin Buzzard]

I had thought that we were now at the stage where you could install Lean and create a new maths project without ever typing something into the terminal. The instructions to install Lean in the Lean 4 manual here don't use a terminal, and I thought there was some kind of panel which you can somehow open in order to make a new project depending on mathlib but I don't know how to make this panel appear. The Lean 4 manual refers to the mathlib4 readme, which doesn't seem to explain this new tool (did I just dream it?)

Looking at the community pages we are still telling mac users to install on command line here and then the link to make a project on the community website here is also command line.

Is there documentation somewhere for "basic usage for mathematicians who don't want to use command line at all?" Am I wrong in thinking that we recently attained the nirvana of being able to install Lean and make a new maths project with 0 command line?

[Patrick Massot]

The updated instructions are coming at lean4#2968

[Patrick Massot]

Looking at it, I wonder whether @Marc Huisinga is waiting for me to do something there.

[Marc Huisinga]

I got distracted by other things but will merge it on monday.

If you'd like to read the new instructions, you can click the forall symbol in the top right in VS code while a file is open and select Documentation > Show Setup Guide.
The button to create new projects using Mathlib is in the same forall button menu.