diff --git a/README.md b/README.md
index f99690ac..20521332 100644
--- a/README.md
+++ b/README.md
@@ -6,5 +6,18 @@ The original version of the book was released by Microsoft Corporation in 2023 u
 
 Generally speaking, the code in this repository is not intended to work on all computers. The purpose of the repository is to produce the book's HTML for readers. In particular, it probably only works on Unix-like systems, due to the way that the built-in tests exercise the programs built in the book. Building the book requires at least a C compiler available as `cc`, with the POSIX headers, and a Unix-like shell.
 
-To build the book, change to the [`book`](book/) directory and run `lake exe fp-lean`. After this, `book/out/html-multi` contains a multi-page Web version of the book.
+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, make sure that Lean and expect are installed, and 
+
+```bash
+cd examples    # pre-build examples first
+lake build
+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.