doc: Clearly spell out what happens on projects that fail to compile

.gitignore

@@ -1,3 +1,3 @@
-/build
+/.lake/*
 /lake-packages/*
 lakefile.olean

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"
 

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

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:
+<https://example.com/path/to/docs/find/?pattern=Nat.add#doc> in the case of the `mathlib4`
+documentation this ends up being to: <https://leanprover-community.github.io/mathlib4_docs/find/?pattern=Nat.add#doc>.
+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.)

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"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc4
+leanprover/lean4:v4.3.0-rc2

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