This is the source code for Mathematics in Lean.
Our build process is rudimentary and not ready for prime time, but it is fairly
convenient to use. Most of the source is written directly in the .lean files
in MIL using some simple markup. The Python script
MIL/mkall.sh then generates the .rst source for the textbook and
an exercise file and a solution file for each section.
To edit the Lean files, you need to have Lean 4 installed. The command
lake exe cache get
should fetch the relevant compiled version of mathlib4, at which point
you should be able to work with the files. lake update will update the manifest
to the most recent version of mathlib, which may require fixing anything that breaks.
To build the textbook, you need to have
Sphinx and ReadTheDocs installed
and regex installed. In simple cases, this means running some variant of pip install sphinx sphinx-rtd-theme regex.
The following files are maintained by hand:
- The file
source/index.rstshould have an entry for each chapter. - For each chapter, there should be a
.rstfile insource. It should include each of the sections. - For each section, there should be a
.leanfile in the appropriate place inMIL. - Each section should have a corresponding line in
MIL/mkall.sh.
Is everything is set up right, the command
MIL/mkall.sh
from the top level should build the restructured text files, the exercise files, and the solutions. The command
make html
builds the html textbook and puts it in the build folder. The command
make latexpdf
builds the pdf textbook instead.
The script deploy.sh is used to deploy everything (the textbook and the
user's version of the example and solution files) to an arbitrary repository, set up to use the gh-pages branch
to display the html. Specifically, we use the following:
./deploy.sh leanprover-community mathematics_in_lean
The textbook is still a work in progress, but feedback and corrections are welcome. You can open a pull request, find us on the Lean Zulip channel, or contact any of us by email.