From 3c2a48b60b7376372e6a5f845cc83bda8c842e2e Mon Sep 17 00:00:00 2001
From: pickleburger <pickleburger233@gmail.com>
Date: Fri, 16 Jul 2021 17:26:59 -0700
Subject: [PATCH] adding support to build PDFs for e-readers

---
 .gitignore     |  2 ++
 README.md      | 11 +++++++++--
 conf.py        |  2 +-
 lean_sphinx.py |  1 -
 4 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/.gitignore b/.gitignore
index 1cb9f3c..ea437be 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,5 @@
 *.olean
 /_target
 /leanpkg.path
+/__pycache__
+/_build
diff --git a/README.md b/README.md
index 092db01..db0f8b8 100644
--- a/README.md
+++ b/README.md
@@ -11,12 +11,19 @@ leanproject get git@github.com: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, ``avigad@cmu.edu``.
\ No newline at end of file
+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, ``avigad@cmu.edu``.
diff --git a/conf.py b/conf.py
index f4528b2..59103ec 100644
--- a/conf.py
+++ b/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').
     #
diff --git a/lean_sphinx.py b/lean_sphinx.py
index db4ef4b..499bfd0 100644
--- a/lean_sphinx.py
+++ b/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 import CodeBlock
 from sphinx.errors import SphinxError
 import os, os.path, fnmatch, subprocess
 import codecs