Merge pull request #19 from leanprover/source-links

Basic source links

DocGen4/Output.lean

@@ -14,8 +14,54 @@ 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 : 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
+  let mut url := out.stdout.trimRight
+
+  if url.startsWith "git@" then
+    url := url.drop 15
+    url := url.dropRight 4
+    s!"https://github.com/{url}"
+  else if url.endsWith ".git" then
+    url.dropRight 4
+  else
+    url
+
+def getCommit : 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
+  out.stdout.trimRight
+
+def sourceLinker : IO (Name → Option DeclarationRange → String) := do
+  let baseUrl ← getGithubBaseUrl
+  let commit ← getCommit
+  return λ name range =>
+    let parts := name.components.map Name.toString
+    let path := (parts.intersperse "/").foldl (· ++ ·) ""
+    let r := name.getRoot
+    let basic := if r == `Lean ∨ r == `Init ∨ r == `Std then
+      s!"https://github.com/leanprover/lean4/blob/{githash}/src/{path}.lean"
+    else
+      s!"{baseUrl}/blob/{commit}/{path}.lean"
+
+    match range with
+    | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
+    | none => basic
+
 def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
-  let config := { root := root, result := result, currentName := none}
+  let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker}
   let basePath := FilePath.mk "./build/doc/"
   let indexHtml := ReaderT.run index config 
   let notFoundHtml := ReaderT.run notFound config

DocGen4/Output/Base.lean

@@ -17,6 +17,8 @@ structure SiteContext where
   root : String
   result : AnalyzerResult
   currentName : Option Name
+  -- Generates a URL pointing to the source of the given module Name
+  sourceLinker : Name → Option DeclarationRange → String
 
 def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name}
 
@@ -26,6 +28,7 @@ abbrev HtmlM := HtmlT Id
 def getRoot : HtmlM String := do (←read).root
 def getResult : HtmlM AnalyzerResult := do (←read).result
 def getCurrentName : HtmlM (Option Name) := do (←read).currentName
+def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do (←read).sourceLinker module range
 
 def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
   new >>= base

DocGen4/Output/Module.lean

@@ -70,7 +70,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
   return <div «class»="decl_header"> [nodes] </div>
 
-def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
+def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
   let doc_html ← match doc with
   | DocInfo.inductiveInfo i => inductiveToHtml i
   | DocInfo.structureInfo i => structureToHtml i
@@ -81,7 +81,7 @@ def docInfoToHtml (doc : DocInfo) : HtmlM Html := do
     <div «class»={doc.getKind}>
       <div «class»="gh_link">
         -- TODO: Put the proper source link
-        <a href="https://github.com">source</a>
+        <a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
       </div>
       -- TODO: Attributes
       {←docInfoHeader doc}
@@ -94,19 +94,19 @@ def moduleToNavLink (module : Name) : Html :=
     <a «class»="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
   </div>
 
-def internalNav (members : Array Name) (moduleName : Name) : Html :=
+def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
   <nav «class»="internal_nav">
     <h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
     -- TODO: Proper source links
-    <p «class»="gh_nav_link"><a href="https://github.com">source</a></p>
+    <p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
     [members.map moduleToNavLink]
   </nav>
 
 def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
-  let docInfos ← module.members.mapM docInfoToHtml
+  let docInfos ← module.members.mapM (λ i => docInfoToHtml module.name i)
   -- TODO: This is missing imports, imported by
   templateExtends (baseHtmlArray module.name.toString) $ #[
-    internalNav (module.members.map DocInfo.getName) module.name,
+    ←internalNav (module.members.map DocInfo.getName) module.name,
     Html.element "main" false #[] docInfos
   ]