Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 10 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,16 @@ To build this manual, first install the fork via
```bash
cargo install --git https://github.com/leanprover/mdBook mdbook
```

To build a PDF, we use [mdbook-pdf](https://github.com/HollowMan6/mdbook-pdf), which requires Chrome (or Edge on Windows) to be installed first. See the README of mdbook-pdf.

```bash
cargo install --git https://github.com/HollowMan6/mdbook-pdf.git
```

and add the appropriate incantations to `book.toml` (as per the mdbook-pdf README).


Then use e.g. [`mdbook watch`](https://rust-lang.github.io/mdBook/cli/watch.html) in the root folder:
```bash
mdbook watch --open # opens the output in `out/` in your default browser
Expand Down
Binary file added book.pdf
Binary file not shown.
5 changes: 5 additions & 0 deletions book.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,3 +13,8 @@ git-repository-url = "https://github.com/leanprover/theorem_proving_in_lean4"

[output.html.playground.boring-prefixes]
lean = "# "

[output.html.print]
enable = true

[output.pdf]