diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 7919f67..8d99535 100644 --- a/DocGen4/Output.lean +++ b/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" diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean new file mode 100644 index 0000000..b50c961 --- /dev/null +++ b/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