feat: show versions in index HTML

DocGen4/Output.lean

@@ -81,7 +81,7 @@ def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT 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
+    sourceLinker := ← SourceLinker.sourceLinker ws
     leanInkEnabled := ink
   }
 
@@ -114,11 +114,13 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
         let baseConfig := {baseConfig with depthToRoot := modName.components.length }
         Process.LeanInk.runInk inputPath |>.run config baseConfig
 
-def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext :=
-  {
+def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do
+  return {
     depthToRoot := 0,
     currentName := none,
     hierarchy
+    projectGithubUrl := ← SourceLinker.getProjectGithubUrl
+    projectCommit := ← SourceLinker.getProjectCommit
   }
 
 def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
@@ -141,7 +143,7 @@ The main entrypoint for outputting the documentation HTML based on an
 `AnalyzerResult`.
 -/
 def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
-  let baseConfig := getSimpleBaseContext hierarchy
+  let baseConfig ← getSimpleBaseContext hierarchy
   htmlOutputResults baseConfig result ws ink
   htmlOutputIndex baseConfig
 

DocGen4/Output/Base.lean

@@ -33,6 +33,14 @@ structure SiteBaseContext where
   pages that don't have a module name.
   -/
   currentName : Option Name
+  /--
+  The Github URL of the project that we are building docs for.
+  -/
+  projectGithubUrl : String
+  /--
+  The commit of the project that we are building docs for.
+  -/
+  projectCommit : String
 
 /--
 The context used in the `HtmlM` monad for HTML templating.
@@ -86,6 +94,8 @@ def getCurrentName : BaseHtmlM (Option Name) := do return (← read).currentName
 def getResult : HtmlM AnalyzerResult := do return (← read).result
 def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do return (← read).sourceLinker module range
 def leanInkEnabled? : HtmlM Bool := do return (← read).leanInkEnabled
+def getProjectGithubUrl : BaseHtmlM String := do return (← read).projectGithubUrl
+def getProjectCommit : BaseHtmlM String := do return (← read).projectCommit
 
 /--
 If a template is meant to be extended because it for example only provides the

DocGen4/Output/Index.lean

@@ -16,7 +16,7 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
     <main>
       <a id="top"></a>
       <h1> Welcome to the documentation page </h1>
-      What is up?
+      <p>This was built for commit <a href={s!"{← getProjectGithubUrl}/tree/{← getProjectCommit}"}>{s!"{← getProjectCommit} "}</a> using Lean 4 at commit <a href={s!"https://github.com/leanprover/lean4/tree/{Lean.githash}"}>{Lean.githash}</a></p>
     </main>
 
 end Output

DocGen4/Output/SourceLinker.lean

@@ -6,7 +6,7 @@ Authors: Henrik Böving
 import Lean
 import Lake.Load
 
-namespace DocGen4.Output
+namespace DocGen4.Output.SourceLinker
 
 open Lean
 
@@ -86,4 +86,4 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange
     | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
     | none => basic
 
-end DocGen4.Output
+end DocGen4.Output.SourceLinker

Main.lean

@@ -17,14 +17,14 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do
   | Except.ok ws =>
     let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules
     IO.println "Outputting HTML"
-    let baseConfig := getSimpleBaseContext hierarchy
+    let baseConfig ← getSimpleBaseContext hierarchy
     htmlOutputResults baseConfig doc ws (p.hasFlag "ink")
     return 0
   | Except.error rc => pure rc
 
 def runIndexCmd (_p : Parsed) : IO UInt32 := do
   let hierarchy ← Hierarchy.fromDirectory Output.basePath
-  let baseConfig := getSimpleBaseContext hierarchy
+  let baseConfig ← getSimpleBaseContext hierarchy
   htmlOutputIndex baseConfig
   return 0
 
@@ -34,7 +34,7 @@ def runGenCoreCmd (_p : Parsed) : IO UInt32 := do
   | Except.ok ws =>
     let (doc, hierarchy) ← loadCore
     IO.println "Outputting HTML"
-    let baseConfig := getSimpleBaseContext hierarchy
+    let baseConfig ← getSimpleBaseContext hierarchy
     htmlOutputResults baseConfig doc ws (ink := False) 
     return 0
   | Except.error rc => pure rc