Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

PDF Generation

Lean Book can generate a PDF version of the book in addition to the HTML version.

Requirements

PDF generation requires the following commands to be installed and available in your PATH. The PDF workflow uses these versions:

Using the same versions locally is recommended to reproduce the PDF generated by GitHub Action. You can install the required mdBook packages with Cargo:

cargo install mdbook --version 0.5.4 --locked
cargo install mdbook-pandoc --version 0.11.1 --locked

You can check that they are available by running:

mdbook --version
mdbook-pandoc --version
pandoc --version
typst --version

The default PDF configuration uses the Arial and Cascadia Mono fonts. Install these fonts or change the font settings described below if they are not available on your system.

Build the PDF

Run the following command from the root directory of the project:

lake run build_pdf

This command first generates the Markdown files in booksrc with mdgen. Then mdbook-pandoc converts the book to Typst, and Typst compiles it into a PDF. The generated file is written to typst/book.pdf.

Customize the PDF

PDF-specific settings are stored in typst/pdf-output.json. Edit this file to change settings such as:

  • The title and authors displayed in the PDF
  • The paper size and margins
  • The body and code fonts
  • The font size
  • The output file path

The Typst template is stored in typst/book.typ. Edit this file when you want to customize the title page, page layout, heading styles, code blocks, or other visual details.

Lean syntax highlighting is configured by typst/lean.sublime-syntax and typst/lean-light.tmTheme.