Install Lean 3 on Windows

If you follow the official installation guide on Windows, Lean 4 will be installed automatically. However, if you want to install Lean 3 on Windows, you can follow the steps below.

These should be the minimum steps and I will try to keep them as clear as possible.

Prerequisites

I assume you have Visual Studio Code installed. (And possibly a web browser 🤷)

1. Download the latest release

Head to the Lean 3 repository on GitHub, find the latest release, and download the lean-<version>-windows.zip file.

At the moment, the latest release is Release v3.51.1, so I will download lean-3.51.1-windows.zip.

There may be a warning that says “This file is not commonly downloaded and may be dangerous”, I’m not sure why, but just keep downloading it. It should be safe as long as you are downloading it from the official repository.

Lean 3 is no longer officially maintained, the version we downloaded here is the community one.

If you want to get the last official version, which was released in 2019, you can download it from Release v3.4.2 · leanprover/lean3, the rest of the steps should be the same.

2. Unzip the file

Unzip the downloaded file to a directory of your choice. There should be three folders: bin, include, and lib respectively.

I stored them on my D drive, and also renamed the folder to lean. So now I have D:\lean\bin, D:\lean\include, and D:\lean\lib.

Optionally, you can test the lean.exe in the bin folder by running .\lean.exe --version in a command prompt or PowerShell:

PS D:\lean> cd bin
PS D:\lean\bin> ./lean --version
Lean (version 3.51.1, commit cce7990ea86a, Release)

3. Add the path to the environment variables

Add the path to the bin folder to the PATH environment variable.

1. On the lower left Start menu or search bar, type env and select Edit the system environment variables.
2. On the pop-up window, click the bottom right button Environment Variables….
3. On the System variables section, scroll down and find the path variable and double click it.
4. On the pop-up window, click the New button. You will need to input the path to lean‘s bin folder (Better to copy and paste it from the file explorer). In my case, it is D:\lean\bin.
5. Click OK on all the pop-up windows to save the changes.

This change may take a few minutes to take effect (and terminals will not recognize lean until you close and reopen them), or you can simply restart your computer to make sure it works.

4. Test the installation (optional)

Open a new command prompt or PowerShell window, and run lean --version again:

PowerShell 7.3.7
PS C:\Users\Lingkang> lean --version
Lean (version 3.51.1, commit cce7990ea86a, Release)
PS C:\Users\Lingkang> lean --help
Lean (version 3.51.1, commit cce7990ea86a, Release)
Miscellaneous:
  --help -h          display this message
  --version -v       display version number
  --githash          display the git commit hash number used to build this binary
  --run              executes the 'main' definition
...

5. Install the Lean extension for VS Code

At this point, you can use Lean 3 from the command prompt or PowerShell. However, if you want to use Lean 3 in VS Code, you will need to install the Lean extension for VS Code.

Open VS Code, navigate to the Extensions tab, and search for lean. Most of the time, the first result should be what we want. Click the Install button to install it.

The extension is supposed to find the installed Lean 3 automatically.

6. Done!

Up to now, the vanilla Lean 3 installation is done.

Create a new file with extension .lean, and you should see the Lean logo on the bottom-right corner of the window. Click it to start the Lean server if needed.

Try some basic Lean code:

#eval 1 + 1

or

#print "Hello world!"

The Lean Infoview window should pop up to provide plenty of information about the code, including the result.

7. Add project manager and package manager

However, if you want to use importation in Lean 3, for example import tactic, it is rather difficult to configure.

Lean 3 uses leanproject as the project manager and leanpkg as the package manager.

7.1. Get leanproject

The leanproject is written in Python and can be installed using pip.

1. Have Python 3 installed (Python 3.7 or later is recommended);
2. Have pip installed by running python -m pip install --upgrade pip in a command prompt or PowerShell (python or python3 doesn’t matter, as long as it is your desired version from the last step);
3. run pip3 install mathlibtools to install leanproject;

It is quite weird that the leanproject has name mathlibtools on PyPI, but it is the correct one.

Check the installation by running leanproject --version:

PS E:\Code\Lean> leanproject --version
leanproject, version 1.3.2

For your information, here is the (outdated) official Lean 3 mathlib installation guide: Installing mathlib supporting tools.

7.2. Create a new Lean 3 project

Features such as importation is only available in Lean 3 projects. To create a new Lean 3 project, run leanproject new <project-name> in a command prompt or PowerShell.

Now go to a desired directory to create a new Lean 3 project. I will use E:\Code\Lean as an example. If you cannot get results similar to the following, proceed to 7.3. Troubleshooting.

PS E:\Code\Lean> leanproject new proj
> cd proj
> git init -q
> git checkout -b lean-3.51.1
Switched to a new branch 'lean-3.51.1'
configuring proj 0.1
Adding mathlib
mathlib: cloning https://github.com/leanprover-community/mathlib to _target/deps/mathlib
> git clone https://github.com/leanprover-community/mathlib _target/deps/mathlib
Cloning into '_target/deps/mathlib'...
remote: Enumerating objects: 397855, done.
remote: Counting objects: 100% (1072/1072), done.
remote: Compressing objects: 100% (333/333), done.
remote: Total 397855 (delta 898), reused 818 (delta 736), pack-reused 396783
Receiving objects: 100% (397855/397855), 221.91 MiB | 13.97 MiB/s, done.
Resolving deltas: 100% (319147/319147), done.
Updating files: 100% (3572/3572), done.
> git checkout --detach 4e976107aa81b41822bd5bb2b15c90b1c8a2aa15    # in directory _target/deps/mathlib
HEAD is now at 4e976107aa feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976)
configuring proj 0.1
mathlib: trying to update _target/deps/mathlib to revision 4e976107aa81b41822bd5bb2b15c90b1c8a2aa15
> git checkout --detach 4e976107aa81b41822bd5bb2b15c90b1c8a2aa15    # in directory _target/deps/mathlib
HEAD is now at 4e976107aa feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (#16976)
Looking for mathlib oleans for 4e976107aa
  locally...
  Found local mathlib oleans
Located matching cache
Applying cache
  files extracted: 3220 [00:08, 379.06/s]

From this output, we can see a few things:

1. Initialized a new Lean project with git;
2. Cloned the whole mathlib repository;
3. Added mathlib as a dependency;
4. Load specified version pre-compiled mathlib (olean files);

If every thing looks fine, we can now open the project in VS Code and start enjoying full-powered Lean 3.

7.3. Troubleshooting

In most cases, things won’t go so smoothly. If you failed to get the above output, for example:

PS E:\Code\Lean> leanproject new proj
FileNotFoundError: [WinError 2] The system cannot find the file specified

Here we directly head to resolve the issue, some thoughts over it could be found at 8. Appendix.

In side the leanproject, leanpkg is actually called for help, so we first verify that leanpkg is installed correctly. Run leanpkg --version:

PowerShell 7.3.9
PS C:\Users\Lingkang> leanpkg --version
Lean package manager, version 3.51.1

Usage: leanpkg <command>

...

This should be runnable no matter what version of Lean 3 you are using, e.g., v3.4.2 or v3.51.1. If not, double check your footprint from step 1 to step 3.

Navigate to the bin folder of lean (here it is D:\lean\bin), create a new file named leanpkg.c with the following content:

#include <stdlib.h>
#include <string.h>

int main(int argc, char *argv[])
{
    char command[500];
    strcpy(command, "leanpkg.bat");
    for (int i = 1; i < argc; i++)
    {
        strcat(command, " ");
        strcat(command, argv[i]);
    }
    system(command);
    return 0;
}

Compile it with output leanpkg.exe:

gcc leanpkg.c -o leanpkg.exe

Now retry 7.2. Create a new Lean 3 project and it should work.

Here, we are basically cheating the python interpreter, see below for more details.

8. Appendix

Here are short explanations and some thoughts over the installation process.

8.1. Causes

If we run leanproject with debug flag, the error stack is quite horrifying:

PS E:\Code\Lean> leanproject --debug new proj
Traceback (most recent call last):
  File "D:\Python3.10\lib\runpy.py", line 196, in _run_module_as_main
    return _run_code(code, main_globals, None,
  File "D:\Python3.10\lib\runpy.py", line 86, in _run_code
    exec(code, run_globals)
  File "D:\Python3.10\Scripts\leanproject.exe\__main__.py", line 7, in <
  File "D:\Python3.10\lib\site-packages\mathlibtools\leanproject.py", li
    handle_exception(err, str(err))
  File "D:\Python3.10\lib\site-packages\mathlibtools\leanproject.py", li
    raise exc
  File "D:\Python3.10\lib\site-packages\mathlibtools\leanproject.py", li
    cli() # pylint: disable=no-value-for-parameter
  File "D:\Python3.10\lib\site-packages\click\core.py", line 716, in __c
    return self.main(*args, **kwargs)
  File "D:\Python3.10\lib\site-packages\click\core.py", line 696, in mai
    rv = self.invoke(ctx)
  File "D:\Python3.10\lib\site-packages\click\core.py", line 1060, in in
    return _process_result(sub_ctx.command.invoke(sub_ctx))
  File "D:\Python3.10\lib\site-packages\click\core.py", line 889, in inv
    return ctx.invoke(self.callback, **ctx.params)
  File "D:\Python3.10\lib\site-packages\click\core.py", line 534, in inv
  File "D:\Python3.10\lib\site-packages\mathlibtools\lib.py", line 700, in new
    subprocess.run(['leanpkg', 'new', str(path)], check=True)
  File "D:\Python3.10\lib\subprocess.py", line 501, in run
    with Popen(*popenargs, **kwargs) as process:
  File "D:\Python3.10\lib\subprocess.py", line 966, in __init__
    self._execute_child(args, executable, preexec_fn, close_fds,
  File "D:\Python3.10\lib\subprocess.py", line 1435, in _execute_child
    hp, ht, pid, tid = _winapi.CreateProcess(executable, args,
FileNotFoundError: [WinError 2] The system cannot find the file specified

We can see that the error is caused by subprocess.run(['leanpkg', 'new', str(path)], check=True) in mathlibtools/lib.py, and almost everywhere calling leanpkg will cause the same error.

Source: mathlib-tools/mathlibtools/lib.py at master · leanprover-community/mathlib-tools

To abstract away irrelevant details, we can simplify the code to:

import subprocess
from typing import List

def run(args: List[str]) -> str:
    return subprocess.run(
        args, stdout=subprocess.PIPE, check=False
    ).stdout.decode()

if __name__ == "__main__":
    print(run(["leanpkg", "--version"]))
    # print(run(["leanpkg.bat", "--version"]))

Running it will cause the same error that we got from leanproject:

Traceback (most recent call last):
  File "E:\Code\Lean\test.py", line 13, in <module>
    print(run(["leanpkg", "--version"]))
  File "E:\Code\Lean\test.py", line 6, in run
    return subprocess.run(
  File "D:\Python3.10\lib\subprocess.py", line 501, in run
    with Popen(*popenargs, **kwargs) as process:
  File "D:\Python3.10\lib\subprocess.py", line 966, in __init__
    self._execute_child(args, executable, preexec_fn, close_fds,
  File "D:\Python3.10\lib\subprocess.py", line 1435, in _execute_child
    hp, ht, pid, tid = _winapi.CreateProcess(executable, args,
FileNotFoundError: [WinError 2] The system cannot find the file specified

And if we change it from leanpkg to leanpkg.bat, the snippet will work:

Lean package manager, version 3.51.1

Usage: leanpkg <command>

...

This is what happened: under the bin folder of lean, we can see that there are two leanpkg files: leanpkg and leanpkg.bat. The first one is a shell script (not sure why put a shell script in a Windows release), and the second one is CMD batch script. When we run leanpkg --version on the command prompt or PowerShell, Windows is smart enough to run the batch script. This can be verified by running Get-Command leanpkg in PowerShell, and the output will specify which file is used for the command.

CommandType	Name	Version	Source
Application	leanpkg.bat	0.0.0.0	D:\lean\bin\leanpkg.bat

Both Get-Command leanpkg and Get-Command leanpkg.bat will return the same result.

However, when we run it in Python, it will try to find an executable exactly named as leanpkg, and it will fail. It can only success to it when we specify the extension leanpkg.bat.

8.2. Solutions

So the solution is quite simple, we can either:

1. Change the Python source code to use leanpkg.bat instead of leanpkg;
2. Make a kind of mapping or alias that maps leanpkg to leanpkg.bat;
3. Create a new executable named leanpkg that calls leanpkg.bat under the hood;

The first solution is quite straightforward, but modifying the source code might cause unexpected issues, and there are many places to modify.

The second solution may work, but in real experiment, techniques such as symbolic link or hard link do not help.

The Third solution, as what we did in 7.3. Troubleshooting, is to create a new executable named leanpkg.exe that passes everything to leanpkg.bat. A little bit tricky.

8.3. Questions

Even though this is a feasible way, I still not sure why the procedure would go so painful.

The leanproject (or mathlibtools) was marked obsolete just on August this year, and its CI tested on all major platforms, including Windows, with different Python versions from 3.7 to 3.11. There is no reason that it would be broken so soon.

And also, the transition from Lean 3 to Lean 4 sucks. The official site becomes a mixture of them, and toolchains’ documentation nearly not exist.

References

1. Installing Lean 4 on Windows
2. Installing Lean 3 and mathlib on Windows
3. leanprover-community/lean: Lean Theorem Prover
4. Lean community
5. How to: Add Tool Locations to the PATH Environment Variable | Microsoft Learn
6. lean - Visual Studio Marketplace
7. leanprover/vscode-lean: Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 (‘lean4’ in the extensions menu) for the Lean 4 language.
8. 1. Using Lean — The Lean Reference Manual 3.3.0 documentation
9. The Lean tool chain
10. Using leanproject
11. mathlibtools · PyPI
12. leanprover-community/mathlib-tools: Development tools for https://github.com/leanprover-community/mathlib
13. leanprover-community/mathlib: Lean 3’s obsolete mathematical components library: please use mathlib4