adding support to build PDFs for e-readers

.gitignore

@@ -1,3 +1,5 @@
 *.olean
 /_target
 /leanpkg.path
+/__pycache__
+/_build

README.md

@@ -11,12 +11,19 @@ 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).
+The build requires python 3, xelatex, latexmk and some OTF fonts.
 
+On Ubuntu, you may install these dependencies by running
+
+```bash
+sudo apt install python3-venv texlive-xetex latexmk fonts-freefont-otf
 ```
+
+```bash
 make install-deps
 make html
 make latexpdf
+PAPER_SIZE=a5paper make latexpdf  # for e-readers
 ```
 
 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.
@@ -35,4 +42,4 @@ make leantest
 
 # How to contribute
 
-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]``.
+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]``.

conf.py

@@ -147,7 +147,7 @@
 latex_elements = {
     # The paper size ('letterpaper' or 'a4paper').
     #
-    # 'papersize': 'letterpaper',
+    'papersize': os.getenv('PAPER_SIZE') or 'letterpaper',
 
     # The font size ('10pt', '11pt' or '12pt').
     #

lean_sphinx.py

@@ -1,7 +1,6 @@
 from docutils import nodes
 from docutils.parsers.rst import Directive
 from sphinx.builders import Builder
-from sphinx.directives.code import CodeBlock
 from sphinx.errors import SphinxError
 import os, os.path, fnmatch, subprocess
 import codecs