refactor: typify git repos + log stdout/stderr on git failures

c.f. leanprover/lake#67

Lake/Build/Context.lean

@@ -38,7 +38,7 @@ instance : MonadLift IO BuildM := ⟨MonadError.runIO⟩
 instance [Pure m] : MonadLift LakeM (BuildT m) where
   monadLift x := fun ctx => pure <| x.run ctx.toContext
 
-instance : MonadLift (LogT IO) BuildM where
+instance : MonadLift LogIO BuildM where
   monadLift x := fun ctx meths => liftM (n := BuildM) (x.run meths.lift) ctx meths
 
 def BuildM.run (logMethods : MonadLog BaseIO) (ctx : BuildContext) (self : BuildM α) : IO α :=

Lake/CLI/Init.lean

@@ -123,7 +123,7 @@ def InitTemplate.configFileContents (pkgName root : Name) : InitTemplate → Str
 instance : Inhabited InitTemplate := ⟨.std⟩
 
 /-- Initialize a new Lake package in the given directory with the given name. -/
-def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogT IO PUnit := do
+def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit := do
   let pkgName := name.decapitalize.toName
 
   -- determine the name to use for the root
@@ -168,17 +168,18 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogT IO PUni
 
   -- initialize a `.git` repository if none already
   unless (← FilePath.isDir <| dir / ".git") do
+    let repo := GitRepo.mk dir
     try
-      quietInit dir
+      repo.quietInit
       unless upstreamBranch = "master" do
-        checkoutBranch upstreamBranch dir
+        repo.checkoutBranch upstreamBranch
     catch _ =>
       logWarning "failed to initialize git repository"
 
-def init (pkgName : String) (tmp : InitTemplate) : LogT IO PUnit :=
+def init (pkgName : String) (tmp : InitTemplate) : LogIO PUnit :=
   initPkg "." pkgName tmp
 
-def new (pkgName : String) (tmp : InitTemplate) : LogT IO PUnit := do
+def new (pkgName : String) (tmp : InitTemplate) : LogIO PUnit := do
   let dirName := pkgName.map fun chr => if chr == '.' then '-' else chr
   IO.FS.createDir dirName
   initPkg dirName pkgName tmp

Lake/CLI/Main.lean

@@ -35,11 +35,11 @@ structure LakeConfig where
   lakeInstall : LakeInstall
   args : List String := []
 
-def loadPkg (config : LakeConfig) : LogT IO Package := do
+def loadPkg (config : LakeConfig) : LogIO Package := do
   setupLeanSearchPath config.leanInstall config.lakeInstall
   Package.load config.rootDir config.args (config.rootDir / config.configFile)
 
-def loadManifestMap (manifestFile : FilePath) : LogT IO (Lean.NameMap PackageEntry) := do
+def loadManifestMap (manifestFile : FilePath) : LogIO (Lean.NameMap PackageEntry) := do
   if let Except.ok contents ← IO.FS.readFile manifestFile  |>.toBaseIO then
     match Json.parse contents with
       | Except.ok json =>
@@ -55,7 +55,7 @@ def loadManifestMap (manifestFile : FilePath) : LogT IO (Lean.NameMap PackageEnt
   else
     pure {}
 
-def loadWorkspace (config : LakeConfig) (updateDeps := false) : LogT IO Workspace := do
+def loadWorkspace (config : LakeConfig) (updateDeps := false) : LogIO Workspace := do
   let pkg ← loadPkg config
   let ws := Workspace.ofPackage pkg
   let manifestMap ← loadManifestMap ws.manifestFile
@@ -221,7 +221,7 @@ def printPaths (config : LakeConfig) (imports : List String := []) : MainM PUnit
 def env (cmd : String) (args : Array String := #[]) : LakeT IO UInt32 := do
   IO.Process.spawn {cmd, args, env := ← getLeanEnv} >>= (·.wait)
 
-def serve (config : LakeConfig) (args : Array String) : LogT IO UInt32 := do
+def serve (config : LakeConfig) (args : Array String) : LogIO UInt32 := do
   let (extraEnv, moreServerArgs) ←
     try
       let ws ← loadWorkspace config

Lake/Config/Load.lean

@@ -20,7 +20,7 @@ def defaultConfigFile : FilePath := "lakefile.lean"
 /-- Evaluate a `package` declaration to its respective `PackageConfig`. -/
 unsafe def evalPackageDecl (env : Environment) (declName : Name)
 (dir : FilePath) (args : List String := []) (leanOpts := Options.empty)
-: LogT IO PackageConfig := do
+: LogIO PackageConfig := do
   let m := env.evalConstCheck IOPackager leanOpts ``IOPackager declName
   if let Except.ok ioPackager := m.run.run then
     logWarning "Support for IO in package declarations may be dropped. Raise an issue if you disagree."
@@ -67,7 +67,7 @@ namespace Package
 /-- Unsafe implementation of `load`. -/
 unsafe def loadUnsafe (dir : FilePath) (args : List String := [])
 (configFile := dir / defaultConfigFile) (leanOpts := Options.empty)
-: LogT IO Package := do
+: LogIO Package := do
 
   -- Read File & Initialize Environment
   let input ← IO.FS.readFile configFile
@@ -145,4 +145,4 @@ the given directory with the given configuration file.
 -/
 @[implementedBy loadUnsafe]
 opaque load (dir : FilePath) (args : List String := [])
-(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogT IO Package
+(configFile := dir / defaultConfigFile) (leanOpts := Options.empty) : LogIO Package

Lake/Config/Resolve.lean

@@ -15,31 +15,28 @@ open Std System
 
 namespace Lake
 
-section
-open Git
-
-/-- Update the Git package in `dir` to `rev` if not already at it. -/
+/-- Update the Git package in `repo` to `rev` if not already at it. -/
 def updateGitPkg (name : String)
-(dir : FilePath) (rev? : Option String) : LogT IO PUnit := do
+(repo : GitRepo) (rev? : Option String) : LogIO PUnit := do
   if let some rev := rev? then
-    if (← headRevision dir) == rev then return
-    logInfo s!"{name}: updating {dir} to revision {rev}"
-    unless ← revisionExists rev dir do fetch dir
-    checkoutDetach rev dir
+    if (← repo.headRevision) == rev then return
+    logInfo s!"{name}: updating {repo} to revision {rev}"
+    unless ← repo.revisionExists rev do repo.fetch
+    repo.checkoutDetach rev
   else
-    logInfo s!"{name}: updating {dir}"
-    pull dir
+    logInfo s!"{name}: updating {repo}"
+    repo.pull
 
-/-- Clone the Git package as `dir`. -/
-def cloneGitPkg (name : String) (dir : FilePath)
-(url : String) (rev? : Option String) : LogT IO PUnit := do
-  logInfo s!"{name}: cloning {url} to {dir}"
-  clone url dir
+/-- Clone the Git package as `repo`. -/
+def cloneGitPkg (name : String) (repo : GitRepo)
+(url : String) (rev? : Option String) : LogIO PUnit := do
+  logInfo s!"{name}: cloning {url} to {repo}"
+  repo.clone url
   if let some rev := rev? then
-    let hash ← parseOriginRevision rev dir
-    checkoutDetach hash dir
+    let hash ← repo.parseOriginRevision rev
+    repo.checkoutDetach hash
 
-abbrev ResolveM := StateT (NameMap PackageEntry) <| LogT IO
+abbrev ResolveM := StateT (NameMap PackageEntry) <| LogIO
 
 /--
 Materializes a Git package in `dir`, cloning and/or updating it as necessary.
@@ -50,39 +47,38 @@ and saves the result to the manifest.
 -/
 def materializeGitPkg (name : String) (dir : FilePath)
 (url : String) (rev? : Option String) (shouldUpdate := true) : ResolveM PUnit := do
+  let repo := GitRepo.mk dir
   if let some entry := (← get).find? name then
-    if (← dir.isDir) then
+    if (← repo.dirExists) then
       if url = entry.url then
         if shouldUpdate then
-          updateGitPkg name dir rev?
-          let rev ← headRevision dir
+          updateGitPkg name repo rev?
+          let rev ← repo.headRevision
           modify (·.insert name {entry with rev})
         else
-          updateGitPkg name dir entry.rev
+          updateGitPkg name repo entry.rev
       else if shouldUpdate then
         logInfo s!"{name}: URL changed, deleting {dir} and cloning again"
         IO.FS.removeDirAll dir
-        cloneGitPkg name dir url rev?
-        let rev ← headRevision dir
+        cloneGitPkg name repo url rev?
+        let rev ← repo.headRevision
         modify (·.insert name {entry with url, rev})
     else
       if shouldUpdate then
-        cloneGitPkg name dir url rev?
-        let rev ← headRevision dir
+        cloneGitPkg name repo url rev?
+        let rev ← repo.headRevision
         modify (·.insert name {entry with url, rev})
       else
-        cloneGitPkg name dir entry.url entry.rev
+        cloneGitPkg name repo entry.url entry.rev
   else
-    if (← dir.isDir) then
-      let rev ← headRevision dir
+    if (← repo.dirExists) then
+      let rev ← repo.headRevision
       modify (·.insert name {name, url, rev})
     else
-      cloneGitPkg name dir url rev?
-      let rev ← headRevision dir
+      cloneGitPkg name repo url rev?
+      let rev ← repo.headRevision
       modify (·.insert name {name, url, rev})
 
-end
-
 /--
 Materializes a `Dependency` relative to the given `Package`,
 downloading and/or updating it as necessary.

Lake/Util/Git.lean

@@ -3,9 +3,13 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
+import Lake.Util.Log
+import Lake.Util.Misc
 
 open System
-namespace Lake.Git
+namespace Lake
+
+namespace Git
 
 def upstreamBranch :=
   "master"
@@ -17,57 +21,81 @@ def defaultRevision : Option String → String
   | none => upstreamBranch
   | some branch => branch
 
-def execGit (args : Array String) (repo : Option FilePath := none) : IO PUnit := do
-  let child ← IO.Process.spawn {
-    cmd := "git", args, cwd := repo,
-    stdout := IO.Process.Stdio.null, stderr := IO.Process.Stdio.null
-  }
-  let exitCode ← child.wait
-  if exitCode != 0 then
-    throw <| IO.userError <| "git exited with code " ++ toString exitCode
-
-def captureGit (args : Array String) (repo : Option FilePath := none) : IO String := do
-  let out ← IO.Process.output {cmd := "git", args, cwd := repo}
+def capture (args : Array String) (wd : Option FilePath := none) : LogIO String := do
+  let out ← IO.Process.output {cmd := "git", args, cwd := wd}
   if out.exitCode != 0 then
-    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
+    logError s!"stdout:\n{out.stdout}\nstderr:\n{out.stderr}"
+    error <| "git exited with code " ++ toString out.exitCode
   return out.stdout
 
-def clone (url : String) (dir : FilePath) :=
-  execGit #["clone", url, dir.toString]
+def exec (args : Array String) (wd : Option FilePath := none) : LogIO PUnit := do
+  discard <| capture args wd
 
-def quietInit (repo : Option FilePath := none) :=
-  execGit #["init", "-q"] repo
+def test (args : Array String) (wd : Option FilePath := none) : LogT BaseIO Bool :=
+  let act : IO _ := do
+    let child ← IO.Process.spawn {cmd := "git", args, cwd := wd}
+    return (← child.wait) == 0
+  act.catchExceptions fun _ => pure false
 
-def fetch (repo : Option FilePath := none) :=
-  execGit #["fetch"] repo
+end Git
 
-def pull (repo : Option FilePath := none) :=
-  execGit #["pull"] repo
+structure GitRepo where
+  dir : FilePath
 
-def checkoutBranch (branch : String) (repo : Option FilePath := none) :=
-  execGit #["checkout", "-B", branch] repo
+instance : ToString GitRepo := ⟨(·.dir.toString)⟩
 
-def checkoutDetach (hash : String) (repo : Option FilePath := none)  :=
-  execGit #["checkout", "--detach", hash] repo
+namespace GitRepo
 
-def parseRevision (rev : String) (repo : Option FilePath := none) : IO String := do
-  let rev ← captureGit #["rev-parse", "-q", "--verify", rev] repo
+def cwd : GitRepo := ⟨"."⟩
+
+def dirExists (repo : GitRepo) : BaseIO Bool :=
+  repo.dir.isDir
+
+def captureGit (args : Array String) (repo : GitRepo) : LogIO String :=
+  Git.capture args repo.dir
+
+def execGit (args : Array String) (repo : GitRepo) : LogIO PUnit :=
+  Git.exec args repo.dir
+
+def testGit (args : Array String) (repo : GitRepo) : LogIO Bool :=
+  Git.test args repo.dir
+
+def clone (url : String) (repo : GitRepo) : LogIO PUnit  :=
+  Git.exec #["clone", url, repo.dir.toString]
+
+def quietInit (repo : GitRepo) : LogIO PUnit  :=
+  repo.execGit #["init", "-q"]
+
+def fetch (repo : GitRepo) : LogIO PUnit  :=
+  repo.execGit #["fetch"]
+
+def pull (repo : GitRepo) : LogIO PUnit  :=
+  repo.execGit #["pull"]
+
+def checkoutBranch (branch : String) (repo : GitRepo) : LogIO PUnit :=
+  repo.execGit #["checkout", "-B", branch]
+
+def checkoutDetach (hash : String) (repo : GitRepo) : LogIO PUnit  :=
+  repo.execGit #["checkout", "--detach", hash]
+
+def parseRevision (rev : String) (repo : GitRepo) : LogIO String := do
+  let rev ← repo.captureGit #["rev-parse", "--verify", rev]
   pure rev.trim -- remove newline at end
 
-def headRevision (repo : Option FilePath := none) : IO String :=
+def headRevision (repo : GitRepo) : LogIO String :=
   parseRevision "HEAD" repo
 
-def parseOriginRevision (rev : String) (repo : Option FilePath := none) : IO String := do
-  if isFullObjectName rev then return rev
-  (parseRevision ("origin/" ++ rev) repo) <|> parseRevision rev repo
-    <|> throw (IO.userError s!"cannot find revision {rev} in repository {repo}")
+def parseOriginRevision (rev : String) (repo : GitRepo) : LogIO String := do
+  if Git.isFullObjectName rev then return rev
+  repo.parseRevision ("origin/" ++ rev) <|> repo.parseRevision rev
+    <|> error s!"cannot find revision {rev} in repository {repo}"
 
-def latestOriginRevision (branch : Option String) (repo : Option FilePath := none) : IO String := do
-  execGit #["fetch"] repo
-  parseOriginRevision (defaultRevision branch) repo
+def latestOriginRevision (branch : Option String) (repo : GitRepo) : LogIO String := do
+  repo.execGit #["fetch"]
+  parseOriginRevision (Git.defaultRevision branch) repo
 
-def revisionExists (rev : String) (repo : Option FilePath := none) : IO Bool := do
-  try
-    discard <| parseRevision (rev ++ "^{commit}") repo
-    pure true
-  catch _ => pure false
+def branchExists (rev : String) (repo : GitRepo) : LogIO Bool := do
+  repo.testGit #["show-ref", "--verify", s!"refs/heads/{rev}"]
+
+def revisionExists (rev : String) (repo : GitRepo) : LogIO Bool := do
+  repo.testGit #["rev-parse", "--verify", rev ++ "^{commit}"]

Lake/Util/Log.lean

@@ -83,6 +83,9 @@ abbrev adaptMethods [Monad n]
 
 end MonadLogT
 
+abbrev LogIO :=
+  MonadLogT BaseIO IO
+
 abbrev LogT (m : Type → Type) :=
   MonadLogT m m
 

Lake/Util/MainM.lean

@@ -75,4 +75,4 @@ protected def error (msg : String) (rc : ExitCode := 1) : MainM α := do
 instance : MonadError MainM := ⟨MainM.error⟩
 instance [ToString ε] : MonadLift (EIO ε) MainM := ⟨MonadError.runEIO⟩
 instance : MonadLift IO MainM := inferInstance -- necessary, but don't know why
-instance : MonadLift (LogT IO) MainM := ⟨fun x => liftM <| x.run MonadLog.eio⟩
+instance : MonadLift LogIO MainM := ⟨fun x => liftM <| x.run MonadLog.eio⟩