A cheap hack to get Lean and mathlib running on a Windows 10 machine

[last updated 25th Oct 2018]

These instructions are specific to people who want to get Lean and mathlib running on a Windows 10 machine. They are guaranteed not to work on any other OS. This is a dirty hack. Advantages: you don’t need to install msys2 or git. Disadvantages — you get a random snapshot of mathlib from October 2018 and it won’t upgrade until someone else does some work. Also this method is unsupported by the devs (you are using .olean files compiled on another machine) so use it at your own risk (but I’ve been informally told by devs that it should work fine, and no undergraduates have reported any problems).

1) Point your browser at http://wwwf.imperial.ac.uk/~buzzard/xena/Xena.zip and download this zip file; save it on the desktop (or somewhere else if you want to deviate from these instructions).

[Technical details: this file contains a binary of Lean 3.4.2 nightly, and a small sample project with mathlib as a dependency, together with all the .olean files for mathlib and lean, so nothing needs compiling]

2) Extract everything (to the desktop!). On my Windows 10 machine you can right click on the zip file, then select 7-Zip -> Extract here.

3) If you’re at Imperial in the MLC then go to the software hub and fire up Visual Studio Code. If you’re not, install Visual Studio Code. Note: *not* “Visual Studio”, and *not* “Visual Studio Enterprise”, and not any of the other things which Microsoft in their wisdom have decided to call Visual Studio Something. Visual Studio Code. Furthermore, if you already installed it a while ago, click “Help -> Check for updates” because (a) a version from a few months ago freezes Windows 10 when you use Lean with it and (b) the way step 5 works in VS Code changed in September 2018 and I’m documenting the new version here.

4) Within Visual Studio Code, install the Lean extension by clicking on the weird square icon in the tall thin panel on the left of the Visual Studio Code window (the one underneath the “no insect” icon), searching for lean and then installing the extension called Lean. Once you’ve installed it, click the little blue Reload icon nearby.

5) We now need to tell Visual Studio Code where Lean is (it’s on your desktop). So within Visual Studio Code, click File -> Preferences -> Settings, and then in the “Search Settings” box type lean. Near or at the top of the search results you will see “Lean: Executable path. Path to the Lean executable to use” and underneath there’s a box which probably just says “lean” on a fresh install. This is wrong — we need a full path to your lean.exe here. Getting this right is hopefully the only thing now standing between you and having Lean+mathlib running on your Windows 10 machine.

6) If you dumped that zip file on your desktop, and your Windows login is “john”, and you’re in the MLC, then the contents of that box need to look something like


(you’ll have to right click on the Xena directory and click “properties” and look at the location to get the first bit right). If you’re not in the MLC it will look something like


If your login is not “john” then change as appropriate. If your login is “Ryan Smith” you can *try*

C:\Users\Ryan Smith\Desktop\Xena\lean-3.4.2-nightly-2018-08-23-windows\bin\lean.exe"

but I did not test this. This should not be an issue for MLC users. I have heard informally that this works (and is hence a workaround for the spaces in path names issue which leanpkg currently has). If you didn’t put xena.zip on your desktop then change as appropriate — VS Code needs the full path to lean.exe with backslashes (and possibly spaces) quoted.

Once the line says what you think it should say, you don’t need to save — this happens automatically.

7) Now comes the moment of truth. In Visual Studio Code, click File -> Open Folder, then find your desktop and the Xena directory [note: *not* the Xena zip file] and then go in this directory and click *once* on my_project (so it says “Folder: my project”) and then click “select folder”.

8) On the left of the Visual Studio Code window you’ll now see “My Project”. Click on src to open it up, then click on test.lean.

9) Wait for a few seconds. If some orange bars appear near the code, pop the champagne. Wait for the orange bars to disappear (Lean is doing some initial compiling).

10) If there are no red underlines, things are probably working. change 2+2=4 to 2+2=5 and check that an error occurs (a red underline will appear). Then change it back and make sure the error disappears. If you’ve got this far — you’re ready to go!