make get_started point to the quickstart page
#453
Conversation
| @@ -1,16 +1,24 @@ | |||
| # Get started with Lean | |||
There was a problem hiding this comment.
I think (some) research mathematicians won't understand the difference between Lean and Mathlib. Maybe this can say: "Get started with Lean and Mathlib" (so they know it's a two-step process?)
| @@ -1,16 +1,24 @@ | |||
| # Get started with Lean | |||
|
|
|||
| We have installation instructions for the following operating systems: | |||
| For users wishing to get started quickly and easily, the [quickstart guide](https://lean-lang.org/lean4/doc/quickstart.html) should walk you through the installation procedure if using the Visual Studio Code editor is acceptable. | |||
There was a problem hiding this comment.
Can these be explicitly marked as "Step 1: Install VSCode and Lean" (is it possible to make the "lean-lang.org" link pop up in another window, so this window isn't lost -- since they'll need to return to it to know how to make a Mathlib project), and "Step 2: Create a Project Using Mathlib", followed by the stated instructions?
|
We should state clearly that someone who wants to use mathlib should stop after the step "install Lean version manager". The guide stops there in the sense that it doesn't say to go on with "set up Lean 4 project", but a mathematician who wants to start a project will probably continue thinking it is the right way. Also, I am not 100% sure we want to show the Lean documentation to mathematicians, I think what the step does is the same as clicking on |
|
What I mean is that maybe it is better to write our own guide, similar to what I did here but adding the first two steps (installing the extension as in the quickstart page and then installing elan using the menu). |
|
Hmm, one also need |
|
@j-loreaux @riccardobrasca Could you please make explicit why you do not want to follow the complete guide? |
I've nothing against the complete guide, but at some point a mathematician will probably want mathlib (newcomers don't know Lean and mathlib are separate entities), and I am not sure what is the best way of explaining this. |
|
The setup guide talks about Mathlib so if you think the wording should be improved, please open an issue at leanprover/vscode-lean4 |
This updates the "Get started with Lean" page so that it points to the quickstart guide first. We also remove the "basic" versions of the Mac OS and Debian install guides, but we leave in place the existing "detailed" versions for all platforms.