Merge pull request #78 from leanprover/LeanInkLink

Simple LeanInk links.

.github/workflows/build.yml

@@ -25,14 +25,6 @@ jobs:
         run: |
           lake build
 
-      - name: Checkout and compile LeanInk
-        run: |
-          cd ../
-          git clone https://github.com/hargonix/LeanInk
-          cd LeanInk
-          git checkout doc-gen-json
-          lake build
-
       - name: Checkout and compile mathlib4
         run: |
           cd ../

DocGen4/LeanInk/Output.lean

@@ -5,7 +5,6 @@ Authors: Henrik Böving, Xubai Wang
 -/
 import DocGen4.Output.Base
 import DocGen4.Output.ToHtmlFormat
-import DocGen4.LeanInk.Process
 import Lean.Data.Json
 import LeanInk.Annotation.Alectryon
 
@@ -17,7 +16,8 @@ open scoped DocGen4.Jsx
 structure AlectryonContext where
   counter : Nat
 
-abbrev AlectryonM := StateT AlectryonContext HtmlM
+abbrev AlectryonT := StateT AlectryonContext
+abbrev AlectryonM := AlectryonT HtmlM
 
 def getNextButtonLabel : AlectryonM String := do
   let val ← get
@@ -35,7 +35,7 @@ def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
               <span class="hyp-type">
                 <var>{tyi.name}</var>
                 <b>: </b>
-                <span>{tyi.type}</span>
+                <span>[←DocGen4.Output.infoFormatToHtml tyi.type.fst]</span>
               </span>
             </div>
           </blockquote>
@@ -80,16 +80,16 @@ def Contents.toHtml : Contents → AlectryonM Html
 
 def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
   let mut hypParts := #[<var>[h.names.intersperse ", " |>.map Html.text |>.toArray]</var>]
-  if h.body != "" then
+  if h.body.snd != "" then
     hypParts := hypParts.push
       <span class="hyp-body">
         <b>:= </b>
-        <span>{h.body}</span>
+        <span>[←infoFormatToHtml h.body.fst]</span>
       </span>
   hypParts := hypParts.push
       <span class="hyp-type">
         <b>: </b>
-        <span >{h.type}</span>
+        <span >[←infoFormatToHtml h.type.fst]</span>
       </span>
 
   pure
@@ -103,6 +103,11 @@ def Goal.toHtml (g : Goal) : AlectryonM Html := do
     let rendered ← hyp.toHtml
     hypotheses := hypotheses.push rendered
     hypotheses := hypotheses.push <br/>
+  let conclusionHtml ←
+    match g.conclusion with
+    | .typed info _ => infoFormatToHtml info
+    | .untyped str => pure <| #[Html.text str]
+
   pure
     <blockquote class="alectryon-goal">
       <div class="goal-hyps">
@@ -112,7 +117,7 @@ def Goal.toHtml (g : Goal) : AlectryonM Html := do
         <hr><span class="goal-name">{g.name}</span></hr>
       </span>
       <div class="goal-conclusion">
-        {g.conclusion}
+        [conclusionHtml]
       </div>
     </blockquote>
 
@@ -197,27 +202,14 @@ def baseHtml (content : Array Html) : AlectryonM Html := do
       </body>
     </html>
 
-def renderFragments (fs : Array Fragment) : AlectryonM Html :=
+def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List Fragment) := do
-  fs.mapM Fragment.toHtml >>= baseHtml
+  let config ← read
+  annotateFileWithCompounds [] config.inputFileContents as
+
+-- TODO: rework monad mess
+def renderAnnotations (as : List Annotation.Annotation) : HtmlT AnalysisM Html := do
+  let fs ← annotationsToFragments as
+  let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 }
+  pure html
 
 end LeanInk.Annotation.Alectryon
-
-namespace DocGen4.Output.LeanInk
-
-open Lean
-open LeanInk.Annotation.Alectryon
-open scoped DocGen4.Jsx
-
-def moduleToHtml (module : Process.Module) (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : HtmlT IO Html := withTheReader SiteBaseContext (setCurrentName module.name) do
-  let json ← runInk inkPath sourceFilePath
-  let fragments := fromJson? json
-  match fragments with
-  | .ok fragments =>
-    let render := StateT.run (LeanInk.Annotation.Alectryon.renderFragments fragments) { counter := 0 }
-    let ctx ← read
-    let baseCtx ← readThe SiteBaseContext
-    let (html, _) := render |>.run ctx baseCtx
-    pure html
-  | .error err => throw <| IO.userError s!"Error while parsing LeanInk Output: {err}"
-
-end DocGen4.Output.LeanInk

DocGen4/LeanInk/Process.lean

@@ -3,38 +3,55 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-import Lean.Data.Json
+import Lean
+import LeanInk.Analysis
+import LeanInk.Annotation
+import DocGen4.LeanInk.Output
+import DocGen4.Output.Base
 
-namespace DocGen4.Output.LeanInk
+namespace DocGen4.Process.LeanInk
 
 open Lean
-open IO
+open DocGen4.Output
 
-def runInk (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : IO Json := do
+def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.AnalysisM UInt32 := do
-  let arguments := #[
+  let some modName ← getCurrentName | unreachable!
-    "analyze", sourceFilePath.toString,
+  let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as
-    "--lake", "lakefile.lean",
+  let srcDir := moduleNameToDirectory srcBasePath modName
-    "--x-enable-type-info",
+  let srcPath := moduleNameToFile srcBasePath modName
-    "--x-enable-docStrings",
+  IO.FS.createDirAll srcDir
-    "--x-enable-semantic-token"
+  IO.FS.writeFile srcPath srcHtml.toString
-  ]
+  pure 0
-  let inkProcess ← Process.spawn {
+
-    stdin := Process.Stdio.null
+def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
-    stdout := Process.Stdio.piped
+  let ctx ← readThe SiteContext
-    stderr := Process.Stdio.piped
+  let baseCtx ← readThe SiteBaseContext
-    cmd := inkPath.toString
+  let outputFn := (docGenOutput · |>.run ctx baseCtx)
-    args := arguments
+  return ← LeanInk.Analysis.runAnalysis { 
+    name := "doc-gen4"
+    genOutput := outputFn
+  } 
+
+def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do
+  execAuxM.run (←readThe SiteContext) (←readThe SiteBaseContext) |>.run config
+
+@[implementedBy enableInitializersExecution]
+private def enableInitializersExecutionWrapper : IO Unit := pure ()
+
+def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do
+  let contents ← IO.FS.readFile sourceFilePath
+  let config := { 
+    inputFilePath := sourceFilePath
+    inputFileContents := contents
+    lakeFile := none
+    verbose := false
+    prettifyOutput := true
+    experimentalTypeInfo := true
+    experimentalDocString := true
+    experimentalSemanticType := true
   }
-  match (←inkProcess.wait) with
+  enableInitializersExecutionWrapper
-  | 0 =>
+  if (← execAux config) != 0 then
-    let outputFilePath := sourceFilePath.withExtension "lean.leanInk"
+    throw <| IO.userError s!"Analysis for \"{sourceFilePath}\" failed!"
-    let output ← FS.readFile outputFilePath
-    FS.removeFile outputFilePath
-    match Json.parse output with
-    | .ok out => pure out
-    | .error err =>
-      throw <| IO.userError s!"LeanInk returned invalid JSON for file: {sourceFilePath}:\n{err}"
-  | code =>
-    throw <| IO.userError s!"LeanInk exited with code {code} for file: {sourceFilePath}:\n{←inkProcess.stderr.readToEnd}"
 
-end DocGen4.Output.LeanInk
+end DocGen4.Process.LeanInk

DocGen4/Load.lean

@@ -19,20 +19,13 @@ Sets up a lake workspace for the current project. Furthermore initialize
 the Lean search path with the path to the proper compiler from lean-toolchain
 as well as all the dependencies.
 -/
-def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do
+def lakeSetup : IO (Except UInt32 Lake.Workspace) := do
   let (leanInstall?, lakeInstall?) ← Lake.findInstall?
   match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with
   | .ok config =>
     let ws : Lake.Workspace ← Lake.loadWorkspace config
       |>.run Lake.MonadLog.eio
       |>.toIO (λ _ => IO.userError "Failed to load Lake workspace")
-    let libraryLeanGitHash := ws.lakeEnv.lean.githash
-    if libraryLeanGitHash ≠ Lean.githash then
-      IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {libraryLeanGitHash}"
-    let _libs ← ws.runBuild (Lake.buildImportsAndDeps imports) false
-      |>.run (Lake.MonadLog.eio config.verbosity)
-      |>.toIO (λ _ => IO.userError "Failed to compile imports via Lake")
-    initSearchPath (←findSysroot) (ws.packageList.map (·.oleanDir))
     pure <| Except.ok ws
   | .error err =>
     throw <| IO.userError err.toString
@@ -62,4 +55,7 @@ def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy)
 
   Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
 
+def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
+  load <| .loadAll [`Init, `Std, `Lean]
+
 end DocGen4

DocGen4/Output.lean

@@ -13,17 +13,13 @@ import DocGen4.Output.NotFound
 import DocGen4.Output.Find
 import DocGen4.Output.SourceLinker
 import DocGen4.Output.ToJson
-import DocGen4.LeanInk.Output
+import DocGen4.LeanInk.Process
 import Std.Data.HashMap
 
 namespace DocGen4
 
 open Lean IO System Output Process Std
 
-def basePath := FilePath.mk "." / "build" / "doc"
-def srcBasePath := basePath / "src"
-def declarationsBasePath := basePath / "declarations"
-
 def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let findBasePath := basePath / "find"
 
@@ -76,11 +72,11 @@ def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
     let jsonDecls ← Module.toJson mod
     FS.writeFile (declarationsBasePath / s!"declaration-data-{mod.name}.bmp") (toJson jsonDecls).compress
 
-def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
+def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
   let config : SiteContext := {
     result := result,
     sourceLinker := ←sourceLinker ws
-    leanInkEnabled := inkPath.isSome
+    leanInkEnabled := ink
   }
 
   FS.createDirAll basePath
@@ -97,21 +93,20 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
     let filePath := moduleNameToFile basePath modName
     -- path: 'basePath/module/components/till/last.html'
     -- The last component is the file name, so we drop it from the depth to root.
-    let baseConfig := { baseConfig with depthToRoot := modName.components.dropLast.length }
+    let baseConfig := { baseConfig with
+      depthToRoot := modName.components.dropLast.length
+      currentName := some modName
+    }
     let moduleHtml := moduleToHtml module |>.run config baseConfig
     FS.createDirAll fileDir
     FS.writeFile filePath moduleHtml.toString
-    if let some inkPath := inkPath then
+    if ink then
       if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
         IO.println s!"Inking: {modName.toString}"
         -- path: 'basePath/src/module/components/till/last.html'
         -- The last component is the file name, however we are in src/ here so dont drop it this time
-        let baseConfig := { baseConfig with depthToRoot := modName.components.length }
+        let baseConfig := {baseConfig with depthToRoot := modName.components.length }
-        let srcHtml ← LeanInk.moduleToHtml module inkPath inputPath |>.run config baseConfig
+        Process.LeanInk.runInk inputPath |>.run config baseConfig
-        let srcDir := moduleNameToDirectory srcBasePath modName
-        let srcPath := moduleNameToFile srcBasePath modName
-        FS.createDirAll srcDir
-        FS.writeFile srcPath srcHtml.toString
 
 def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext :=
   {
@@ -139,9 +134,9 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
 The main entrypoint for outputting the documentation HTML based on an
 `AnalyzerResult`.
 -/
-def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
+def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
   let baseConfig := getSimpleBaseContext hierarchy
-  htmlOutputResults baseConfig result ws inkPath
+  htmlOutputResults baseConfig result ws ink
   htmlOutputIndex baseConfig
 
 end DocGen4

DocGen4/Output/Base.lean

@@ -11,6 +11,10 @@ namespace DocGen4.Output
 open scoped DocGen4.Jsx
 open Lean System Widget Elab Process
 
+def basePath := FilePath.mk "." / "build" / "doc"
+def srcBasePath := basePath / "src"
+def declarationsBasePath := basePath / "declarations"
+
 /--
 The context used in the `BaseHtmlM` monad for HTML templating.
 -/
@@ -61,6 +65,12 @@ def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) :
 def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α :=
   ReaderT.run x ctx |>.run baseCtx |>.run
 
+instance [Monad m] : MonadLift HtmlM (HtmlT m) where
+  monadLift x := do pure <| x.run (←readThe SiteContext) (←readThe SiteBaseContext)
+
+instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
+  monadLift x := do pure <| x.run (←readThe SiteBaseContext)
+
 /--
 Obtains the root URL as a relative one to the current depth.
 -/
@@ -202,17 +212,21 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
   | TaggedText.tag a t =>
     match a.info.val.info with
     | Info.ofTermInfo i =>
-      match i.expr.consumeMData with
+      let cleanExpr :=  i.expr.consumeMData
-      | Expr.const name _ =>
+      if let Expr.const name _ := cleanExpr then
-         match t with
+        -- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM
-         | TaggedText.text t =>
+        -- find a better solution
-           let (front, t, back) := splitWhitespaces <| Html.escape t
+        if (←getResult).name2ModIdx.contains name then
-           let elem := <a href={←declNameToLink name}>{t}</a>
+          match t with
-           pure #[Html.text front, elem, Html.text back]
+          | TaggedText.text t =>
-         | _ =>
+            let (front, t, back) := splitWhitespaces <| Html.escape t
-           -- TODO: Is this ever reachable?
+            let elem := <a href={←declNameToLink name}>{t}</a>
-           pure #[<a href={←declNameToLink name}>[←infoFormatToHtml t]</a>]
+            pure #[Html.text front, elem, Html.text back]
-      | _ =>
+          | _ =>
+            pure #[<a href={←declNameToLink name}>[←infoFormatToHtml t]</a>]
+        else
+         pure #[<span class="fn">[←infoFormatToHtml t]</span>]
+      else
          pure #[<span class="fn">[←infoFormatToHtml t]</span>]
     | _ => pure #[<span class="fn">[←infoFormatToHtml t]</span>]
 

Main.lean

@@ -4,16 +4,6 @@ import Cli
 
 open DocGen4 Lean Cli
 
-def findLeanInk? (p : Parsed) : IO (Option System.FilePath) := do
-  match p.flag? "ink" with
-  | some ink =>
-    let inkPath := System.FilePath.mk ink.value
-    if ←inkPath.pathExists then
-      pure <| some inkPath
-    else
-      throw <| IO.userError "Invalid path to LeanInk binary provided"
-  | none => pure none
-
 def getTopLevelModules (p : Parsed) : IO (List String) :=  do
   let topLevelModules := p.variableArgsAs! String |>.toList
   if topLevelModules.length == 0 then
@@ -21,46 +11,45 @@ def getTopLevelModules (p : Parsed) : IO (List String) :=  do
   pure topLevelModules
 
 def runSingleCmd (p : Parsed) : IO UInt32 := do
-    let relevantModules := [p.positionalArg! "module" |>.as! String]
+  let relevantModules := [p.positionalArg! "module" |>.as! String |> String.toName]
-    let res ← lakeSetup (relevantModules)
+  let res ← lakeSetup
-    match res with
+  match res with
-    | Except.ok ws =>
+  | Except.ok ws =>
-      let relevantModules := relevantModules.map String.toName
+    let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules
-      let (doc, hierarchy) ← load (.loadAllLimitAnalysis relevantModules)
+    IO.println "Outputting HTML"
-      IO.println "Outputting HTML"
+    let baseConfig := getSimpleBaseContext hierarchy
-      let baseConfig := getSimpleBaseContext hierarchy
+    htmlOutputResults baseConfig doc ws (p.hasFlag "ink")
-      htmlOutputResults baseConfig doc ws (←findLeanInk? p)
+    pure 0
-      pure 0
+  | Except.error rc => pure rc
-    | Except.error rc => pure rc
 
 def runIndexCmd (_p : Parsed) : IO UInt32 := do
-  let hierarchy ← Hierarchy.fromDirectory basePath
+  let hierarchy ← Hierarchy.fromDirectory Output.basePath
   let baseConfig := getSimpleBaseContext hierarchy
   htmlOutputIndex baseConfig
   pure 0
 
-def runDocGenCmd (p : Parsed) : IO UInt32 := do
+def runGenCoreCmd (_p : Parsed) : IO UInt32 := do
-  let modules : List String := p.variableArgsAs! String |>.toList
+  let res ← lakeSetup
-  if modules.length == 0 then
-    throw <| IO.userError "No modules provided."
-
-  let res ← lakeSetup modules
   match res with
   | Except.ok ws =>
-    IO.println s!"Loading modules from: {←searchPathRef.get}"
+    let (doc, hierarchy) ← loadCore
-    let modules := modules.map String.toName
-    let (doc, hierarchy) ← load (.loadAll modules)
     IO.println "Outputting HTML"
-    htmlOutput doc hierarchy ws (←findLeanInk? p)
+    let baseConfig := getSimpleBaseContext hierarchy
+    htmlOutputResults baseConfig doc ws (ink := False) 
     pure 0
   | Except.error rc => pure rc
 
+def runDocGenCmd (_p : Parsed) : IO UInt32 := do
+  IO.println "You most likely want to use me via Lake now, check my README on Github on how to:"
+  IO.println "https://github.com/leanprover/doc-gen4"
+  return 0
+
 def singleCmd := `[Cli|
   single VIA runSingleCmd;
   "Only generate the documentation for the module it was given, might contain broken links unless all documentation is generated."
 
   FLAGS:
-    ink : String; "Path to a LeanInk binary to use for rendering the Lean sources."
+    ink; "Render the files with LeanInk in addition"
 
   ARGS:
     module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules."
@@ -73,19 +62,19 @@ def indexCmd := `[Cli|
     ...topLevelModule : String; "The top level modules this documentation will be for."
 ]
 
+def genCoreCmd := `[Cli|
+  genCore VIA runGenCoreCmd;
+  "Generate documentation for the core Lean modules: Init, Std and Lean since they are not Lake projects"
+]
+
 def docGenCmd : Cmd := `[Cli|
-  "doc-gen4" VIA runDocGenCmd; ["0.0.1"]
+  "doc-gen4" VIA runDocGenCmd; ["0.1.0"]
   "A documentation generator for Lean 4."
 
-  FLAGS:
-    ink : String; "Path to a LeanInk binary to use for rendering the Lean sources."
-
-  ARGS:
-    ...modules : String; "The modules to generate the HTML for."
-
   SUBCOMMANDS:
     singleCmd;
-    indexCmd
+    indexCmd;
+    genCoreCmd
 ]
 
 def main (args : List String) : IO UInt32 :=

README.md

@@ -2,48 +2,15 @@
 Document Generator for Lean 4
 
 ## Usage
-You can call `doc-gen4` from the top of a Lake project like this:
+`doc-gen4` is the easiest to use via its custom Lake facet, in order
-```sh
+to do this you have to add it to your `lakefile.lean` like this:
-$ /path/to/doc-gen4 Module
 ```
-
+meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
-where `Module` is one or more of the top level modules you want to document.
+require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"
-The tool will then proceed to compile the project using lake (if that hasn't happened yet),
-analyze it and put the result in `./build/doc`.
-
-You can optionally provide the path to a `LeanInk` binary using the `--ink` flag which will make
-the tool produce `Alectryon` style rendered output along the usual documentation.
-
-You could e.g. host the files locally with the built-in Python webserver:
-```sh
-$ cd build/doc && python -m http.server
 ```
-
+Then you can generate documentation for an entire library using:
-### 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 build stage is to run doc-gen for all modules separately:
-
-1. `doc-gen4 single Init`
-2. `doc-gen4 single Std`
-3. `doc-gen4 single Lean`
-4. `doc-gen4 single Mathlib`
-
-Note that you can also just make a call to submodules so `Mathlib.Algebra`
-will work standalone as well. Furthermore one can use the `--ink` flag
-here to also generate LeanInk documentation in addition.
-
-The second and last stage is the index one which zips up some
-information relevant for the search:
-```sh
-$ doc-gen4 index Mathlib
 ```
-Now `build/doc` should contain the same files with the same context as if one had run
+lake -Kenv=dev build Test:docs
-```
-$ doc-gen4 Mathlib
 ```
+If you have multiple libraries you want to generate documentation for
+the recommended way right now is to run it for each library.

deploy_docs.sh

@@ -23,7 +23,7 @@ fi
 
 # generate the docs
 cd $1
-../$2/build/bin/doc-gen4 --ink ../$4/build/bin/leanInk Mathlib
+lake -Kenv=dev build Mathlib:docs --verbose
 
 if [ "$3" = "true" ]; then
   cd ..

lakefile.lean

@@ -25,4 +25,93 @@ require lake from git
   "https://github.com/leanprover/lake" @ "master"
 
 require leanInk from git
-  "https://github.com/hargonix/LeanInk" @ "doc-gen-json"
+  "https://github.com/hargonix/LeanInk" @ "doc-gen"
+
+module_facet docs (mod) : FilePath := do
+  let some docGen4 ← findLeanExe? `«doc-gen4»
+    | error "no doc-gen4 executable configuration found in workspace"
+  let exeJob ← docGen4.exe.fetch
+  let modJob ← mod.leanBin.fetch
+  let buildDir := (← getWorkspace).root.buildDir
+  let docFile := mod.filePath (buildDir / "doc") "html"
+  exeJob.bindAsync fun exeFile exeTrace => do
+  modJob.bindSync fun _ modTrace => do
+    let depTrace := exeTrace.mix modTrace
+    let trace ← buildFileUnlessUpToDate docFile depTrace do
+      logInfo s!"Documenting module: {mod.name}"
+      proc {
+        cmd := exeFile.toString
+        args := #["single", mod.name.toString, "--ink"]
+        env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
+      }
+    return (docFile, trace)
+
+-- TODO: technically speaking this facet does not show all file dependencies
+target coreDocs : FilePath := do
+  let some docGen4 ← findLeanExe? `«doc-gen4»
+    | error "no doc-gen4 executable configuration found in workspace"
+  let exeJob ← docGen4.exe.fetch
+  let basePath := (←getWorkspace).root.buildDir / "doc"
+  let dataFile := basePath / "declarations" / "declaration-data-Lean.bmp"
+  exeJob.bindSync fun exeFile exeTrace => do
+    let trace ← buildFileUnlessUpToDate dataFile exeTrace do
+      logInfo "Documenting Lean core: Init, Std, Lean"
+      proc {
+        cmd := exeFile.toString
+        args := #["genCore"]
+        env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
+      }
+    return (dataFile, trace)
+
+library_facet docs (lib) : FilePath := do
+  let some docGen4Pkg ← findPackage? `«doc-gen4»
+    | error "no doc-gen4 package found in workspace"
+  let some docGen4 := docGen4Pkg.findLeanExe? `«doc-gen4»
+    | error "no doc-gen4 executable configuration found in workspace"
+  let exeJob ← docGen4.exe.fetch
+
+  -- XXX: Workaround remove later
+  let coreJob ← if h : docGen4Pkg.name = _package.name then
+    have : Fact (docGen4Pkg.name = _package.name) := Fact.mk h
+    let job := fetch <| docGen4Pkg.target `coreDocs
+    job
+  else
+    error "wrong package"
+
+  let moduleJobs ← BuildJob.mixArray (α := FilePath) <| ← lib.recBuildLocalModules #[`docs]
+  -- Shared with DocGen4.Output
+  let basePath := (←getWorkspace).root.buildDir / "doc"
+  let dataFile := basePath / "declarations" / "declaration-data.bmp"
+  let staticFiles := #[
+    basePath / "style.css",
+    basePath / "declaration-data.js",
+    basePath / "nav.js",
+    basePath / "how-about.js",
+    basePath / "search.js",
+    basePath / "mathjax-config.js",
+    basePath / "instances.js",
+    basePath / "importedBy.js",
+    basePath / "index.html",
+    basePath / "404.html",
+    basePath / "navbar.html",
+    basePath / "find" / "index.html",
+    basePath / "find" / "find.js",
+    basePath / "src"  / "alectryon.css",
+    basePath / "src"  / "alectryon.js",
+    basePath / "src"  / "docutils_basic.css",
+    basePath / "src"  / "pygments.css"
+  ]
+  coreJob.bindAsync fun _ coreInputTrace => do
+    exeJob.bindAsync fun exeFile exeTrace => do
+      moduleJobs.bindSync fun _ inputTrace => do
+        let depTrace := mixTraceArray #[inputTrace, exeTrace, coreInputTrace]
+        let trace ← buildFileUnlessUpToDate dataFile depTrace do
+          logInfo "Documentation indexing"
+          proc {
+            cmd := exeFile.toString
+            args := #["index"]
+          }
+        let traces ← staticFiles.mapM computeTrace
+        let indexTrace := mixTraceArray traces
+
+        return (dataFile, trace.mix indexTrace)

lean_packages/manifest.json

@@ -4,7 +4,7 @@
    "rev": "112b35fc348a4a18d2111ac2c6586163330b4941",
    "name": "Cli"},
   {"url": "https://github.com/hargonix/LeanInk",
-   "rev": "eed51a5e121233c3d15fb14642048a9bd3e00695",
+   "rev": "439303af06465824588a486f5f9c023ca69979f3",
    "name": "leanInk"},
   {"url": "https://github.com/xubaiw/Unicode.lean",
    "rev": "25b32ef69fd6d8ae34300d51dc0b9403ffb1fd29",