From f9d987567129f422ebd8cfac6a1e6233a06c720b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Mon, 9 Oct 2023 09:30:16 +0200 Subject: [PATCH] perf: Don't call Lake from within doc-gen anymore --- DocGen4/Load.lean | 19 +------ DocGen4/Output.lean | 16 +++--- DocGen4/Output/Base.lean | 10 ---- DocGen4/Output/SourceLinker.lean | 85 ++------------------------------ Main.lean | 26 ++++------ lakefile.lean | 71 ++++++++++++++++++++++++-- 6 files changed, 89 insertions(+), 138 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index b40e7d5..c579837 100644 --- a/DocGen4/Load.lean +++ b/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 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 8548b0f..f7ca30b 100644 --- a/DocGen4/Output.lean +++ b/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 sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath - let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath + let some p := (← IO.getEnv "LEAN_SRC_PATH") | throw <| IO.userError "LEAN_SRC_PATH not found in env" + let sourceSearchPath := System.SearchPath.parse p 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 diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 260bf47..bb48a0f 100644 --- a/DocGen4/Output/Base.lean +++ b/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 diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean index 9829388..977922c 100644 --- a/DocGen4/Output/SourceLinker.lean +++ b/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 - let leanHash := ws.lakeEnv.lean.githash - -- Compute a map from package names to source URL - 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) - +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 => 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 - | 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" + gitUrl?.get! match range with | some range => s!"{basic}#L{range.pos.line}-L{range.endPos.line}" diff --git a/Main.lean b/Main.lean index aa262c7..2bab169 100644 --- a/Main.lean +++ b/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 - match res with - | Except.ok ws => - let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules - let baseConfig ← getSimpleBaseContext hierarchy - htmlOutputResults baseConfig doc ws (p.hasFlag "ink") - return 0 - | Except.error rc => pure rc + let gitUrl := p.positionalArg! "gitUrl" |>.as! String + let (doc, hierarchy) ← load <| .loadAllLimitAnalysis relevantModules + let baseConfig ← getSimpleBaseContext hierarchy + htmlOutputResults baseConfig doc (some gitUrl) (p.hasFlag "ink") + return 0 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) - return 0 - | Except.error rc => pure rc + let (doc, hierarchy) ← loadCore + let baseConfig ← getSimpleBaseContext hierarchy + htmlOutputResults baseConfig doc none (ink := False) + return 0 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| diff --git a/lakefile.lean b/lakefile.lean index 8f33e46..9757492 100644 --- a/lakefile.lean +++ b/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] - env := #[("LEAN_PATH", (← getAugmentedLeanPath).toString)] + args := #["single", mod.name.toString, gitUrl] + 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)