Home

Awesome

mathlib-tools

Test on Linux Test on MacOS Test on Windows

This package contains leanproject, a supporting tool for Lean 3 mathlib.

This tool is fully obsolete and no longer has any relevance outside of historical studies. All Lean users are now expected to switch to Lean 4 which is not supported at all by this tool.

Installation

In principle, you should install those tools as part of the global Lean installation procedure recommended by the Lean community. Read what what remains of this section only if you want more details about this specific part of the procedure (the tools described here won't give you anything if Lean itself is not available).

Released version

pipx

The tools in this repository use python3, at least python 3.6, which is the oldest version of python supported by the python foundation. They can be installed using pip. The basic install command for the latest released version is thus:

python3 -m pip install mathlibtools

The above command may complain about permissions. This can be solved by running it as root, but this is not recommended in general. You can run python3 -m pip install --user mathlibtools to install it in your home directory (make sure that $HOME/.local/bin/ is on your shell path afterwards), but an even better way is to use pipx:

python3 -m pip install --user pipx
python3 -m pipx ensurepath
source ~/.profile
pipx install mathlibtools

macOS

If you are on macOS, the recommended way to install is via homebrew, which will handle the above Python installation for you:

brew install mathlibtools

NixOS

If you are using NixOS, you can also install mathlib tools using the bundled default.nix file:

nix-env -if https://github.com/leanprover-community/mathlib-tools/archive/master.tar.gz

Development version

If you want to use the latest development version, you can clone this repository, go to the repository folder, and run pip install ..

Usage

See the dedicated page on the community website. Recall this tool is fully obsolete and no longer has any relevance outside of historical studies. All Lean users are now expected to switch to Lean 4 which is not supported at all by this tool.