mathlibtools 0.0.8

Lean prover mathlib supporting tools.

mathlib-tools

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

Installation

Those tools use python3, at least python 3.5, which is the oldest version of python supported by the python foundation. They can be installed using pip. The basic install command is thus:

pip install mathlibtools

Depending on your setup you may need to preface this command with sudo, and pip may be called pip3 to distinguish it from its deprecated python2 version. For instance on Debian or Ubuntu, you can install pip using sudo apt install python3-pip and then run sudo pip3 install mathlibtools to install mathlib tools system-wide. If you want to use the latest development version, you can clone this repository, go to the repository folder, and run pip install ..

You also need to have elan already installed.

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

Basic usage

Everything is done using the leanproject command-line tool. You can use leanproject --help to get the list of available commands and options.

Getting an existing Lean project

The command to fetch an existing project from GitHub and make sure it includes a copy of mathlib ready to go is leanproject get name where name is either a git url, such as https://github.com/leanprover-community/tutorials.git or [e-mail]:leanprover-community/tutorials.git, or a GitHub project identifier such as leanprover-community/tutorials. The organization name defaults to leanprover-community so the simplest way get the tutorials project is to run:

leanproject get tutorials

You can specify a git branch name my_branch by appending :my_branch at the end of the specified name (without space). By default this branch should be an existing branch. Use leanproject get -b project_name:branch_name to get the project project_name and then create a branch branch_name and start working on it. You can also specify a target directory name as a second argument to the command.

Creating a new project

You can create a project in a new folder my_project by running:

leanproject new my_project

If you omit the argument, the project will be created directly inside the current folder. This new project will be using the latest version of Lean compatible with mathlib, and include a pre-built mathlib.

Building a project

Only mathlib itself comes with pre-built olean files. In order to build oleans in a project (which is needed for every non-trivial project in order to get decent interactive Lean speed), you can use:

leanproject build

Getting mathlib oleans

In an existing project depending on mathlib (or in mathlib itself), you can run:

leanproject get-mathlib-cache

to download a compiled mathlib at the commit currently specified in the project leanpkg.toml (see the next section if you want to update this commit and get the latest mathlib).

Upgrading mathlib

In an existing project depending on mathlib, you can upgrade to the latest mathlib version by running:

leanproject upgrade-mathlib

This can be abbreviated to leanproject up. By default, this will update the version of Lean used by this project to match the latest version compatible with mathlib. You can forbid such an upgrade by using leanproject --no-lean-upgrade upgrade-mathlib.

Advanced usage

Global mathlib install

If you want to use mathlib outside of a Lean project, you can run:

leanproject global-install

This will put a pre-compiled mathlib inside $HOME/.lean, the user-wide Lean project whose dependencies can be used by lean files outside projects. You can upgrade this project using:

leanproject global-upgrade

Adding mathlib to an existing project

If you already have a Lean project but it doesn't use mathlib yet, you can go to the project folder and run:

leanproject add-mathlib

By default, this will update the version of Lean used by this project to match the latest version compatible with mathlib. You can forbid such an upgrade by using leanproject --no-lean-upgrade add-mathlib.

Project olean cache

In any Lean project, it can be useful to store and retrieve olean files, especially if the project has several git branches. Storing oleans is done by:

leanproject mk-cache

while retrieving them is done by:

leanproject get-cache

One should note that, although olean files are indeed the primary target here, these commands actually store everything from the src and test folders of the current project.

If the project is mathlib itself, the caches will be stored in $HOME/.mathlib/. Otherwise, they will be stored in a folder _cache inside the project top-level folder. They are named after the corresponding git commit hash.

In general, using these commands in a dirty git repository (ie a repository whose working copy contains uncommitted changes) is a bad idea. You can do it anyway by running leanproject mk-cache --force or leanproject get-cache --force respectively.

The --force option will also overwrite existing cache for the current git revision.

When using get-cache inside the mathlib project, the local cache in $HOME/.mathlib/ will be searched first, before trying to download it. You can force download by running leanproject --force-download get-cache. This --force-download option can also be used with the upgrade-mathlib command.

Import graphs

If you want to generate a graph file showing your project import structure, you can run:

leanproject import-graph my_graph_file_name.suffix

where the suffix will determine the output format. It must be either dot or graphml or gexf, (or pdf, svg or png if graphviz is installed). If you want to restrict the graph to files leading to a certain file my_subproject/my_file.lean then you can run:

leanproject import-graph --to my_subproject.my_file my_graph_file_name.suffix

Dually, if you want to see all files using my_subproject/my_file.lean then you can run:

leanproject import-graph --from my_subproject.my_file my_graph_file_name.suffix

Combining --to and --from is possible.

Git hooks

If you want leanproject to fetch olean caches after each git checkout, and make olean caches after each git commmit in the current project, you can run:

leanproject hooks

Beware this will overwrite any post-checkout or post-commit file you might have in your project .git/hooks.

Cache download url handling

By default, leanproject will try to find mathlib olean files hosted on an Azure server. You permanently override the base url it uses by running:

leanproject set-url my_url

so that leanproject will look for caches at my_url/relevant_git_hash.tar.gz. You can override this base url for one invocation using leanprover --from-url my_url ... (where ... denotes a command and its arguments).

Time-stamps diagnostic and repairing

lean uses timestamps to decide whether an olean file should be recompiled. You can use:

leanproject check

to check that every olean from the core library and mathlib is more recent than its source. In case there is some issue, leanproject will propose to reset timestamps. Of course doing so is a good idea only if you are sure you didn't want to modify one of those lean files.

Troubleshooting

If leanproject ends with a mysterious error message, you can run it using the --debug flag, e.g. leanproject --debug new my_project. It will then probably output a python trace that you'll be able to paste in a GitHub issue or on Zulip.