refactor: pull source linker into submodule

DocGen4/Output.lean

@@ -12,74 +12,12 @@ import DocGen4.Output.Module
 import DocGen4.Output.NotFound
 import DocGen4.Output.Find
 import DocGen4.Output.Semantic
+import DocGen4.Output.SourceLinker
 
 namespace DocGen4
 
 open Lean Std IO System Output
 
-
-/-
-Three link types from git supported:
-- https://github.com/org/repo
-- https://github.com/org/repo.git
-- git@github.com:org/repo.git
-TODO: This function is quite brittle and very github specific, we can
-probably do better.
--/
-def getGithubBaseUrl (gitUrl : String) : String := Id.run do
-  let mut url := gitUrl
-  if url.startsWith "git@" then
-    url := url.drop 15
-    url := url.dropRight 4
-    pure s!"https://github.com/{url}"
-  else if url.endsWith ".git" then
-    pure $ url.dropRight 4
-  else
-    pure url
-
-def getProjectGithubUrl : IO String := do
-  let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
-  if out.exitCode != 0 then
-    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
-  pure out.stdout.trimRight
-
-def getProjectCommit : IO String := do
-  let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]}
-  if out.exitCode != 0 then
-    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
-  pure out.stdout.trimRight
-
-def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do
-  -- Compute a map from package names to source URL
-  let mut gitMap := Std.mkHashMap
-  let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
-  let projectCommit ← getProjectCommit
-  gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
-  for pkg in ws.packageArray do
-    for dep in pkg.dependencies do
-      let value := match dep.src with
-        | Lake.Source.git url commit => (getGithubBaseUrl url, commit)
-        -- TODO: What do we do here if linking a source is not possible?
-        | _ => ("https://example.com", "master")
-      gitMap := gitMap.insert dep.name value
-
-  pure $ λ module range =>
-    let parts := module.components.map Name.toString
-    let path := (parts.intersperse "/").foldl (· ++ ·) ""
-    let root := module.getRoot
-    let basic := if root == `Lean ∨ root == `Init ∨ root == `Std then
-      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
-    else
-      match ws.packageForModule? module with
-      | some pkg =>
-        let (baseUrl, commit) := gitMap.find! pkg.name
-        s!"{baseUrl}/blob/{commit}/{path}.lean"
-      | none => "https://example.com"
-
-    match range with
-    | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
-    | none => basic
-
 def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
   let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
   let basePath := FilePath.mk "." / "build" / "doc"

DocGen4/Output/SourceLinker.lean

@@ -0,0 +1,70 @@
+import Lean
+import Lake
+
+namespace DocGen4.Output
+
+open Lean
+
+/-
+Three link types from git supported:
+- https://github.com/org/repo
+- https://github.com/org/repo.git
+- git@github.com:org/repo.git
+TODO: This function is quite brittle and very github specific, we can
+probably do better.
+-/
+def getGithubBaseUrl (gitUrl : String) : String := Id.run do
+  let mut url := gitUrl
+  if url.startsWith "git@" then
+    url := url.drop 15
+    url := url.dropRight 4
+    pure s!"https://github.com/{url}"
+  else if url.endsWith ".git" then
+    pure $ url.dropRight 4
+  else
+    pure url
+
+def getProjectGithubUrl : IO String := do
+  let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
+  if out.exitCode != 0 then
+    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
+  pure out.stdout.trimRight
+
+def getProjectCommit : IO String := do
+  let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]}
+  if out.exitCode != 0 then
+    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
+  pure out.stdout.trimRight
+
+def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do
+  -- Compute a map from package names to source URL
+  let mut gitMap := Std.mkHashMap
+  let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
+  let projectCommit ← getProjectCommit
+  gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
+  for pkg in ws.packageArray do
+    for dep in pkg.dependencies do
+      let value := match dep.src with
+        | Lake.Source.git url commit => (getGithubBaseUrl url, commit)
+        -- TODO: What do we do here if linking a source is not possible?
+        | _ => ("https://example.com", "master")
+      gitMap := gitMap.insert dep.name value
+
+  pure $ λ module range =>
+    let parts := module.components.map Name.toString
+    let path := (parts.intersperse "/").foldl (· ++ ·) ""
+    let root := module.getRoot
+    let basic := if root == `Lean ∨ root == `Init ∨ root == `Std then
+      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
+    else
+      match ws.packageForModule? module with
+      | some pkg =>
+        let (baseUrl, commit) := gitMap.find! pkg.name
+        s!"{baseUrl}/blob/{commit}/{path}.lean"
+      | none => "https://example.com"
+
+    match range with
+    | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
+    | none => basic
+
+end DocGen4.Output