Lean prover mathlib supporting tools.
Project description
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 git@github.com: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.
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for mathlibtools-0.0.6-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | b69c2767440a3828938c515fa4109345706cef13ecd357988a2f427e1b8b3cac |
|
MD5 | 0f92c57d41d807db1b48c50a7443a2dd |
|
BLAKE2b-256 | 1762d8b0c2ea94bb6e73d8d2bd4ea7c342b19df7d7cfd484a714cba5d9b0b724 |