Installation instructions for elan without VSCode

Stream: lean4

[Niels Voss]

I recently had to install Lean in WSL due to a Lean project not being supported on Windows, and I was surprised to see that the only installation instructions for Lean were to install VSCode, run the "Setup guide" command in VSCode, and then click on a link within the setup guide. All this does is cause VSCode to run the command

bash -c 'curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain leanprover/lean4:stable || (echo && read -n 1 -s -r -p "Install failed, press ENTER to continue...")' && exit

The bash and powershell scripts to install elan are not linked anywhere on the webpage. I'm personally more comfortable with installing using the terminal, so my first instinct after I didn't find any shell commands on the webpage was to run sudo apt install elan, but this unfortunately gave me version 1.something of elan which was hopelessly out of date.

I think it's totally reasonable to have the default installation method be through the setup guide on VSCode, since many mathematicians aren't familiar with the terminal. However, if it won't cause any maintenance issues, could there at least be a link to shell based installation instructions (such as the official elan installation instructions), for advanced users? Right now the only link on the official installation instructions webpage is to here: https://github.com/leanprover/lean4/releases, which I think is probably the last link we want to be providing new users.

[Jz Pan]

The last 5 legacy links in https://leanprover-community.github.io/get_started.html should provide you installation instructions with command line. It may be unclear, though.

[Niels Voss]

I was able to get it working but I hope this gets fixed on the official website because we shouldn't be pointing newcomers to the legacy instructions