perf: Don't call Lake from within doc-gen anymore

DocGen4/Load.lean

@@ -5,30 +5,12 @@ Authors: Henrik Böving
 -/
 
 import Lean
-import Lake
-import Lake.CLI.Main
 import DocGen4.Process
 import Lean.Data.HashMap
 
 namespace DocGen4
 
 open Lean System IO
-/--
-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 : IO (Except UInt32 Lake.Workspace) := do
-  let (_, leanInstall?, lakeInstall?) ← Lake.findInstall?
-  let config := Lake.mkLoadConfig.{0} {leanInstall?, lakeInstall?}
-  match ←(EIO.toIO' config) with
-  | .ok config =>
-    let ws : Lake.Workspace ← Lake.loadWorkspace config
-      |>.run Lake.MonadLog.eio
-      |>.toIO (λ _ => IO.userError "Failed to load Lake workspace")
-    pure <| Except.ok ws
-  | .error err =>
-    throw <| IO.userError err.toString
 
 def envOfImports (imports : Array Name) : IO Environment := do
  importModules (imports.map (Import.mk · false)) Options.empty
@@ -42,6 +24,7 @@ Load a list of modules from the current Lean search path into an `Environment`
 to process for documentation.
 -/
 def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) := do
+  initSearchPath (← findSysroot)
   let env ← envOfImports task.getLoad
   let config := {
     -- TODO: parameterize maxHeartbeats

DocGen4/Output.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 import Lean
-import Lake
 import DocGen4.Process
 import DocGen4.Output.Base
 import DocGen4.Output.Index
@@ -81,19 +80,18 @@ 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) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
+def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
   let config : SiteContext := {
     result := result,
-    sourceLinker := ← SourceLinker.sourceLinker ws
+    sourceLinker := ← SourceLinker.sourceLinker gitUrl?
     leanInkEnabled := ink
   }
 
   FS.createDirAll basePath
   FS.createDirAll declarationsBasePath
 
-  -- Rendering the entire lean compiler takes time....
+  let some p := (← IO.getEnv "LEAN_SRC_PATH") | throw <| IO.userError "LEAN_SRC_PATH not found in env"
-  --let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath
+  let sourceSearchPath := System.SearchPath.parse p
-  let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath
 
   discard <| htmlOutputDeclarationDatas result |>.run config baseConfig
 
@@ -121,8 +119,6 @@ def getSimpleBaseContext (hierarchy : Hierarchy) : IO SiteBaseContext := do
     depthToRoot := 0,
     currentName := none,
     hierarchy
-    projectGithubUrl := ← SourceLinker.getProjectGithubUrl
-    projectCommit := ← SourceLinker.getProjectCommit
   }
 
 def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
@@ -148,9 +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) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
+def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (gitUrl? : Option String) (ink : Bool) : IO Unit := do
   let baseConfig ← getSimpleBaseContext hierarchy
-  htmlOutputResults baseConfig result ws ink
+  htmlOutputResults baseConfig result gitUrl? ink
   htmlOutputIndex baseConfig
 
 end DocGen4

DocGen4/Output/Base.lean

@@ -33,14 +33,6 @@ structure SiteBaseContext where
   pages that don't have a module name.
   -/
   currentName : Option Name
-  /--
-  The Github URL of the project that we are building docs for.
-  -/
-  projectGithubUrl : String
-  /--
-  The commit of the project that we are building docs for.
-  -/
-  projectCommit : String
 
 /--
 The context used in the `HtmlM` monad for HTML templating.
@@ -94,8 +86,6 @@ def getCurrentName : BaseHtmlM (Option Name) := do return (← read).currentName
 def getResult : HtmlM AnalyzerResult := do return (← read).result
 def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do return (← read).sourceLinker module range
 def leanInkEnabled? : HtmlM Bool := do return (← read).leanInkEnabled
-def getProjectGithubUrl : BaseHtmlM String := do return (← read).projectGithubUrl
-def getProjectCommit : BaseHtmlM String := do return (← read).projectCommit
 
 /--
 If a template is meant to be extended because it for example only provides the

DocGen4/Output/SourceLinker.lean

@@ -4,105 +4,30 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
 import Lean
-import Lake.Load
 
 namespace DocGen4.Output.SourceLinker
 
 open Lean
 
-/--
-Turns a Github git remote URL into an HTTPS Github URL.
-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
-    return s!"https://github.com/{url}"
-  else if url.endsWith ".git" then
-    return url.dropRight 4
-  else
-    return url
-
-/--
-Obtain the Github URL of a project by parsing the origin remote.
--/
-def getProjectGithubUrl (directory : System.FilePath := "." ) : IO String := do
-  let out ← IO.Process.output {
-    cmd := "git",
-    args := #["remote", "get-url", "origin"],
-    cwd := directory
-  }
-  if out.exitCode != 0 then
-    throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the git remote in {directory}"
-  return out.stdout.trimRight
-
-/--
-Obtain the git commit hash of the project that is currently getting analyzed.
--/
-def getProjectCommit (directory : System.FilePath := "." ) : IO String := do
-  let out ← IO.Process.output {
-    cmd := "git",
-    args := #["rev-parse", "HEAD"]
-    cwd := directory
-  }
-  if out.exitCode != 0 then
-    throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the current commit in {directory}"
-  return out.stdout.trimRight
-
-def modulePath (ws : Lake.Workspace) (module : Name) : Option (Lake.Package × Lake.LeanLibConfig) := do
-  let pkg ← ws.packages.find? (·.isLocalModule module)
-  let libConfig ← pkg.leanLibConfigs.toArray.find? (·.isLocalModule module)
-  return (pkg, libConfig)
-
 /--
 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) : IO (Name → Option DeclarationRange → String) := do
+def sourceLinker (gitUrl? : Option String) : IO (Name → Option DeclarationRange → String) := do
-  let leanHash := ws.lakeEnv.lean.githash
+  -- TOOD: Refactor this, we don't need to pass in the module into the returned closure
-  -- Compute a map from package names to source URL
+  -- since we have one sourceLinker per module
-  let mut gitMap := Lean.mkHashMap
-  let projectBaseUrl := getGithubBaseUrl (← getProjectGithubUrl)
-  let projectCommit ← getProjectCommit
-  gitMap := gitMap.insert ws.root.name (projectBaseUrl, projectCommit)
-  let manifest ← Lake.Manifest.loadOrEmpty ws.root.manifestFile
-      |>.run (Lake.MonadLog.eio .normal)
-      |>.toIO (fun _ => IO.userError "Failed to load lake manifest")
-  for pkg in manifest.packages do
-    match pkg with
-    | .git _ _ _ url rev .. => gitMap := gitMap.insert pkg.name (getGithubBaseUrl url, rev)
-    | .path _ _ _ path =>
-      let pkgBaseUrl := getGithubBaseUrl (← getProjectGithubUrl path)
-      let pkgCommit ← getProjectCommit path
-      gitMap := gitMap.insert pkg.name (pkgBaseUrl, pkgCommit)
-
   return fun module range =>
     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
-      match modulePath ws module with
+      gitUrl?.get!
-      | some (pkg, lib) =>
-        match gitMap.find? pkg.name with
-        | some (baseUrl, commit) =>
-          let libPath := pkg.config.srcDir / lib.srcDir
-          let basePath := String.intercalate "/" (libPath.components.filter (· != "."))
-          s!"{baseUrl}/blob/{commit}/{basePath}/{path}.lean"
-        | none => "https://example.com"
-      | none => "https://example.com"
 
     match range with
     | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}"

Main.lean

@@ -12,14 +12,11 @@ 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 res ← lakeSetup
+  let gitUrl := p.positionalArg! "gitUrl" |>.as! String
-  match res with
-  | Except.ok ws =>
   let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules
   let baseConfig ← getSimpleBaseContext hierarchy
-    htmlOutputResults baseConfig doc ws (p.hasFlag "ink")
+  htmlOutputResults baseConfig doc (some gitUrl) (p.hasFlag "ink")
   return 0
-  | Except.error rc => pure rc
 
 def runIndexCmd (_p : Parsed) : IO UInt32 := do
   let hierarchy ← Hierarchy.fromDirectory Output.basePath
@@ -28,14 +25,10 @@ def runIndexCmd (_p : Parsed) : IO UInt32 := do
   return 0
 
 def runGenCoreCmd (_p : Parsed) : IO UInt32 := do
-  let res ← lakeSetup
-  match res with
-  | Except.ok ws =>
   let (doc, hierarchy) ← loadCore
   let baseConfig ← getSimpleBaseContext hierarchy
-    htmlOutputResults baseConfig doc ws (ink := False) 
+  htmlOutputResults baseConfig doc none (ink := False) 
   return 0
-  | Except.error rc => pure rc
 
 def runDocGenCmd (_p : Parsed) : IO UInt32 := do
   IO.println "You most likely want to use me via Lake now, check my README on Github on how to:"
@@ -51,6 +44,7 @@ def singleCmd := `[Cli|
 
   ARGS:
     module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules."
+    gitUrl : String; "The gitUrl as computed by the Lake facet"
 ]
 
 def indexCmd := `[Cli|

lakefile.lean

@@ -23,15 +23,78 @@ require Cli from git
 require leanInk from git
   "https://github.com/hargonix/LeanInk" @ "doc-gen"
 
+
+/--
+Turns a Github git remote URL into an HTTPS Github URL.
+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
+    return s!"https://github.com/{url}"
+  else if url.endsWith ".git" then
+    return url.dropRight 4
+  else
+    return url
+
+/--
+Obtain the Github URL of a project by parsing the origin remote.
+-/
+def getProjectGithubUrl (directory : System.FilePath := "." ) : IO String := do
+  let out ← IO.Process.output {
+    cmd := "git",
+    args := #["remote", "get-url", "origin"],
+    cwd := directory
+  }
+  if out.exitCode != 0 then
+    throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the git remote in {directory}"
+  return out.stdout.trimRight
+
+/--
+Obtain the git commit hash of the project that is currently getting analyzed.
+-/
+def getProjectCommit (directory : System.FilePath := "." ) : IO String := do
+  let out ← IO.Process.output {
+    cmd := "git",
+    args := #["rev-parse", "HEAD"]
+    cwd := directory
+  }
+  if out.exitCode != 0 then
+    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)
+  let commit ← getProjectCommit pkg.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
+
 module_facet docs (mod) : FilePath := do
   let some docGen4 ← findLeanExe? `«doc-gen4»
     | error "no doc-gen4 executable configuration found in workspace"
   let exeJob ← docGen4.exe.fetch
   let modJob ← mod.leanArts.fetch
-  let buildDir := (← getWorkspace).root.buildDir
+  let ws ← getWorkspace
+  let pkg ← ws.packages.find? (·.isLocalModule mod.name)
+  let libConfig ← pkg.leanLibConfigs.toArray.find? (·.isLocalModule mod.name)
   -- Build all documentation imported modules
   let imports ← mod.imports.fetch
   let depDocJobs ← BuildJob.mixArray <| ← imports.mapM fun mod => fetch <| mod.facet `docs
+  let gitUrl ← getGitUrl pkg libConfig mod
+  let buildDir := ws.root.buildDir
   let docFile := mod.filePath (buildDir / "doc") "html"
   depDocJobs.bindAsync fun _ depDocTrace => do
   exeJob.bindAsync fun exeFile exeTrace => do
@@ -41,8 +104,8 @@ module_facet docs (mod) : FilePath := do
       logStep s!"Documenting module: {mod.name}"
       proc {
         cmd := exeFile.toString
-        args := #["single", mod.name.toString]
+        args := #["single", mod.name.toString, gitUrl]
-        env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
+        env := ← getAugmentedEnv
       }
     return (docFile, trace)
 
@@ -59,7 +122,7 @@ target coreDocs : FilePath := do
       proc {
         cmd := exeFile.toString
         args := #["genCore"]
-        env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)]
+        env := ← getAugmentedEnv
       }
     return (dataFile, trace)