Skip to content
Open
Changes from 2 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
11 changes: 10 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,5 +10,14 @@ The book's build has been tested with:
1. Lean 4 (see the version in lean-toolchain in examples/)
2. expect (tested with v5.45.4 but any version from the last decade should work)

To build the book, change to the "book" directory and run "lake exe fp-lean". After this, "book/out/html-multi" contains a multi-page Web version of the book.
To build the book, make sure that Lean and expect are installed, and

```bash
cd examples # pre-build examples first
lake build
lake build subverso-extract-mod
Comment thread
dimpase marked this conversation as resolved.
Outdated
cd ../book # now the book can be built
lake exe fp-lean
```
After this, `book/_out/html-multi` contains a multi-page Web version of the book.

Loading