Skip to content

Commit

Permalink
adding support to build PDFs for e-readers
Browse files Browse the repository at this point in the history
  • Loading branch information
pickleburger committed Jul 17, 2021
1 parent 2a00e9a commit f3f21e8
Show file tree
Hide file tree
Showing 4 changed files with 12 additions and 4 deletions.
2 changes: 2 additions & 0 deletions .gitignore
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
*.olean
/_target
/leanpkg.path
/__pycache__
/_build
11 changes: 9 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 free serif fonts (in OTF format).

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.
Expand All @@ -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]``.
2 changes: 1 addition & 1 deletion conf.py
Original file line number Diff line number Diff line change
Expand Up @@ -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').
#
Expand Down
1 change: 0 additions & 1 deletion lean_sphinx.py
Original file line number Diff line number Diff line change
@@ -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
Expand Down

0 comments on commit f3f21e8

Please sign in to comment.