From 9cc4c787e6e90f6838bafeb040b6b337c83b9c3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 6 Mar 2022 18:51:06 +0100 Subject: [PATCH] feat: lake integration --- DocGen4/Load.lean | 46 ++++++++++++++------------------------ DocGen4/Output.lean | 54 ++++++++++++++++++++++++++++++--------------- Main.lean | 15 ++++++++----- lakefile.lean | 4 ++++ 4 files changed, 65 insertions(+), 54 deletions(-) diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index e49f23b..841891a 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -5,6 +5,7 @@ Authors: Henrik Böving -/ import Lean +import Lake import DocGen4.Process import Std.Data.HashMap @@ -12,40 +13,25 @@ namespace DocGen4 open Lean System Std IO -def getLakePath : IO FilePath := do - match (← IO.getEnv "LAKE") with - | some path => pure $ System.FilePath.mk path - | none => - let lakePath := (←findSysroot) / "bin" / "lake" - pure $ lakePath.withExtension System.FilePath.exeExtension - --- Modified from the LSP Server -def lakeSetupSearchPath (lakePath : System.FilePath) (imports : List String) : IO Lean.SearchPath := do - let args := "print-paths" :: imports - let cmdStr := " ".intercalate (toString lakePath :: args) - let lakeProc ← Process.spawn { - stdin := Process.Stdio.null - stdout := Process.Stdio.piped - stderr := Process.Stdio.piped - cmd := lakePath.toString - args := args.toArray - } - let stdout := String.trim (← lakeProc.stdout.readToEnd) - let stderr := String.trim (← lakeProc.stderr.readToEnd) - match (← lakeProc.wait) with - | 0 => - let stdout := stdout.split (· == '\n') |>.getLast! - let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?) - | throw $ userError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}" - initSearchPath (← findSysroot) paths.oleanPath - paths.oleanPath.mapM realPathNormalized - | 2 => pure [] -- no lakefile.lean - | _ => throw $ userError s!"`{cmdStr}` failed:\n{stdout}\nstderr:\n{stderr}" +def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do + let (leanInstall?, lakeInstall?) ← Lake.findInstall? + let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO' + match res with + | Except.ok (ws, options) => + let lean := leanInstall?.get! + if lean.githash ≠ Lean.githash then + IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {lean.githash}" + let lake := lakeInstall?.get! + let ctx ← Lake.mkBuildContext ws lean lake + ws.root.buildImportsAndDeps imports |>.run Lake.LogMethods.eio ctx + initSearchPath (←findSysroot) ws.leanPaths.oleanPath + pure $ Except.ok (ws, lean.githash) + | Except.error rc => pure $ Except.error rc def load (imports : List Name) : IO AnalyzerResult := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty -- TODO parameterize maxHeartbeats IO.println "Processing modules" - Prod.fst <$> (Meta.MetaM.toIO process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}) + Prod.fst <$> Meta.MetaM.toIO process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {} end DocGen4 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 7351530..4412ec5 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -4,6 +4,7 @@ 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 @@ -25,12 +26,8 @@ Three link types from git supported: 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 - +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 @@ -40,30 +37,51 @@ def getGithubBaseUrl : IO String := do else pure url -def getCommit : IO String := do +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 : IO (Name → Option DeclarationRange → String) := do - let baseUrl ← getGithubBaseUrl - let commit ← getCommit - pure λ name range => - let parts := name.components.map Name.toString +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 r := name.getRoot - let basic := if r == `Lean ∨ r == `Init ∨ r == `Std then - s!"https://github.com/leanprover/lean4/blob/{githash}/src/{path}.lean" + 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 - s!"{baseUrl}/blob/{commit}/{path}.lean" + 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) (root : String) : IO Unit := do - let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker} +def htmlOutput (result : AnalyzerResult) (root : String) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do + let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash} let basePath := FilePath.mk "." / "build" / "doc" let indexHtml := ReaderT.run index config let findHtml := ReaderT.run find config diff --git a/Main.lean b/Main.lean index 4a7c71d..e8b2d82 100644 --- a/Main.lean +++ b/Main.lean @@ -7,12 +7,15 @@ open DocGen4 Lean Cli def runDocGenCmd (p : Parsed) : IO UInt32 := do let root := p.positionalArg! "root" |>.as! String let modules : List String := p.variableArgsAs! String |>.toList - let path ← lakeSetupSearchPath (←getLakePath) modules - IO.println s!"Loading modules from: {path}" - let doc ← load $ modules.map Name.mkSimple - IO.println "Outputting HTML" - htmlOutput doc root - pure 0 + let res ← lakeSetup modules + match res with + | Except.ok (ws, leanHash) => + IO.println s!"Loading modules from: {←searchPathRef.get}" + let doc ← load $ modules.map Name.mkSimple + IO.println "Outputting HTML" + htmlOutput doc root ws leanHash + pure 0 + | Except.error rc => pure rc def docGenCmd : Cmd := `[Cli| "doc-gen4" VIA runDocGenCmd; ["0.0.1"] diff --git a/lakefile.lean b/lakefile.lean index 9d9c138..d18d59c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -16,6 +16,10 @@ package «doc-gen4» { { name := `Cli src := Source.git "https://github.com/mhuisi/lean4-cli" "1f8663e3dafdcc11ff476d74ef9b99ae5bdaedd3" + }, + { + name := `lake + src := Source.git "https://github.com/leanprover/lake" "9378575b5575f49a185d50130743a190a9be2f82" } ] }