From fbbdb2179532cb3bc15295d739dc210a4cd3fab0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 21 Jul 2022 02:25:26 +0200
Subject: [PATCH] fix: remove redundant argument

---
 DocGen4/Load.lean                | 4 ++--
 DocGen4/Output.lean              | 8 ++++----
 DocGen4/Output/SourceLinker.lean | 3 ++-
 Main.lean                        | 4 ++--
 4 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index 7a45ec1..a47f918 100644
--- a/DocGen4/Load.lean
+++ b/DocGen4/Load.lean
@@ -19,7 +19,7 @@ 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 × String)) := do
+def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do
   let (leanInstall?, lakeInstall?) ← Lake.findInstall?
   match ←(EIO.toIO' $ Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with
   | .ok config =>
@@ -30,7 +30,7 @@ def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × Str
     let ctx ← Lake.mkBuildContext ws
     (ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx
     initSearchPath (←findSysroot) ws.leanPaths.oleanPath
-    pure $ Except.ok (ws, libraryLeanGitHash)
+    pure $ Except.ok ws
   | .error err =>
     throw $ IO.userError err.toString
 
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 11ec462..b482b7a 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -82,10 +82,10 @@ def Process.Module.toJson (module : Module) : HtmlM (Array Json) := do
       jsonDecls := jsonDecls.push json
     pure jsonDecls
 
-def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) (inkPath : Option System.FilePath) : IO Unit := do
+def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
   let config : SiteContext := {
     result := result,
-    sourceLinker := ←sourceLinker ws leanHash
+    sourceLinker := ←sourceLinker ws
     leanInkEnabled := inkPath.isSome
   }
   let basePath := FilePath.mk "." / "build" / "doc"
@@ -136,10 +136,10 @@ def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext :=
 The main entrypoint for outputting the documentation HTML based on an
 `AnalyzerResult`.
 -/
-def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (leanHash: String) (inkPath : Option System.FilePath) : IO Unit := do
+def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
   let baseConfig := getSimpleBaseContext hierarchy
   htmlOutputSetup baseConfig
-  htmlOutputResults baseConfig result ws leanHash inkPath
+  htmlOutputResults baseConfig result ws inkPath
 
 end DocGen4
 
diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean
index e269965..1080b76 100644
--- a/DocGen4/Output/SourceLinker.lean
+++ b/DocGen4/Output/SourceLinker.lean
@@ -54,7 +54,8 @@ Given a lake workspace with all the dependencies as well as the hash of the
 compiler release to work with this provides a function to turn names of
 declarations into (optionally positional) Github URLs.
 -/
-def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do
+def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange → String) := do
+  let leanHash := ws.env.lean.githash
   -- Compute a map from package names to source URL
   let mut gitMap := Std.mkHashMap
   let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
diff --git a/Main.lean b/Main.lean
index 1da5cbd..cbe8a8f 100644
--- a/Main.lean
+++ b/Main.lean
@@ -22,7 +22,7 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do
     let res ← lakeSetup modules
     let modules := modules.map Name.mkSimple
     match res with
-    | Except.ok (ws, leanHash) =>
+    | Except.ok ws =>
         IO.println s!"Loading modules from: {←searchPathRef.get}"
       --if p.hasFlag "single" then
       --  if modules.length ≠ 1 then
@@ -47,7 +47,7 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do
       --else
         let (doc, hierarchy) ← load modules true
         IO.println "Outputting HTML"
-        htmlOutput doc hierarchy ws leanHash (←findLeanInk? p)
+        htmlOutput doc hierarchy ws (←findLeanInk? p)
         pure 0
     | Except.error rc => pure rc