Built using Sphinx and restructured text.
Make sure you have Lean installed. Use
leanproject get [email protected]:leanprover/theorem_proving_in_lean.git
to clone the repository and install the mathlib library.
The build requires python 3 (install python3-venv on ubuntu).
make install-deps
make html
make latexpdf
The call to make install-deps is only required the first time, and only if you want to use the bundled version of Sphinx and Pygments with improved syntax highlighting for Lean.
make leantest
./deploy.sh leanprover theorem_proving_in_lean
Pull requests with corrections are welcome. Please follow our commit conventions <https://github.com/leanprover/lean/blob/master/doc/commit_convention.md>. If you have questions about whether a change will be considered helpful, please contact Jeremy Avigad, [email protected].