From 8d6376c01986508f763106d9c809e6ceed498a49 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 21 Jul 2022 18:32:09 +0200 Subject: [PATCH] doc: Document the staged build --- README.md | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/README.md b/README.md index 4ca3074..758f1bd 100644 --- a/README.md +++ b/README.md @@ -18,3 +18,34 @@ You could e.g. host the files locally with the built-in Python webserver: ```sh $ cd build/doc && python -m http.server ``` + +### Multi stage +You can also use `doc-gen4` in multiple separate stages to generate the whole documentation. +For example `mathlib4` consists out of 4 modules, the 3 Lean compiler ones and itself: +- `Init` +- `Std` +- `Lean` +- `Mathlib` +The first stage in the build is: +```sh +$ doc-gen4 init Mathlib +``` +We already have to pass the `Mathlib` top level module here so it can generate the +navbar on the left hand side properly in the index and 404 HTML pages. +Next we can run the actual build stages: +1. `doc-gen4 single Init Mathlib` +2. `doc-gen4 single Std Mathlib` +3. `doc-gen4 single Lean Mathlib` +4. `doc-gen4 single Mathlib Mathlib` +We have to pass `Mathlib` here again for the same reason, the single command +will only generate documentation for its first argument module. Furthermore +one can use the `--ink` flag here to also generate LeanInk documentation in addition. +The last stage is the finalize one which zips up some information relevant for +the search: +```sh +$ doc-gen4 finalize +``` +Now `build/doc` should contain the same files with the same context as if one had run +``` +$ doc-gen4 Mathlib +```