Merge pull request #46 from leanprover/lake

Lake integration

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
+def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × String)) := do
-  match (← IO.getEnv "LAKE") with
+  let (leanInstall?, lakeInstall?) ← Lake.findInstall?
-  | some path => pure $ System.FilePath.mk path
+  let res ← StateT.run Lake.Cli.loadWorkspace {leanInstall?, lakeInstall?} |>.toIO'
-  | none =>
+  match res with
-    let lakePath := (←findSysroot?) / "bin" / "lake"
+  | Except.ok (ws, options) =>
-    pure $ lakePath.withExtension System.FilePath.exeExtension
+    let lean := leanInstall?.get!
-
+    if lean.githash ≠ Lean.githash then
--- Modified from the LSP Server
+      IO.println s!"WARNING: This doc-gen was built with Lean: {Lean.githash} but the project is running on: {lean.githash}"
-def lakeSetupSearchPath (lakePath : System.FilePath) (imports : List String) : IO Lean.SearchPath := do
+    let lake := lakeInstall?.get!
-  let args := "print-paths" :: imports
+    let ctx ← Lake.mkBuildContext ws lean lake
-  let cmdStr := " ".intercalate (toString lakePath :: args)
+    ws.root.buildImportsAndDeps imports |>.run Lake.LogMethods.eio ctx
-  let lakeProc ← Process.spawn {
+    initSearchPath (←findSysroot) ws.leanPaths.oleanPath
-    stdin  := Process.Stdio.null
+    pure $ Except.ok (ws, lean.githash)
-    stdout := Process.Stdio.piped
+  | Except.error rc => pure $ Except.error rc
-    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 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

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
+def getGithubBaseUrl (gitUrl : String) : String := Id.run do
-  let out ← IO.Process.output {cmd := "git", args := #["remote", "get-url", "origin"]}
+  let mut url := gitUrl
-  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
@@ -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
+def sourceLinker (ws : Lake.Workspace) (leanHash : String): IO (Name → Option DeclarationRange → String) := do
-  let baseUrl ← getGithubBaseUrl
+  -- Compute a map from package names to source URL
-  let commit ← getCommit
+  let mut gitMap := Std.mkHashMap
-  pure λ name range =>
+  let projectBaseUrl := getGithubBaseUrl (←getProjectGithubUrl)
-    let parts := name.components.map Name.toString
+  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 root := module.getRoot
-    let basic := if r == `Lean ∨ r == `Init ∨ r == `Std then
+    let basic := if root == `Lean ∨ root == `Init ∨ root == `Std then
-      s!"https://github.com/leanprover/lean4/blob/{githash}/src/{path}.lean"
+      s!"https://github.com/leanprover/lean4/blob/{leanHash}/src/{path}.lean"
     else
+      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
+def htmlOutput (result : AnalyzerResult) (root : String) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
-  let config := { root := root, result := result, currentName := none, sourceLinker := ←sourceLinker}
+  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

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
+  let res ← lakeSetup modules
-  IO.println s!"Loading modules from: {path}"
+  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
+    htmlOutput doc root ws leanHash
     pure 0
+  | Except.error rc => pure rc
 
 def docGenCmd : Cmd := `[Cli|
   "doc-gen4" VIA runDocGenCmd; ["0.0.1"]

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"
     }
   ]
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-27
+leanprover/lean4:nightly-2022-03-06