Lean Book

Lean Book is the mdbook template configured for the Lean Project. Intended for use in writing textbooks and documentation in Lean.

Lean Book has a variety of features.

Syntax Highlighting for Lean Code

Lean syntax highlighting works in this book. Here is an example of Lean code block.

variable {P Q : Prop}

example : P → (P ∨ Q) := by
  intro hP
  apply Or.inl
  exact hP

Run Lean4 Code Block

All Lean code blocks in this book have a button that jumps to the Lean Playground.

Jump to Lean Playground from any page

Jump to the Lean4 Playground by clicking on the play button in the top right corner of a page.

Table of Contents

Automatically add a table of contents to each page.

Easy Code Management

The markdown files in this book are generated from Lean code using mdgen. There is no need to maintain separately the code examples and the text.

Automatically update Lean version

The lean-update action is configured in this repository, which periodically attempts to update the version of Lean and its libraries.

The mdbook does not support searches in languages other than English, but this book does support searches in other languages (e.g. Japanese)!

MathJax

You can use MathJax in this book. For example, $a^2 + b^2 = c^2$.

$$ ζ (s) = \sum_{n=1}^{\infty} \frac{1}{n^s} $$

Mdbook Admonish

Info

mdbook-admonish is preinstalled!

How to Use

Basic Setup

Install git, Lean and mdbook. The installation of git and Lean is not described here.

I recommend using mdbook version 0.4.35. Otherwise, the table of contents layout may be broken.

# install mdbook
cargo install mdbook --version 0.4.35

clone this repository

Clone this repository and remove it from origin. To do so, run the following command in your terminal.

mkdir your-book-dir
cd your-book-dir
git clone https://github.com/Seasawher/lean-book.git .
git remote remove origin

Do not fork to use this repository. Fork only when you want to submit a PR.

Don't select "Use this template" on GitHub UI if you want your repository to be indexed by Reservoir.

Customize as you need

Please modify the following items to suit your project:

  • Change the package name «Lean Book» as you like. And run lake update.
  • The libname LeanBook and the directory name LeanBook should not be changed. If you change it, do not forget to change assets/filePlay.js as well.
  • Edit book.toml as you need. There are many things to edit, but the following are especially important.
    • Change the site_url in book.toml to your GitHub page's URL. This is required to display 404 page correctly.
    • Change the edit-url-template in book.toml to reflect the URL of your GitHub repository. This is required to use the "jump to Lean 4 Web" feature.
  • Edit .lycheeignore file. This controls which URL is ignored by the link checker in CI.

How to write

Writing a book can be done in the same way as writing in mdbook.

  1. After updating the Lean file, don't forget to run lake run build. This will generate markdown files with mdgen, HTML files with mdbook.
  2. Run mdbook serve --open to see the preview.

Publish

Push to GitHub. The workflow for deploy has already been set up, so you can publish it as a web page by enabling deploy to GitHub Pages via GitHub Action from the repository settings.

Note that:

  • Your repository must be public. If you are developing in a private repository and are tired of the deploy action failing, temporarily disable the action from running.
  • When deploying to GitHub Pages, please select "github actions" instead of "deploy from a branch".