From b9b37b06fedf5573717d87a4143dcccd0fc162cc Mon Sep 17 00:00:00 2001 From: Dima Pasechnik Date: Sun, 26 Jul 2026 15:33:39 -0500 Subject: [PATCH 1/3] update local building instructions in README.md It will fix #283 --- README.md | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index f51ae094..72c68abb 100644 --- a/README.md +++ b/README.md @@ -10,5 +10,16 @@ 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 +lean --version # makes sure the needed here Lean version is installed +lake build +lake build subverso-extract-mod +cd ../book # now the book can be built +lean --version # makes sure the needed here Lean version is installed +lake exe fp-lean +``` +After this, `book/_out/html-multi` contains a multi-page Web version of the book. From ebbd186d3fe0bb2ef7267d58064cd453b0302c98 Mon Sep 17 00:00:00 2001 From: Dima Pasechnik Date: Mon, 27 Jul 2026 17:48:42 +0100 Subject: [PATCH 2/3] removing redundant commands in README.md Removed duplicate Lean version check from README. --- README.md | 2 -- 1 file changed, 2 deletions(-) diff --git a/README.md b/README.md index 72c68abb..b4a8357d 100644 --- a/README.md +++ b/README.md @@ -14,11 +14,9 @@ To build the book, make sure that Lean and expect are installed, and ```bash cd examples # pre-build examples first -lean --version # makes sure the needed here Lean version is installed lake build lake build subverso-extract-mod cd ../book # now the book can be built -lean --version # makes sure the needed here Lean version is installed lake exe fp-lean ``` After this, `book/_out/html-multi` contains a multi-page Web version of the book. From 23407ee9088551907aa4f0a7e3dc0f14dbdab564 Mon Sep 17 00:00:00 2001 From: Dima Pasechnik Date: Sat, 1 Aug 2026 14:35:08 -0500 Subject: [PATCH 3/3] remove an unneeded step Removed unnecessary command from README build instructions. --- README.md | 1 - 1 file changed, 1 deletion(-) diff --git a/README.md b/README.md index b4a8357d..28cec2e6 100644 --- a/README.md +++ b/README.md @@ -15,7 +15,6 @@ 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 cd ../book # now the book can be built lake exe fp-lean ```