From 3ef381bb6cb68ee6eeb49ae8a6ae3174db9dcbf8 Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Wed, 14 Jul 2021 12:46:07 -0400
Subject: [PATCH] refactor: merge `Proc` into `Compile` and cleanup `Build`

---
 Lake/Build.lean       | 48 +++++++++++++++----------------------------
 Lake/BuildTarget.lean | 36 ++++++++++++++++++++++----------
 Lake/Compile.lean     | 39 +++++++++++++++++++++++------------
 Lake/Git.lean         | 30 +++++++++++++++++++--------
 Lake/Init.lean        |  1 -
 Lake/Proc.lean        | 18 ----------------
 6 files changed, 90 insertions(+), 82 deletions(-)
 delete mode 100644 Lake/Proc.lean

diff --git a/Lake/Build.lean b/Lake/Build.lean
index 19eebaf24b..ee90697f7a 100644
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@@ -21,10 +21,10 @@ abbrev FileTarget := MTimeBuildTarget FilePath
 
 namespace FileTarget
 
-def mk (file : FilePath) (maxMTime : IO.FS.SystemTime) (task : BuildTask) :=
+def mk (file : FilePath) (maxMTime : MTime) (task : BuildTask) :=
   BuildTarget.mk file maxMTime task
 
-def pure (file : FilePath) (maxMTime : IO.FS.SystemTime) :=
+def pure (file : FilePath) (maxMTime : MTime) :=
   BuildTarget.pure file maxMTime
 
 end FileTarget
@@ -122,16 +122,9 @@ def skipIfNewer [GetMTime a]
 
 -- # Build Components
 
-def catchErrors (action : IO PUnit) : IO PUnit := do
-  try action catch e =>
-    -- print compile errors early
-    IO.eprintln e
-    throw e
-
 def buildO (oFile : FilePath)
-(cTarget : FileTarget) (leancArgs : Array String := #[]) : IO BuildTask :=
-  BuildTask.afterTarget cTarget <| catchErrors <|
-    compileO oFile cTarget.artifact leancArgs
+(cTarget : BuildTarget t FilePath) (leancArgs : Array String := #[]) : IO BuildTask :=
+  afterTarget cTarget <| compileO oFile cTarget.artifact leancArgs
 
 def fetchOFileTarget (oFile : FilePath)
 (cTarget : FileTarget) (leancArgs : Array String := #[]) : IO FileTarget :=
@@ -225,8 +218,8 @@ def fetchAfterDirectLocalImports
     let cFile := pkg.modToC mod
     let oleanFile := pkg.modToOlean mod
     let importTasks := importTargets.map (·.buildTask)
-    BuildTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ← skipIf sameHash <|
-      BuildTask.afterTasks (depsTarget.buildTask :: importTasks) <| catchErrors do
+    BuildTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ←
+      skipIf sameHash <| afterTaskList (depsTarget.buildTask :: importTasks) do
         compileOleanAndC leanFile oleanFile cFile leanPath pkg.dir pkg.leanArgs
         IO.FS.writeFile hashFile (toString fullHash)
 
@@ -234,14 +227,11 @@ def fetchAfterDirectLocalImports
   Equivalent to `RBTopT (cmp := Name.quickCmp) Name ModuleTarget IO`.
   Phrased this way to use `NameMap`.
 -/
-abbrev LeanTargetM :=
+abbrev ModuleTargetM :=
   EStateT (List Name) (NameMap ModuleTarget) IO
 
-abbrev LeanTargetFetch :=
-  RecFetch Name ModuleTarget LeanTargetM
-
-abbrev RecLeanTargetM :=
-  ReaderT (RecFetch Name ModuleTarget LeanTargetM) LeanTargetM
+abbrev ModuleTargetFetch :=
+  RecFetch Name ModuleTarget ModuleTargetM
 
 def throwOnCycle (mx : IO (Except (List Name) α)) : IO α  :=
   mx >>= fun
@@ -260,7 +250,7 @@ def Package.buildModuleTargets
 (mods : List Name) (oleanDirs : List FilePath)
 (depsTarget : LeanTarget PUnit) (self : Package)
 : IO (List ModuleTarget) := do
-  let fetch : LeanTargetFetch :=
+  let fetch : ModuleTargetFetch :=
     fetchAfterDirectLocalImports self oleanDirs depsTarget
   throwOnCycle <| mods.mapM (buildRBTop fetch) |>.run' {}
 
@@ -337,22 +327,19 @@ def PackageTarget.fetchOFileTargets
 (self : PackageTarget) : IO (List FileTarget) := do
   self.moduleTargets.toList.mapM fun (mod, target) => do
     let oFile := self.package.modToO mod
-    fetchOFileTarget oFile target.cTarget self.package.leancArgs
+    fetchOFileTarget (oFile) target.cTarget self.package.leancArgs
 
 def PackageTarget.buildStaticLib
 (self : PackageTarget) : IO BuildTask := do
   let oFileTargets ← self.fetchOFileTargets
   let oFiles := oFileTargets.map (·.artifact) |>.toArray
-  BuildTask.afterTargets oFileTargets <| catchErrors <|
-    compileStaticLib self.package.staticLibFile oFiles
+  oFileTargets >> compileStaticLib self.package.staticLibFile oFiles
 
-def PackageTarget.fetchStaticLibTarget
-(self : PackageTarget) : IO FileTarget := do
+def PackageTarget.fetchStaticLibTarget (self : PackageTarget) : IO FileTarget := do
   skipIfNewer self.package.staticLibFile self.mtime self.buildStaticLib
 
 def Package.fetchStaticLibTarget (self : Package) : IO FileTarget := do
-  let target ← self.buildTarget
-  target.fetchStaticLibTarget
+  (← self.buildTarget).fetchStaticLibTarget
 
 def Package.fetchStaticLib (self : Package) : IO FilePath := do
   let target ← self.fetchStaticLibTarget
@@ -370,11 +357,10 @@ def PackageTarget.buildBin
 (depTargets : List PackageTarget) (self : PackageTarget)
 : IO BuildTask := do
   let oFileTargets ← self.fetchOFileTargets
-  let oFiles := oFileTargets.map (·.artifact) |>.toArray
   let libTargets ← depTargets.mapM (·.fetchStaticLibTarget)
-  let libFiles := libTargets.map (·.artifact) |>.toArray
-  BuildTask.afterTargets (oFileTargets ++ libTargets) <| catchErrors <|
-    compileBin self.package.binFile (oFiles ++ libFiles) self.package.linkArgs
+  let linkTargets := oFileTargets ++ libTargets
+  let linkFiles := linkTargets.map (·.artifact) |>.toArray
+  linkTargets >> compileBin self.package.binFile linkFiles self.package.linkArgs
 
 def PackageTarget.fetchBinTarget
 (depTargets : List PackageTarget) (self : PackageTarget) : IO FileTarget :=
diff --git a/Lake/BuildTarget.lean b/Lake/BuildTarget.lean
index cb89baffc5..538a37d2c8 100644
--- a/Lake/BuildTarget.lean
+++ b/Lake/BuildTarget.lean
@@ -6,6 +6,8 @@ Authors: Mac Malone
 
 namespace Lake
 
+-- # Build Task
+
 def BuildTask := Task (Except IO.Error PUnit)
 
 namespace BuildTask
@@ -13,22 +15,32 @@ namespace BuildTask
 def nop : BuildTask :=
   Task.pure (Except.ok ())
 
+def spawn (action : IO PUnit) (prio := Task.Priority.dedicated) : IO BuildTask :=
+  IO.asTask action prio
+
 def await (self : BuildTask) : IO PUnit := do
   IO.ofExcept (← IO.wait self)
 
 def all (tasks : List BuildTask) : IO BuildTask :=
   IO.asTask (tasks.forM (·.await))
 
-def afterTask (task : BuildTask) (action : IO PUnit)  : IO BuildTask :=
-  IO.mapTask (fun x => IO.ofExcept x *> action) task
-
-def afterTasks (tasks : List BuildTask) (action : IO PUnit) : IO BuildTask :=
-  IO.mapTasks (fun xs => xs.forM IO.ofExcept *> action) <| tasks
-
 end BuildTask
 
 instance : Inhabited BuildTask := ⟨BuildTask.nop⟩
 
+def afterTask (task : BuildTask) (action : IO PUnit)  : IO BuildTask :=
+  IO.mapTask (fun x => IO.ofExcept x *> action) task
+
+def afterTaskList (tasks : List BuildTask) (action : IO PUnit) : IO BuildTask :=
+  IO.mapTasks (fun xs => xs.forM IO.ofExcept *> action) <| tasks
+
+instance : HAndThen BuildTask (IO PUnit) (IO BuildTask) :=
+  ⟨afterTask⟩
+
+instance : HAndThen (List BuildTask) (IO PUnit) (IO BuildTask) :=
+  ⟨afterTaskList⟩
+
+-- # Build Target
 
 structure BuildTarget (t : Type) (a : Type) where
   artifact    : a
@@ -61,15 +73,17 @@ def materialize (self : BuildTarget t α) : IO PUnit :=
 
 end BuildTarget
 
-namespace BuildTask
-
 def afterTarget (target : BuildTarget t a) (action : IO PUnit)  : IO BuildTask :=
   afterTask target.buildTask action
 
-def afterTargets (targets : List (BuildTarget t a)) (action : IO PUnit) : IO BuildTask :=
-  afterTasks (targets.map (·.buildTask)) action
+def afterTargetList (targets : List (BuildTarget t a)) (action : IO PUnit) : IO BuildTask :=
+  afterTaskList (targets.map (·.buildTask)) action
 
-end BuildTask
+instance : HAndThen (BuildTarget t a) (IO PUnit) (IO BuildTask) :=
+  ⟨afterTarget⟩
+
+instance : HAndThen (List (BuildTarget t a)) (IO PUnit) (IO BuildTask) :=
+  ⟨afterTargetList⟩
 
 -- # Hash Traces
 
diff --git a/Lake/Compile.lean b/Lake/Compile.lean
index 32828dc094..234bb0bd74 100644
--- a/Lake/Compile.lean
+++ b/Lake/Compile.lean
@@ -1,22 +1,35 @@
 /-
-Copyright (c) 2021 Mac Malone. All rights reserved.
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mac Malone
+Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
-import Lake.Proc
+import Lake.BuildTarget
 
 namespace Lake
 open System
 
-def createParentDirs (path : FilePath) : IO Unit :=
-  if let some dir := path.parent then IO.FS.createDirAll dir else pure ()
+def createParentDirs (path : FilePath) : IO PUnit := do
+  if let some dir := path.parent then
+    try IO.FS.createDirAll dir catch e => IO.eprintln e
+
+def proc (args : IO.Process.SpawnArgs) : IO PUnit := do
+  let envStr := String.join <| args.env.toList.map fun (k, v) => s!"{k}={v.getD ""} "
+  let cmdStr := " ".intercalate (args.cmd :: args.args.toList)
+  IO.println <| "> " ++ envStr ++
+    match args.cwd with
+    | some cwd => s!"{cmdStr}    # in directory {cwd}"
+    | none     => cmdStr
+  let child ← IO.Process.spawn args
+  let exitCode ← child.wait
+  if exitCode != 0 then
+    IO.eprintln s!"external command exited with status {exitCode}"
 
 def compileOleanAndC (leanFile oleanFile cFile : FilePath)
 (leanPath : String := "") (rootDir : FilePath := ".") (leanArgs : Array String := #[])
-: IO Unit := do
+: IO PUnit := do
   createParentDirs cFile
   createParentDirs oleanFile
-  execCmd {
+  proc {
     cmd := "lean"
     args := leanArgs ++ #[
       "-R", rootDir.toString, "-o", oleanFile.toString, "-c",
@@ -26,25 +39,25 @@ def compileOleanAndC (leanFile oleanFile cFile : FilePath)
   }
 
 def compileO (oFile cFile : FilePath)
-(leancArgs : Array String := #[]) : IO Unit := do
+(leancArgs : Array String := #[]) : IO PUnit := do
   createParentDirs oFile
-  execCmd {
+  proc {
     cmd := "leanc"
     args := #["-c", "-o", oFile.toString, cFile.toString] ++ leancArgs
   }
 
 def compileStaticLib
-(libFile : FilePath) (oFiles : Array FilePath) : IO Unit := do
+(libFile : FilePath) (oFiles : Array FilePath) : IO PUnit := do
   createParentDirs libFile
-  execCmd {
+  proc {
     cmd := "ar"
     args := #["rcs", libFile.toString] ++ oFiles.map toString
   }
 
 def compileBin (binFile : FilePath)
-(linkFiles : Array FilePath) (linkArgs : Array String := #[]) : IO Unit := do
+(linkFiles : Array FilePath) (linkArgs : Array String := #[]) : IO PUnit := do
   createParentDirs binFile
-  execCmd {
+  proc {
     cmd := "leanc"
     args := #["-o", binFile.toString] ++ linkFiles.map toString ++ linkArgs
   }
diff --git a/Lake/Git.lean b/Lake/Git.lean
index d6afd45501..bde51c16cb 100644
--- a/Lake/Git.lean
+++ b/Lake/Git.lean
@@ -3,7 +3,6 @@ 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.Proc
 import Lake.LeanVersion
 
 open System
@@ -17,23 +16,38 @@ 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}
+  if out.exitCode != 0 then
+    throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
+  return out.stdout
+
 def clone (url : String) (dir : FilePath) :=
-  execCmd {cmd := "git", args := #["clone", url, dir.toString]}
+  execGit #["clone", url, dir.toString]
 
 def quietInit (repo : Option FilePath := none) :=
-  execCmd {cmd := "git", args := #["init", "-q"]}
+  execGit #["init", "-q"] repo
 
 def fetch (repo : Option FilePath := none) :=
-  execCmd {cmd := "git", args := #["fetch"], cwd := repo}
+  execGit #["fetch"] repo
 
 def checkoutBranch (branch : String) (repo : Option FilePath := none) :=
-  execCmd {cmd := "git", args := #["checkout", "-B", branch]}
+  execGit #["checkout", "-B", branch] repo
 
 def checkoutDetach (hash : String) (repo : Option FilePath := none)  :=
-  execCmd {cmd := "git", args := #["checkout", "--detach", hash], cwd := repo}
+  execGit #["checkout", "--detach", hash] repo
 
 def parseRevision (rev : String) (repo : Option FilePath := none) : IO String := do
-  let rev ← IO.Process.run {cmd := "git", args := #["rev-parse", "-q", "--verify", rev], cwd := repo}
+  let rev ← captureGit #["rev-parse", "-q", "--verify", rev] repo
   rev.trim -- remove newline at end
 
 def headRevision (repo : Option FilePath := none) : IO String :=
@@ -44,7 +58,7 @@ def parseOriginRevision (rev : String) (repo : Option FilePath := none) : IO Str
     <|> throw (IO.userError s!"cannot find revision {rev} in repository {repo}")
 
 def latestOriginRevision (branch : Option String) (repo : Option FilePath := none) : IO String := do
-  discard <| IO.Process.run {cmd := "git", args := #["fetch"], cwd := repo}
+  execGit #["fetch"] repo
   parseOriginRevision (defaultRevision branch) repo
 
 def revisionExists (rev : String) (repo : Option FilePath := none) : IO Bool := do
diff --git a/Lake/Init.lean b/Lake/Init.lean
index 3685453121..7ad5181028 100644
--- a/Lake/Init.lean
+++ b/Lake/Init.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lake.Git
-import Lake.Proc
 import Lake.LeanConfig
 
 namespace Lake
diff --git a/Lake/Proc.lean b/Lake/Proc.lean
deleted file mode 100644
index 83d8db043c..0000000000
--- a/Lake/Proc.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-/-
-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
--/
-namespace Lake
-
-def execCmd (args : IO.Process.SpawnArgs) : IO Unit := do
-  let envstr := String.join <| args.env.toList.map fun (k, v) => s!"{k}={v.getD ""} "
-  let cmdstr := " ".intercalate (args.cmd :: args.args.toList)
-  IO.eprintln <| "> " ++ envstr ++
-    match args.cwd with
-    | some cwd => s!"{cmdstr}    # in directory {cwd}"
-    | none     => cmdstr
-  let child ← IO.Process.spawn args
-  let exitCode ← child.wait
-  if exitCode != 0 then
-    throw <| IO.userError <| s!"external command exited with status {exitCode}"