diff --git a/.gitignore b/.gitignore index 5bff016..bcfc2e6 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,3 @@ -/build +/.lake/* /lake-packages/* lakefile.olean diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index bb48a0f..e6c4074 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -11,7 +11,7 @@ namespace DocGen4.Output open scoped DocGen4.Jsx open Lean System Widget Elab Process -def basePath := FilePath.mk "." / "build" / "doc" +def basePath := FilePath.mk "." / ".lake" / "build" / "doc" def srcBasePath := basePath / "src" def declarationsBasePath := basePath / "declarations" diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean index c6255d5..14cfdac 100644 --- a/DocGen4/Process/DefinitionInfo.lean +++ b/DocGen4/Process/DefinitionInfo.lean @@ -36,8 +36,14 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := let info ← Info.ofConstantVal v.toConstantVal let isUnsafe := v.safety == DefinitionSafety.unsafe let isNonComputable := isNoncomputable (← getEnv) v.name + try - let eqs? ← getEqnsFor? v.name + -- Temporary workaround until + -- https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/maxRecDepth.20in.20getEqnsFor.3F/near/402917295 + -- is adddressed + let eqs? : Option (Array Name) := none + -- let eqs? ← getEqnsFor? v.name + match eqs? with | some eqs => let equations ← eqs.mapM processEq diff --git a/README.md b/README.md index a5df110..8564c36 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# doc-gen4 +# `doc-gen4` Document Generator for Lean 4 ## Usage @@ -11,21 +11,54 @@ require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main" Then update your dependencies: ``` -lake -Kenv=dev update +lake -R -Kenv=dev update ``` Then you can generate documentation for an entire library and all files imported by that library using: ``` -lake -Kenv=dev build Test:docs +lake -R -Kenv=dev build Test:docs ``` If you have multiple libraries you want to generate full documentation for: ``` -lake -Kenv=dev build Test:docs Foo:docs +lake -R -Kenv=dev build Test:docs Foo:docs ``` -Note that doc-gen currently always generates documentation for `Lean`, `Init` + +Note that `doc-gen4` currently always generates documentation for `Lean`, `Init` and `Lake` in addition to the provided targets. +The root of the built docs will be `.lake/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 +`python3 -m http.server` from the `.lake/build/docs` directory. + +## Assumptions that `doc-gen4` makes +The only requirement for the `lake -Kenv=dev build Test:docs` to work is that your +target library builds, that is `lake build Test` exits without an error. If this requirement +is not fulfilled, the documentation generation will fail and you will end up with +partial build artefacts in `.lake/build/doc`. Note that `doc-gen4` is perfectly capable of +generating documentation for Lean code that contains `sorry`, just not for code +that doesn't compile. + +If you are working on a project that only partially compiles but can't fix the +errors from the top of your head, you can try to remove `import`s of both the failing files +and all files that refer to the failing ones from your top level library file. +Like this you will end up with an incomplete documentation but at least working +documentation of your project. + +Note that we do not recommend this approach and suggest to instead make sure your +projects always compile by using CI to prevent broken code from being added and `sorry`-ing +out things that you intend to complete later. + +## How does `docs#Nat.add` from the Lean Zulip work? +If someone sends a message that contains `docs#Nat.add` on the Lean Zulip this will +automatically link to `Nat.add` from the `mathlib4` documentation. The way that this +feature is implemented is by linking to `/find` of generated documentation in the following way: + in the case of the `mathlib4` +documentation this ends up being to: . +If you wish to provide a similar feature to `docs#Nat.add` from the Lean Zulip for your documentation, +this is the way to go. + ## 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 path to the modified version of `doc-gen4` is `../doc-gen4`, it would be: @@ -34,12 +67,7 @@ meta if get_config? env = some "dev" then -- dev is so not everyone has to build 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 -`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 -you rebuild the documentation. You can manually copy the changes to the `build/docs` directory to make +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 `.lake/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/lake-manifest.json b/lake-manifest.json index edbc3db..b69b2f9 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,36 +1,41 @@ -{"version": 6, - "packagesDir": "lake-packages", +{"version": 7, + "packagesDir": ".lake/packages", "packages": - [{"git": - {"url": "https://github.com/xubaiw/CMark.lean", - "subDir?": null, - "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", - "opts": {}, - "name": "CMark", - "inputRev?": "main", - "inherited": false}}, - {"git": - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "subDir?": null, - "rev": "4ecf4f1f98d14d03a9e84fa1c082630fa69df88b", - "opts": {}, - "name": "UnicodeBasic", - "inputRev?": "main", - "inherited": false}}, - {"git": - {"url": "https://github.com/mhuisi/lean4-cli", - "subDir?": null, - "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", - "opts": {}, - "name": "Cli", - "inputRev?": "nightly", - "inherited": false}}, - {"git": - {"url": "https://github.com/hargonix/LeanInk", - "subDir?": null, - "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", - "opts": {}, - "name": "leanInk", - "inputRev?": "doc-gen", - "inherited": false}}], - "name": "«doc-gen4»"} + [{"url": "https://github.com/xubaiw/CMark.lean", + "type": "git", + "subDir": null, + "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77", + "name": "CMark", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/hargonix/LeanInk", + "type": "git", + "subDir": null, + "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1", + "name": "leanInk", + "manifestFile": "lake-manifest.json", + "inputRev": "doc-gen", + "inherited": false, + "configFile": "lakefile.lean"}], + "name": "«doc-gen4»", + "lakeDir": ".lake"} diff --git a/lean-toolchain b/lean-toolchain index 183a307..24a3cdb 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.2.0-rc4 +leanprover/lean4:v4.3.0-rc2 diff --git a/test_docs.sh b/test_docs.sh index 387af03..c42005e 100755 --- a/test_docs.sh +++ b/test_docs.sh @@ -9,5 +9,5 @@ set -x cd "$1" sed -i "s|from git \"https://github.com/leanprover/doc-gen4\" @ \"main\"| from \"..\" / \"doc-gen4\" with NameMap.empty|" lakefile.lean -lake -Kdoc=on update -lake -Kdoc=on build Std:docs +lake -R -Kdoc=on update +lake -R -Kdoc=on build Std:docs