8
$\begingroup$

I want to get started with Lean 4, but I need to install it. The download page links to binaries to download, but I don't know what to do with them. Is there a "best practice" way to install Lean, or should I just download them and put them in my $PATH?

I'm using Arch Linux (x86-64).

Improve this question
$\endgroup$
6
  • 8
    $\begingroup$ I agree with the answer by k4rtik. If you're going to ask how to install something, it would be nice if you could show us what you have tried so far. $\endgroup$
    – Nike Dattani
    Feb 8, 2022 at 18:06
  • $\begingroup$ @NikeDattani "The download page links to binaries to download, but I don't know what to do with them". I was going to install Lean by just copying the binaries somewhere, but I wanted to know if there was a better ("best practice") method of doing so. And now I know about elan, which I missed in my initial search. $\endgroup$
    – pxeger
    Feb 8, 2022 at 19:49
  • 2
    $\begingroup$ Since there is no documentation on how to install the basic binaries (without elan) I would say this is on topic. On linux, /user/local/bin is a good place to put binaries. $\endgroup$
    – Couchy ♦
    Mar 4, 2022 at 1:15
  • 1
    $\begingroup$ How can installing a proof asssistant be "off topic" on the Proof assistants Q & A site?! Come on people, don't be like those other sites. At least pick a plausible reason for closing the question. Better yet, don't close the question and tell the OP how to ask better. I am disappointed. $\endgroup$
    – Andrej Bauer
    May 22, 2022 at 20:58
  • $\begingroup$ Apologies for digging a three month old question from its grave. $\endgroup$
    – Andrej Bauer
    May 22, 2022 at 22:28

2 Answers 2

Reset to default
10
$\begingroup$

  1. Install the latest Lean 4 nightly through elan: in any bash-compatible shell, run:

    curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain leanprover/lean4:nightly

    On Windows, instead run in cmd

    curl -O --location  https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1  powershell -f elan-init.ps1 --default-toolchain leanprover/lean4:nightly  del elan-init.ps1

  2. Install VS Code.

  3. Open VS Code and install the lean4 extension.

  4. Create a new file with the extension .lean and add the following code:

    #eval Lean.versionString

    You should get a syntax-highlighted file with a "Lean Infoview" on the right that tells you the installed Lean version when placing your cursor on the last line.

  5. You are set up! You can now also run lake init foo from the command line to create a package, followed by lake build to get an executable version of your Lean program.

Note: Packages have to be opened using "File > Open Folder..." for imports to work. Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (Ctrl+Shift+X).
Note: This information may be outdated. Find out more here.
Source: Quickstart - Lean Manual
Improve this answer
$\endgroup$
3
  • $\begingroup$ Thanks, this is helpful. Is there a simple way to use Lean without installing VS code though? $\endgroup$
    – pxeger
    Feb 8, 2022 at 18:13
  • 5
    $\begingroup$ You can use Lean 4 from the command line like any other compiler, either via elan or from the release tarballs. There are Emacs and Neovim extensions as well. Currently there is no online version. $\endgroup$
    – Sebastian Ullrich
    Feb 8, 2022 at 18:20
  • 3
    $\begingroup$ For posterity I would note that Lean changes rapidly and these instructions might not be correct in a few months time. For a future visitor, I'd recommend double checking that the instructions on leanprover.github.io are the same. $\endgroup$
    – Jason Rute
    Feb 9, 2022 at 5:32
2
$\begingroup$

See this webpage for setup instructions.

Lean 4 has a separate repository.

(As an aside, I am not sure if this is the best place to ask such questions here that can be answered easily using a search engine while setting up the tone for the new community.)

Improve this answer
$\endgroup$
4
  • 2
    $\begingroup$ Search results can vary in reliability, and experience can be an asset. I guess we'll see how the Community judges such posts. $\endgroup$
    – hardmath
    Feb 8, 2022 at 19:47
  • $\begingroup$ Please do try to not base your answers around hyperlinks, in case the page gets removed / edited. $\endgroup$
    – taylor.2317
    Feb 8, 2022 at 20:04
  • 3
    $\begingroup$ IMHO there is no point in having the installation instructions duplicated here on the SE site as they could change/become outdated, while only the source repo/homepage is expected to keep that info updated. There is something to be said about what kind of knowledge is worth preserving and answering here especially if longevity is a concern. My larger point about the usefulness of the question remains. $\endgroup$
    – k4rtik
    Feb 8, 2022 at 22:12
  • 1
    $\begingroup$ I do think that questions whose best answer could be written as a primer on how to use a relevant tool should be welcome. They may help to develop the board as the place to check about proof assistant. $\endgroup$
    – mario
    Feb 9, 2022 at 18:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.