leanprover / leanprover/fp-lean
Update build instructions in `README.md`
Open
Beginner friendly
Nobody has claimed this yet.
- Dominant language
- Lean
- Stars
- 192
- Forks
- 73
- PR merge metrics
- No merged PRs in 30d
Description
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.
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Update the build instructions in README.md using the suggested command sequence: build from examples/, run lake build and lake build subverso-extract-mod, then build the book. Verify that the instructions produce the multi-page Web version in _out/html-multi and that the documented paths match the repository layout.
Written by the indexing model from the issue text.
Assessment
- Domain
- build-system, documentation
- Issue type
- Documentation
- Difficulty
- 1/5
- Estimated time
- Under an hour
- Activity status
- Stale
- Clarity
- Clearly specified
- Newbie friendliness
- 78/100