Installing Lean (and VSCode) on Windows from scratch

Here are some notes, but honestly I am no expert. This just worked for me though. Some hints for Mac users are in the comments below.

  • Step 1: Install Lean.

Go to

https://github.com/leanprover/lean/releases/tag/v3.3.0

and scroll to the very bottom.

Download lean-3.3.0-windows.zip and put it somewhere you can remember (e.g. C:\Users\Chris) because you’ll need to know where it is later on.

Extract the zip file. It will create a directory.

Lean is now installed but you might have no reasonable way of interacting with it. Poke around in the directory if you like — find a subdirectory called bin and in there you’ll probably find a file called lean.exe. You’ll need to know exactly where that file is located in your system when we get to Step 4.

  • Step 2: Install Visual Studio Code.

Google for Visual Studio Code (or VSCode — it’s the same thing) and install it. Then run it.

  • Step 3: Install lean extension for VSCode.

In the vertical bar on the left in Visual Studio Code, hover over the symbols until you find that one that says “Extensions” (it’s square, it’s at the bottom) and click on it.

A list of popular extensions appears. Type lean in the search bar just above it. It should find an extension just called “lean”. Click “Install”.

  • Step 4: Tell the VSCode Lean extension where Lean is.

In VSCode, go to File -> Preferences -> Settings, and on the right hand box titled Place your settings here…, make it look like this:

{
"lean.executablePath": "[wherever you put the lean-3.3.0-windows directory]\\bin\\lean.exe"
}

e.g.

{
"lean.executablePath": "C:\\Users\\Chris\\lean-3.3.0-windows\\bin\\lean.exe"
}

or, if you’re using the computers in the MLC,

{
"lean.executablePath": "C:\\Xena\\lean\\bin\\lean.exe"
}

Make sure that you type in the exact full path to the program lean.exe. Make sure you use two backslashes instead of one (if some letters are red this is bad, if they’re orange this is OK). I would also recommend that you make sure that there are no spaces anywhere in the full path (unless you know enough JSON to know what you’re doing). I still have never seen anyone who has managed to get lean working in VS Code after they installed the Lean executable somewhere in C:\Program Files; if anyone works this out then do let me know. [Edit: see a comment below, where someone does manage to do this by changing Windows’ path variable.]

You might now have to click “reload” on the lean extension on the left.

  • Step 5: Try it.

Create a file called test.lean (e.g. use Windows file explorer in a directory and right click, make a new text document and then rename it test.lean). My memory is that by default Windows suppresses file extensions, so try and make sure it’s not called test.lean.txt.

Now go to VSCode and open test.lean (File -> Open File)

Now try typing something like

#eval 1+1

If VSCode complains that it can’t find lean.exe, you’ve probably got that lean.executablePath bit wrong. If eval gets underlined in green, you’re probably good to go. In the top right there are some symbols, and hovering over them you’ll see one that says “Display messages”. Click on that and if you’re lucky there might be a 2 there.

If something doesn’t work — google might be a better option than asking me!

Problems people had, and solutions which sometimes worked.

You can restart Lean in VS Code with Ctrl-Shift-P and then typing Lean: restart in the window which just appeared (or selecting Lean: restart when it appears as you begin typing). This sometimes gets things working.

If you cut and pasted the lean.executablePath stuff from some earlier version of this web page, then I’m really sorry, I could have screwed you up, because for technical reasons wordpress gave me the wrong kind of quotes. Delete all the quotation marks in that line, and replace them with usual quotation marks, and this might help VS Code to run Lean.

Windows may be hiding file extensions by default. If Lean is not running on your test.lean file — are you 100 percent sure it’s called test.lean and not test.lean.txt? There’s a way to switch this off which varies with which version of Windows you’re using. Google for help. A symptom of this is that Windows’ file explorer will tell you that the file it’s telling you is called test.lean is actually a text file, and comes with a free text file icon (rather than the “I don’t have a clue what kind of file this is” icon, which is the one we’re looking for).

It’s working, now can I please have the real numbers?

You need to install not just Lean but also the maths library mathlib. The library is here and, once you’ve downloaded it, the only issue is figuring out how to tell VS Code about it. If import analysis.real works, you’re good to go. Someone much wiser than me once told me the below about paths:

Lean will use
1) the paths in the LEAN_PATH envvar, or else
2) the paths in the closest surrounding leanpkg.path file, or else
3) the default “current directory + core lib”
That should work just as well on Windows, hopefully

  • Notes on mathlib.

Open C:\Xena (the directory not a file) in VS Code and create a leanpkg.path in that directory, containing the lines

builtin_path
path mathlib-master
path xena/xena-master

Something like this should work. Note to self — chase up on Thursday.

Advertisements

About xenaproject

The Xena Project aims to get mathematics undergraduates at Imperial College trained in the art of formalising mathematics on a computer.
This entry was posted in Technical assistance. Bookmark the permalink.

4 Responses to Installing Lean (and VSCode) on Windows from scratch

  1. Philip Thiede says:

    I got an error when installing it on macOS, something along the lines of that it couldn’t run “lean –version”. This is what I did to fix it!

    1. Install homebrew from https://brew.sh.
    2. Install the program gmp using homebrew, by typing “brew install gmp” into your terminal.

    I figured this out by searching online, and following the directions from this post on StackOverflow: https://stackoverflow.com/questions/26555902/ruby-v-dyld-library-not-loaded-usr-local-lib-libgmp-10-dylib

    It worked for me and some other people using macs during the first meeting (Thurs 5th Oct)!

    Liked by 1 person

  2. Elliott Macneil says:

    If you are trying to install Lean on macOS using the steps outlined above (in addition to Philip Thiede’s comment) and you’re still stuck on step 4 (“Tell the VSCode Lean extension where Lean is”) then be aware of the type of quotation marks in this webpage.

    If you’re copying the executable path from the webpage, then the use of the ‘curly’ “” quotation marks will not work. Instead, replace this with ‘straight’ “” quotation marks, and this should work now.

    Like

  3. xenaproject says:

    I made an html error. I think they’re fixed now. Thanks Elliott.

    Like

  4. xenaproject says:

    Peiran Wu sent me a very helpful email, saying that they had managed to get VS Code working with Lean installed in C:\Program Files (i.e. a path name with a space in). Their trick was that instead of setting “lean.executablePath” in the VS Code User Settings, one can add the directory of the Lean binary to the system path by modifying the Windows system environment variable. I’m sure google will be able to tell you how to change system environment variables in any recent version of Windows, so this sounds like a great solution.

    Thanks Peiran!

    Like

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s