diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index ef495f5..f21c609 100644 --- a/DocGen4/Output.lean +++ b/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 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index eb29fc0..d02bf99 100644 --- a/DocGen4/Output/Base.lean +++ b/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 diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean index 48fcd3d..270daf7 100644 --- a/DocGen4/Output/Index.lean +++ b/DocGen4/Output/Index.lean @@ -16,7 +16,7 @@ def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|

Welcome to the documentation page

- What is up? +

This was built for commit {s!"{← getProjectCommit} "} using Lean 4 at commit {Lean.githash}

end Output diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean index d54b9f9..1d921ca 100644 --- a/DocGen4/Output/SourceLinker.lean +++ b/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 diff --git a/Main.lean b/Main.lean index d40c742..5758b8d 100644 --- a/Main.lean +++ b/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