From fa8c9d771aa6a06e25468c92b049fecc3e482b99 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 7 Oct 2023 21:07:55 +0200 Subject: [PATCH] feat: Always document the transitive closure of a module --- README.md | 15 ++++++++++----- lakefile.lean | 3 +++ 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/README.md b/README.md index e6097cd..a5df110 100644 --- a/README.md +++ b/README.md @@ -14,12 +14,17 @@ Then update your dependencies: lake -Kenv=dev update ``` -Then you can generate documentation for an entire library using: +Then you can generate documentation for an entire library and all files imported +by that library using: ``` lake -Kenv=dev build Test:docs ``` -If you have multiple libraries you want to generate documentation for -the recommended way right now is to run it for each library. +If you have multiple libraries you want to generate full documentation for: +``` +lake -Kenv=dev build Test:docs Foo:docs +``` +Note that doc-gen currently always generates documentation for `Lean`, `Init` +and `Lake` in addition to the provided targets. ## Development of doc-gen4 You can build docs using a modified `doc-gen4` as follows: Replace the `from git "..." @ "main"` in the `lakefile.lean` with just `from "..."` using the path to the modified version of `doc-gen4`. E.g. if the @@ -31,10 +36,10 @@ require «doc-gen4» from "../doc-gen4" The root of the built docs will be `build/docs/index.html`. However, due to the "Same Origin Policy", the generated website will be partially broken if you just open the generated html files in your browser. You -need to serve them from a proper http server for it to work. An easy way to do that is to run +need to serve them from a proper http server for it to work. An easy way to do that is to run `python3 -m http.server` from the `build/docs` directory. -Note that if you modify the `.js` or `.css` files in doc-gen4, they won't necessarily be copied over when +Note that if you modify the `.js` or `.css` files in doc-gen4, they won't necessarily be copied over when you rebuild the documentation. You can manually copy the changes to the `build/docs` directory to make sure the changes appear, or just do a full recompilation (`lake clean` and `lake build` inside the `doc-gen4` directory.) diff --git a/lakefile.lean b/lakefile.lean index bc1d608..0a3027f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -29,6 +29,9 @@ module_facet docs (mod) : FilePath := do let exeJob ← docGen4.exe.fetch let modJob ← mod.leanArts.fetch let buildDir := (← getWorkspace).root.buildDir + -- Build all documentation imported modules + let imports ← mod.imports.fetch + imports.forM fun mod => discard <| fetch <| mod.facet `docs let docFile := mod.filePath (buildDir / "doc") "html" exeJob.bindAsync fun exeFile exeTrace => do modJob.bindSync fun _ modTrace => do