Sphinx setup for Mathematics in Lean

Stream: Lean for teaching

[Matthew Hertz]

Hi everyone. I am a student of @Heather Macbeth and I am trying to compile a sphinx repository made by @Jeremy Avigad (https://github.com/avigad/mathematics_in_lean_source) but I am running into a problem. When I build the html files for the project, some of the lean files are not being found through the mkdoc script. Therefore I will get an error such as:

source/02_Basics.rst:11: CRITICAL: Problems with "include" directive path:
InputError: [Errno 2] No such file or directory: 'source/02_Basics/01_Calculating.inc'.

I tried fiddling with the mkdoc file and I can get some of the lean file to appear, but then the regular expressions fail to parse some of the lean code and latex.
Screen-Shot-2022-06-11-at-4.53.00-PM.png

Any help would be greatly appreciated. Thanks!

[Jeremy Avigad]

Hi, Matthew. I am sorry that the process is not well documented. It's not really designed for public use. Improving it and documenting it is on my very long list of things to do.

To build e.g. the html, the following should work, from the top level folder:

lean_source/mkall.sh
make html

If you want the pdf instead, change the second line to make latexpdf. Most of the source material is in the directory lean_source. The first line runs a Python script to generate the Sphinx source, the exercises, and the solutions from the Lean source files.

To start with, you need Sphinx and the readthedocs template:

https://sphinx-rtd-tutorial.readthedocs.io/en/latest/install.html

Adding a new section requires adding it to the chapter under source, adding it to the list of things to complie in mkall.sh, and then putting the source code in the right place under lean_source.

Adding a new chapter requires creating a new .rst file under source, and adding it to index.rst.

Creating your own textbook follows suit. The file index.rst should list all the chapters, there should be a .rst file under source for each chapter that imports all the sections, there should be a Lean file in lean_source corresponding to each section, and mkall.sh should list all the sections.

[Jeremy Avigad]

P.S. The file README.md is left over from previous incarnations. I'll update it now with the information above.

[Matthew Hertz]

It's working now, thank you so much for the help.