feat: Add support for vscode links (default true if changes)

DocGen4/Output.lean

@@ -80,10 +80,10 @@ def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
     let jsonDecls ← Module.toJson mod
     FS.writeFile (declarationsBasePath / s!"declaration-data-{mod.name}.bmp") (toJson jsonDecls).compress
 
-def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
+def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (sourceUrl? : Option String) (ink : Bool) : IO Unit := do
   let config : SiteContext := {
     result := result,
-    sourceLinker := ← SourceLinker.sourceLinker gitUrl?
+    sourceLinker := SourceLinker.sourceLinker sourceUrl?
     leanInkEnabled := ink
   }
 
@@ -144,10 +144,9 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
 The main entrypoint for outputting the documentation HTML based on an
 `AnalyzerResult`.
 -/
-def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
+def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (sourceUrl? : Option String) (ink : Bool) : IO Unit := do
   let baseConfig ← getSimpleBaseContext hierarchy
-  htmlOutputResults baseConfig result gitUrl? ink
+  htmlOutputResults baseConfig result sourceUrl? ink
   htmlOutputIndex baseConfig
 
 end DocGen4
-

DocGen4/Output/SourceLinker.lean

@@ -9,28 +9,40 @@ namespace DocGen4.Output.SourceLinker
 
 open Lean
 
+def mkGithubSourceLinker (baseUrl : String) (range : Option DeclarationRange) : String :=
+  match range with
+  | some range => s!"{baseUrl}#L{range.pos.line}-L{range.endPos.line}"
+  | none => baseUrl
+
+def mkVscodeSourceLinker (baseUrl : String) (range : Option DeclarationRange) : String :=
+  match range with
+  -- Note. We may want to verify Lean line and column numbers match VSCode.
+  | some range => s!"{baseUrl}:{range.pos.line}:{range.pos.column}"
+  | none => baseUrl
+
 /--
 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 (gitUrl? : Option String) : IO (Name → Option DeclarationRange → String) := do
-  -- TOOD: Refactor this, we don't need to pass in the module into the returned closure
-  -- since we have one sourceLinker per module
-  return fun module range =>
+def sourceLinker (gitUrl? : Option String) (module : Name) : Option DeclarationRange → String :=
+  let root := module.getRoot
+  let leanHash := Lean.githash
+  if root == `Lean ∨ root == `Init then
     let parts := module.components.map Name.toString
     let path := String.intercalate "/" parts
-    let root := module.getRoot
-    let leanHash := Lean.githash
-    let basic := if root == `Lean ∨ root == `Init then
-      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
-    else if root == `Lake then
-      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/lake/{path}.lean"
-    else
-      gitUrl?.get!
-
-    match range with
-    | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"
-    | none => basic
+    mkGithubSourceLinker s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
+  else if root == `Lake then
+    let parts := module.components.map Name.toString
+    let path := String.intercalate "/" parts
+    mkGithubSourceLinker s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/lake/{path}.lean"
+  else
+    match gitUrl? with
+    | .some url =>
+      if url.startsWith "vscode://file/" then
+        mkVscodeSourceLinker url
+      else
+        mkGithubSourceLinker url
+    | .none => panic! s!"Github URL must be defined for {module}."
 
 end DocGen4.Output.SourceLinker

DocGen4/Output/ToJson.lean

@@ -117,12 +117,12 @@ def JsonIndex.addModule (index : JsonIndex) (module : JsonModule) : BaseHtmlM Js
     }
   return index
 
-def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclaration := do
+def DocInfo.toJson (sourceLinker : Option DeclarationRange → String) (info : Process.DocInfo) : HtmlM JsonDeclaration := do
   let name := info.getName.toString
   let kind := info.getKind
   let doc := info.getDocString.getD ""
   let docLink ← declNameToLink info.getName
-  let sourceLink ← getSourceUrl module info.getDeclarationRange
+  let sourceLink := sourceLinker info.getDeclarationRange
   let line := info.getDeclarationRange.pos.line
   let header := (← docInfoHeader info).toString
   let info := { name, kind, doc, docLink, sourceLink, line }
@@ -131,9 +131,10 @@ def DocInfo.toJson (module : Name) (info : Process.DocInfo) : HtmlM JsonDeclarat
 def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
     let mut jsonDecls := []
     let mut instances := #[]
+    let sourceLinker := (← read).sourceLinker module.name
     let declInfo := Process.filterDocInfo module.members
     for decl in declInfo do
-      jsonDecls := (← DocInfo.toJson module.name decl) :: jsonDecls
+      jsonDecls := (← DocInfo.toJson sourceLinker decl) :: jsonDecls
       if let .instanceInfo i := decl then
         instances := instances.push {
           name := i.name.toString,

Main.lean

@@ -12,10 +12,10 @@ def getTopLevelModules (p : Parsed) : IO (List String) :=  do
 
 def runSingleCmd (p : Parsed) : IO UInt32 := do
   let relevantModules := #[p.positionalArg! "module" |>.as! String |> String.toName]
-  let gitUrl := p.positionalArg! "gitUrl" |>.as! String
+  let sourceUrl := p.positionalArg! "sourceUrl" |>.as! String
   let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules
   let baseConfig ← getSimpleBaseContext hierarchy
-  htmlOutputResults baseConfig doc (some gitUrl) (p.hasFlag "ink")
+  htmlOutputResults baseConfig doc (some sourceUrl) (p.hasFlag "ink")
   return 0
 
 def runIndexCmd (_p : Parsed) : IO UInt32 := do
@@ -27,7 +27,7 @@ def runIndexCmd (_p : Parsed) : IO UInt32 := do
 def runGenCoreCmd (_p : Parsed) : IO UInt32 := do
   let (doc, hierarchy) ← loadCore
   let baseConfig ← getSimpleBaseContext hierarchy
-  htmlOutputResults baseConfig doc none (ink := False) 
+  htmlOutputResults baseConfig doc none (ink := False)
   return 0
 
 def runDocGenCmd (_p : Parsed) : IO UInt32 := do

lakefile.lean

@@ -48,10 +48,10 @@ def getGithubBaseUrl (gitUrl : String) : String := Id.run do
 /--
 Obtain the Github URL of a project by parsing the origin remote.
 -/
-def getProjectGithubUrl (directory : System.FilePath := "." ) : IO String := do
+def getProjectGithubUrl (directory : System.FilePath := "." ) (remote : String := "origin") : IO String := do
   let out ← IO.Process.output {
     cmd := "git",
-    args := #["remote", "get-url", "origin"],
+    args := #["remote", "get-url", remote],
     cwd := directory
   }
   if out.exitCode != 0 then
@@ -71,16 +71,31 @@ def getProjectCommit (directory : System.FilePath := "." ) : IO String := do
     throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the current commit in {directory}"
   return out.stdout.trimRight
 
-def getGitUrl (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do
-  let baseUrl := getGithubBaseUrl (← getProjectGithubUrl pkg.dir)
+def filteredPath (path : FilePath) : List String := path.components.filter (· != ".")
+
+def getGitPkgUrl (pkg : Package) : IO (List String) := do
+  let baseUrl := getGithubBaseUrl (← getProjectGithubUrl pkg.dir "origin")
   let commit ← getProjectCommit pkg.dir
+  let srcDir := filteredPath pkg.config.srcDir
+  return baseUrl :: "blob" :: commit :: srcDir
+
+def getVsCodeUrl (pkg : Package) := do
+  let dir ← IO.FS.realPath pkg.config.srcDir
+  pure [s!"vscode://file/{dir}"]
 
-  let parts := mod.name.components.map toString
-  let path := String.intercalate "/" parts
-  let libPath := pkg.config.srcDir / lib.srcDir
-  let basePath := String.intercalate "/" (libPath.components.filter (· != "."))
-  let url := s!"{baseUrl}/blob/{commit}/{basePath}/{path}.lean"
-  return url
+def getGitChanged (directory : System.FilePath := ".") : IO Bool := do
+  let out ← IO.Process.output {
+    cmd := "git",
+    args := #["status", "--porcelain=v1"]
+    cwd := directory
+  }
+  return out.exitCode != 0 || out.stdout.trim != ""
+
+def getGitUrl (pkg : Package) (lib : LeanLibConfig) (mod : Module) : IO String := do
+  let baseUrl ← if ← getGitChanged then getVsCodeUrl pkg else getGitPkgUrl pkg
+  let libPath := filteredPath lib.srcDir
+  let modPath := mod.name.components.map toString
+  return s!"{String.intercalate "/" (baseUrl ++ libPath ++ modPath)}.lean"
 
 module_facet docs (mod) : FilePath := do
   let some docGen4 ← findLeanExe? `«doc-gen4»