Xena

Installing Lean (and VSCode) on Windows from scratch

Advertisements

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.

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.

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

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”.

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.

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

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