(obsolete) feat: add bibliography support

DocGen4/Output.lean

@@ -10,6 +10,8 @@ import DocGen4.Output.Index
 import DocGen4.Output.Module
 import DocGen4.Output.NotFound
 import DocGen4.Output.Find
+import DocGen4.Output.References
+import DocGen4.Output.Pybtex
 import DocGen4.Output.SourceLinker
 import DocGen4.Output.Search
 import DocGen4.Output.ToJson
@@ -20,6 +22,21 @@ namespace DocGen4
 
 open Lean IO System Output Process
 
+def collectBackrefs : IO (Array BackrefItem) := do
+  let mut backrefs : Array BackrefItem := #[]
+  for entry in ← System.FilePath.readDir declarationsBasePath do
+    if entry.fileName.startsWith "backrefs-" && entry.fileName.endsWith ".json" then
+      let fileContent ← FS.readFile entry.path
+      match Json.parse fileContent with
+      | .error err =>
+        throw <| IO.userError s!"failed to parse file '{entry.path}' as json: {err}"
+      | .ok jsonContent =>
+        match fromJson? jsonContent with
+        | .error err =>
+          throw <| IO.userError s!"failed to parse file '{entry.path}': {err}"
+        | .ok (arr : Array BackrefItem) => backrefs := backrefs ++ arr
+  return backrefs
+
 def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let findBasePath := basePath / "find"
 
@@ -35,6 +52,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let foundationalTypesHtml := ReaderT.run foundationalTypes config |>.toString
   let navbarHtml := ReaderT.run navbar config |>.toString
   let searchHtml := ReaderT.run search config |>.toString
+  let referencesHtml := ReaderT.run (references (← collectBackrefs)) config |>.toString
   let docGenStatic := #[
     ("style.css", styleCss),
     ("favicon.svg", faviconSvg),
@@ -52,7 +70,8 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
     ("index.html", indexHtml),
     ("foundational_types.html", foundationalTypesHtml),
     ("404.html", notFoundHtml),
-    ("navbar.html", navbarHtml)
+    ("navbar.html", navbarHtml),
+    ("references.html", referencesHtml)
   ]
   for (fileName, content) in docGenStatic do
     FS.writeFile (basePath / fileName) content
@@ -72,14 +91,15 @@ def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
 
 def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (sourceUrl? : Option String) : IO Unit := do
   let config : SiteContext := {
-    result := result,
+    result := result
     sourceLinker := SourceLinker.sourceLinker sourceUrl?
+    refsMap := .ofList (baseConfig.refs.map fun x => (x.citekey, x)).toList
   }
 
   FS.createDirAll basePath
   FS.createDirAll declarationsBasePath
 
-  discard <| htmlOutputDeclarationDatas result |>.run config baseConfig
+  discard <| htmlOutputDeclarationDatas result |>.run {} config baseConfig
 
   for (modName, module) in result.moduleInfo.toArray do
     let fileDir := moduleNameToDirectory basePath modName
@@ -90,16 +110,29 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
       depthToRoot := modName.components.dropLast.length
       currentName := some modName
     }
-    let moduleHtml := moduleToHtml module |>.run config baseConfig
+    let (moduleHtml, cfg) := moduleToHtml module |>.run {} config baseConfig
+    if not cfg.errors.isEmpty then
+      throw <| IO.userError s!"There are errors when generating '{filePath}': {cfg.errors}"
     FS.createDirAll fileDir
     FS.writeFile filePath moduleHtml.toString
+    FS.writeFile (declarationsBasePath / s!"backrefs-{module.name}.json") (toString (toJson cfg.backrefs))
 
 def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do
-  return {
-    depthToRoot := 0,
-    currentName := none,
-    hierarchy
-  }
+  let contents ← FS.readFile (declarationsBasePath / "references.json") <|> (pure "[]")
+  match Json.parse contents with
+  | .error err =>
+    throw <| IO.userError s!"Failed to parse 'references.json': {err}"
+  | .ok jsonContent =>
+    match fromJson? jsonContent with
+    | .error err =>
+      throw <| IO.userError s!"Failed to parse 'references.json': {err}"
+    | .ok (refs : Array BibItem) =>
+      return {
+        depthToRoot := 0
+        currentName := none
+        hierarchy := hierarchy
+        refs := refs
+      }
 
 def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
   htmlOutputSetup baseConfig
@@ -109,10 +142,16 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
   for entry in ← System.FilePath.readDir declarationsBasePath do
     if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
       let fileContent ← FS.readFile entry.path
-      let .ok jsonContent := Json.parse fileContent | unreachable!
-      let .ok (module : JsonModule) := fromJson? jsonContent | unreachable!
-      index := index.addModule module |>.run baseConfig
-      headerIndex := headerIndex.addModule module
+      match Json.parse fileContent with
+      | .error err =>
+        throw <| IO.userError s!"failed to parse file '{entry.path}' as json: {err}"
+      | .ok jsonContent =>
+        match fromJson? jsonContent with
+        | .error err =>
+          throw <| IO.userError s!"failed to parse file '{entry.path}': {err}"
+        | .ok (module : JsonModule) =>
+          index := index.addModule module |>.run baseConfig
+          headerIndex := headerIndex.addModule module
 
   let finalJson := toJson index
   let finalHeaderJson := toJson headerIndex

DocGen4/Output/Base.lean

@@ -15,6 +15,32 @@ def basePath := FilePath.mk "." / ".lake" / "build" / "doc"
 def srcBasePath := basePath / "src"
 def declarationsBasePath := basePath / "declarations"
 
+/-- The structure representing a processed bibitem. -/
+structure BibItem where
+  /-- The cite key as in the bib file. -/
+  citekey : String
+  /-- The tag generated by bib processor, e.g. `[Doe12]`.
+  Should be plain text and should not be escaped. -/
+  tag : String
+  /-- The HTML generated by bib processor, e.g.
+  `John Doe. <i>Test</i>. 2012.`-/
+  html : String
+  /-- The plain text form of `html` field. Should not be escaped. -/
+  plaintext : String
+  deriving FromJson, ToJson
+
+/-- The structure representing a backref item. -/
+structure BackrefItem where
+  /-- The cite key as in the bib file. -/
+  citekey : String
+  /-- The name of the module. -/
+  modName : Name
+  /-- The name of the function, as a string. It is empty if the backref is in modstring. -/
+  funName : String
+  /-- The index of the backref in that module, starting from zero. -/
+  index : Nat
+  deriving FromJson, ToJson, Inhabited
+
 /--
 The context used in the `BaseHtmlM` monad for HTML templating.
 -/
@@ -33,9 +59,13 @@ structure SiteBaseContext where
   pages that don't have a module name.
   -/
   currentName : Option Name
+  /--
+  The list of references, as an array.
+  -/
+  refs : Array BibItem
 
 /--
-The context used in the `HtmlM` monad for HTML templating.
+The read-only context used in the `HtmlM` monad for HTML templating.
 -/
 structure SiteContext where
   /--
@@ -46,23 +76,42 @@ structure SiteContext where
   A function to link declaration names to their source URLs, usually Github ones.
   -/
   sourceLinker : Name → Option DeclarationRange → String
+  /--
+  The references as a map.
+  -/
+  refsMap : HashMap String BibItem
+
+/--
+The writable state used in the `HtmlM` monad for HTML templating.
+-/
+structure SiteState where
+  /--
+  The list of back references, as an array.
+  -/
+  backrefs : Array BackrefItem := #[]
+  /--
+  The errors occurred during the process.
+  -/
+  errors : String := ""
 
 def setCurrentName (name : Name) (ctx : SiteBaseContext) := {ctx with currentName := some name}
 
 abbrev BaseHtmlT := ReaderT SiteBaseContext
 abbrev BaseHtmlM := BaseHtmlT Id
 
-abbrev HtmlT (m) := ReaderT SiteContext (BaseHtmlT m)
+abbrev HtmlT (m) := StateT SiteState <| ReaderT SiteContext <| BaseHtmlT m
 abbrev HtmlM := HtmlT Id
 
-def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : m α :=
-  ReaderT.run x ctx |>.run baseCtx
+def HtmlT.run (x : HtmlT m α) (state : SiteState) (ctx : SiteContext)
+    (baseCtx : SiteBaseContext) : m (α × SiteState) :=
+  StateT.run x state |>.run ctx |>.run baseCtx
 
-def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α :=
-  ReaderT.run x ctx |>.run baseCtx |>.run
+def HtmlM.run (x : HtmlM α) (state : SiteState) (ctx : SiteContext)
+    (baseCtx : SiteBaseContext) : α × SiteState :=
+  StateT.run x state |>.run ctx |>.run baseCtx |>.run
 
 instance [Monad m] : MonadLift HtmlM (HtmlT m) where
-  monadLift x := do return x.run (← readThe SiteContext) (← readThe SiteBaseContext)
+  monadLift x := do return (x.run (← getThe SiteState) (← readThe SiteContext) (← readThe SiteBaseContext)).1
 
 instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
   monadLift x := do return x.run (← readThe SiteBaseContext)