fp-lean icon indicating copy to clipboard operation
fp-lean copied to clipboard

Update build instructions in `README.md`

Open euprunin opened this issue 7 months ago • 0 comments

Suggested change:

diff --git a/README.md b/README.md
index f51ae09..c54499e 100644
--- a/README.md
+++ b/README.md
@@ -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, run:

+```
+% cd examples/
+% lake build
+% lake build subverso-extract-mod
+% cd ../book/
+% lake exe fp-lean
+```
+
+After this, "_out/html-multi" contains a multi-page Web version of the book.

euprunin avatar Jun 04 '25 20:06 euprunin