feat: tactic overview page (#353)

* feat: a page documenting all tactics

* Fix: save in correct location

* Link to definition/module in tactic docs

* Sort tactics alphabetically in output

* Don't treat Tactics as a module when generating side bar

* Don't need to talk about supplement anymore.

* Add tactics.html to Lake's list of generated files

* Case sensitivity

Author: Vierkantor

DocGen4/Output.lean

@@ -14,6 +14,7 @@ import DocGen4.Output.References
 import DocGen4.Output.Bibtex
 import DocGen4.Output.SourceLinker
 import DocGen4.Output.Search
+import DocGen4.Output.Tactics
 import DocGen4.Output.ToJson
 import DocGen4.Output.FoundationalTypes
 
@@ -52,6 +53,7 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let navbarHtml := ReaderT.run navbar config |>.toString
   let searchHtml := ReaderT.run search config |>.toString
   let referencesHtml := ReaderT.run (references (← collectBackrefs config.buildDir)) config |>.toString
+  let tacticsHtml := ReaderT.run (tactics (← loadTacticsJSON config.buildDir)) config |>.toString
   let docGenStatic := #[
     ("style.css", styleCss),
     ("favicon.svg", faviconSvg),
@@ -70,7 +72,8 @@ def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
     ("foundational_types.html", foundationalTypesHtml),
     ("404.html", notFoundHtml),
     ("navbar.html", navbarHtml),
-    ("references.html", referencesHtml)
+    ("references.html", referencesHtml),
+    ("tactics.html", tacticsHtml),
   ]
   for (fileName, content) in docGenStatic do
     FS.writeFile (basePath config.buildDir / fileName) content
@@ -117,18 +120,22 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
       currentName := some modName
     }
     let (moduleHtml, cfg) := moduleToHtml module |>.run {} config baseConfig
+    let (tactics, cfg) := module.tactics.mapM TacticInfo.docStringToHtml |>.run cfg config baseConfig
     if not cfg.errors.isEmpty then
       throw <| IO.userError s!"There are errors when generating '{filePath}': {cfg.errors}"
     if let .some d := filePath.parent then
       FS.createDirAll d
     FS.writeFile filePath moduleHtml.toString
     FS.writeFile (declarationsBasePath baseConfig.buildDir / s!"backrefs-{module.name}.json") (toString (toJson cfg.backrefs))
+    saveTacticsJSON (declarationsBasePath baseConfig.buildDir / s!"tactics-{module.name}.json") tactics
     -- The output paths need to be relative to the build directory, as they are stored in a build
     -- artifact.
     outputs := outputs.push relFilePath
+
   return outputs
 
-def getSimpleBaseContext (buildDir : System.FilePath) (hierarchy : Hierarchy) : IO SiteBaseContext := do
+def getSimpleBaseContext (buildDir : System.FilePath) (hierarchy : Hierarchy) :
+    IO SiteBaseContext := do
   let contents ← FS.readFile (declarationsBasePath buildDir / "references.json") <|> (pure "[]")
   match Json.parse contents with
   | .error err =>

DocGen4/Output/Navbar.lean

@@ -57,15 +57,15 @@ The main entry point to rendering the navbar on the left hand side.
 def navbar : BaseHtmlM Html := do
   /-
   TODO: Add these in later
-  <div class="nav_link"><a href={s!"{← getRoot}tactics.html"}>tactics</a></div>
   <div class="nav_link"><a href={s!"{← getRoot}commands.html"}>commands</a></div>
   <div class="nav_link"><a href={s!"{← getRoot}hole_commands.html"}>hole commands</a></div>
   <div class="nav_link"><a href={s!"{← getRoot}attributes.html"}>attributes</a></div>
   <div class="nav_link"><a href={s!"{← getRoot}notes.html"}>notes</a></div>
   -/
   let mut staticPages : Array Html := #[
     <div class="nav_link"><a href={s!"{← getRoot}"}>index</a></div>,
-    <div class="nav_link"><a href={s!"{← getRoot}foundational_types.html"}>foundational types</a></div>
+    <div class="nav_link"><a href={s!"{← getRoot}foundational_types.html"}>foundational types</a></div>,
+    <div class="nav_link"><a href={s!"{← getRoot}tactics.html"}>tactics</a></div>,
   ]
   let config ← read
   if not config.refs.isEmpty then

DocGen4/Output/Tactics.lean

@@ -0,0 +1,91 @@
+/-
+Copyright (c) 2025 Anne Baanen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anne Baanen
+-/
+import DocGen4.Process.Analyze
+import DocGen4.Output.Module
+
+namespace DocGen4.Process
+
+open scoped DocGen4.Jsx
+open DocGen4 Output Lean
+
+/--
+Render the HTML for a single tactic.
+-/
+def TacticInfo.docStringToHtml (tac : TacticInfo MarkdownDocstring) : Output.HtmlM (TacticInfo Html) := do
+  return {
+    tac with
+    docString := <p>[← Output.docStringToHtml tac.docString tac.internalName.toString]</p>
+  }
+
+/--
+Render the HTML for a single tactic.
+-/
+def TacticInfo.toHtml (tac : TacticInfo Html) : Output.BaseHtmlM Html := do
+  let internalName := tac.internalName.toString
+  let defLink := (← moduleNameToLink tac.definingModule) ++ "#" ++ internalName
+  let tags := ", ".intercalate (tac.tags.map (·.toString)).qsort.toList
+  return <div id={internalName}>
+    <h2>{tac.userName}</h2>
+    {tac.docString}
+    <dl>
+      <dt>Tags:</dt>
+      <dd>{tags}</dd>
+      <dt>Defined in module:</dt>
+      <dd><a href={defLink}>{tac.definingModule.toString}</a></dd>
+    </dl>
+  </div>
+
+def TacticInfo.navLink (tac : TacticInfo α) : Html :=
+  <p><a href={"#".append tac.internalName.toString}>{tac.userName}</a></p>
+
+end DocGen4.Process
+
+namespace DocGen4.Output
+
+open scoped DocGen4.Jsx
+open Lean Process
+
+/--
+Render the HTML for the tactics listing page.
+-/
+def tactics (tacticInfo : Array (TacticInfo Html)) : BaseHtmlM Html := do
+  let sectionsHtml ← tacticInfo.mapM (· |>.toHtml)
+  templateLiftExtends (baseHtmlGenerator "Tactics") <| pure #[
+    <nav class="internal_nav">
+      <p><a href="#top">return to top</a></p>
+      [tacticInfo.map (· |>.navLink)]
+    </nav>,
+    Html.element "main" false #[] (
+      #[<p>The tactic language is a special-purpose programming language for constructing proofs, indicated using the keyword <code>by</code>.</p>] ++
+      sectionsHtml)
+  ]
+
+def loadTacticsJSON (buildDir : System.FilePath) : IO (Array (TacticInfo Html)) := do
+  let mut result : Array (TacticInfo _) := #[]
+  for entry in ← System.FilePath.readDir (declarationsBasePath buildDir) do
+    if entry.fileName.startsWith "tactics-" && entry.fileName.endsWith ".json" then
+      let fileContent ← IO.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 (TacticInfo _)) => result := result ++ arr
+  return result.qsort (lt := (·.userName < ·.userName))
+
+/-- Save sections of supplementary pages declared in a specific module.
+
+This `abbrev` exists as a type-checking wrapper around `toJson`, ensuring `loadTacticsJSON` gets
+objects in the expected format.
+-/
+abbrev saveTacticsJSON (fileName : System.FilePath) (tacticInfo : Array (TacticInfo Html)) : IO Unit := do
+  if tacticInfo.size > 0 then
+    IO.FS.writeFile fileName (toString (toJson tacticInfo))
+
+end Output
+end DocGen4

DocGen4/Process/Analyze.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 
+import Lean.Elab.Tactic.Doc
 import Lean.Meta.Basic
+import Lean.Parser.Extension
 import Std.Data.HashMap
 import Std.Data.HashSet
 
@@ -15,6 +17,10 @@ import DocGen4.Process.DocInfo
 namespace DocGen4.Process
 
 open Lean Meta
+open Lean.Elab.Tactic.Doc
+
+/-- Represents a non-verso docstring; these will be rendered using `Output.docStringToHtml`. -/
+abbrev MarkdownDocstring := String
 
 /--
 Member of a module, either a declaration or some module doc string.
@@ -24,6 +30,25 @@ inductive ModuleMember where
 | modDoc (doc : ModuleDoc) : ModuleMember
 deriving Inhabited
 
+/-- Information about a tactic declaration which will be rendered on the Tactics page.
+
+This datastructure contains slightly different contents compared to a `TacticDoc` to make
+it easily serializable as JSON. It is designed to be easy to instantiate,
+using `{ tacticDoc with ... }`.
+-/
+structure TacticInfo (textType : Type) where
+  /-- The name of the canonical parser for the tactic -/
+  internalName : Name
+  /-- The user-facing name to display (typically the first keyword token) -/
+  userName : String
+  /-- The tags that have been applied to the tactic -/
+  tags : Array Name
+  /-- The docstring for the tactic, including any extension docstrings. -/
+  docString : textType
+  /-- Name of the module where the tactic is declared. -/
+  definingModule : Name
+deriving FromJson, ToJson
+
 /--
 A Lean module.
 -/
@@ -37,6 +62,10 @@ structure Module where
   -/
   members : Array ModuleMember
   imports : Array Name
+  /--
+  Tactics declared in this module.
+  -/
+  tactics : Array (TacticInfo MarkdownDocstring)
   deriving Inhabited
 
 /--
@@ -92,6 +121,24 @@ def AnalyzeTask.getLoad (task : AnalyzeTask) : Array Name :=
   | .analyzePrefixModules topLevel => #[topLevel]
   | .analyzeConcreteModules modules => modules
 
+/-- Collect tactic info for pages to display in addition to the module docs. -/
+def collectTactics (module : Name) (env : Environment) :
+    MetaM (Array (TacticInfo MarkdownDocstring)) := do
+  let docs ← Elab.Tactic.Doc.allTacticDocs
+  let mut contents := #[]
+  for doc in docs do
+    let some modIdx := env.getModuleIdxFor? doc.internalName | continue
+    let definingModule := env.header.moduleNames[modIdx]!
+    if module != definingModule then continue
+    contents := contents.push {
+      doc with
+      docString := doc.docString.getD "This tactic has no documentation." ++
+        ("\n\n".intercalate doc.extensionDocs.toList)
+      tags := doc.tags.toArray,
+      definingModule := definingModule,
+    }
+  return contents
+
 def getAllModuleDocs (relevantModules : Array Name) : MetaM (Std.HashMap Name Module) := do
   let env ← getEnv
   let mut res := Std.HashMap.emptyWithCapacity relevantModules.size
@@ -100,7 +147,8 @@ def getAllModuleDocs (relevantModules : Array Name) : MetaM (Std.HashMap Name Mo
     let some modIdx := env.getModuleIdx? module | unreachable!
     let moduleData := env.header.moduleData[modIdx]!
     let imports := moduleData.imports.map Import.module
-    res := res.insert module <| Module.mk module modDocs imports
+    let tactics ← collectTactics module env
+    res := res.insert module <| Module.mk module modDocs imports tactics
   return res
 
 def mkOptions : IO DocGenOptions := do

DocGen4/Process/Hierarchy.lean

@@ -96,7 +96,8 @@ def baseDirBlackList : Std.HashSet String :=
     "search.js",
     "src",
     "style.css",
-    "favicon.svg"
+    "favicon.svg",
+    "tactics.html",
   ]
 
 partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array Name) := do

lakefile.lean

@@ -308,6 +308,7 @@ library_facet docs (lib) : Array FilePath := do
     basePath / "foundational_types.html",
     basePath / "references.html",
     basePath / "references.bib",
+    basePath / "tactics.html",
     basePath / "find" / "index.html",
     basePath / "find" / "find.js"
   ]