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

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.5.4. This template uses the sidebar heading navigation introduced in mdBook 0.5.

# install mdbook
cargo install mdbook --version 0.5.4

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_html. 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”.