From 981db940e82ab62637c2cea2e713481f4c95f39a Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Thu, 8 Jul 2021 19:46:10 -0400
Subject: [PATCH] feat: build packages without make

---
 Lake/Build.lean               | 299 ++++++++++++++++++++--------------
 Lake/Cli.lean                 |  22 +--
 Lake/Compile.lean             |  51 ++++++
 Lake/Make.lean                |  59 -------
 Lake/Package.lean             |  62 +++++--
 Lake/Resolve.lean             |   1 -
 README.md                     |   4 +-
 build-msys2.sh                |   2 +-
 build-unix.sh                 |   2 +-
 examples/hello/package.sh     |   2 +-
 examples/helloDeps/package.sh |   3 +-
 11 files changed, 298 insertions(+), 209 deletions(-)
 create mode 100644 Lake/Compile.lean
 delete mode 100644 Lake/Make.lean

diff --git a/Lake/Build.lean b/Lake/Build.lean
index bad5f9af18..0530e3f382 100644
--- a/Lake/Build.lean
+++ b/Lake/Build.lean
@@ -7,162 +7,217 @@ import Lean.Data.Name
 import Lean.Elab.Import
 import Lake.Resolve
 import Lake.Package
-import Lake.Make
-import Lake.Proc
+import Lake.Compile
 
-open Lean System
+open System
+open Lean hiding SearchPath
 
 namespace Lake
 
-structure BuildConfig where
-  module   : Name
-  leanArgs : List String
-  leanPath : String
-  -- things that should also trigger rebuilds
-  -- ex. olean roots of dependencies
-  moreDeps : List FilePath
+-- # Basic Build Infos
 
-def mkBuildConfig
-(pkg : Package) (deps : List Package) (leanArgs : List String)
-: BuildConfig := {
-  leanArgs,
-  module := pkg.module
-  leanPath := SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
-  moreDeps := deps.map (·.oleanRoot)
-}
-
-structure BuildContext extends BuildConfig where
-  parents       : List Name := []
-  moreDepsMTime : IO.FS.SystemTime
-
-structure BuildResult where
-  maxMTime : IO.FS.SystemTime
-  task     : Task (Except IO.Error Unit)
+structure BuildInfo (α : Type) where
+  artifact  : α
+  maxMTime  : IO.FS.SystemTime
+  task : Task (Except IO.Error PUnit)
   deriving Inhabited
 
-structure BuildState where
-  modTasks : NameMap BuildResult := ∅
+abbrev ModuleBuildInfo := BuildInfo (FilePath × FilePath)
 
-abbrev BuildM := ReaderT BuildContext <| StateT BuildState IO
+namespace ModuleBuildInfo
+def oleanFile (self : ModuleBuildInfo) := self.artifact.1
+def cFile (self : ModuleBuildInfo) := self.artifact.2
+end ModuleBuildInfo
 
-partial def buildModule (mod : Name) : BuildM BuildResult := do
-  let ctx ← read
-
-  -- detect cyclic imports
-  if ctx.parents.contains mod then
-    let cycle := mod :: (ctx.parents.partition (· != mod)).1 ++ [mod]
-    let cycle := cycle.map (s!"  {·}")
-    throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
-
-  -- skip if already visited
-  if let some res := (← get).modTasks.find? mod then
-    return res
-
-  -- deduce lean file
-  let leanFile := modToFilePath "." mod "lean"
-
-  -- parse imports
-  let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
-  let localImports := imports.filter (·.module.getRoot == ctx.module)
-
-  -- recursively build local dependencies
-  let deps ← localImports.mapM fun i =>
-    withReader (fun ctx => { ctx with parents := mod :: ctx.parents }) <|
-      buildModule i.module
-
-  -- calculate transitive `maxMTime`
-  let leanMData ← leanFile.metadata
-  let depMTimes ← deps.mapM (·.maxMTime)
-  let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
-
-  -- check whether we have an up-to-date .olean
-  let oleanFile := modToFilePath buildPath mod "olean"
+def buildOleanAndC  (leanFile oleanFile cFile : FilePath) 
+(depInfos : List ModuleBuildInfo) (maxMTime : IO.FS.SystemTime) 
+(leanPath : String := "") (rootDir : FilePath := ".") (leanArgs : Array String := #[])
+: IO ModuleBuildInfo := do
+  let artifact := (oleanFile, cFile)
+  -- check whether we have an up-to-date .olean and .c
   try
-    if (← oleanFile.metadata).modified >= maxMTime then
-      let res := { maxMTime, task := Task.pure (Except.ok ()) }
-      modify fun st => { st with modTasks := st.modTasks.insert mod res }
-      return res
+    let cMTime := (← cFile.metadata).modified
+    let oleanMTime := (← oleanFile.metadata).modified
+    if cMTime >= maxMTime && oleanMTime >= maxMTime then
+      let task := Task.pure (Except.ok ())
+      return { artifact, maxMTime, task }
   catch
     | IO.Error.noFileOrDirectory .. => pure ()
     | e                             => throw e
-
   -- (try to) compile the olean and c file
-  let task ← IO.mapTasks (tasks := deps.map (·.task)) fun rs => do
-    if let some e := rs.findSome? (fun | Except.error e => some e | Except.ok _ => none) then
-      -- propagate failure from dependencies
-      throw e
+  let task ← IO.mapTasks (tasks := depInfos.map (·.task)) fun rs => do
+    rs.forM IO.ofExcept  -- propagate first failure from dependencies
     try
-      let cFile := modToFilePath tempBuildPath mod "c"
-      IO.FS.createDirAll oleanFile.parent.get!
-      IO.FS.createDirAll cFile.parent.get!
-      execCmd {
-        cmd := "lean"
-        args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString]
-        env := #[("LEAN_PATH", ctx.leanPath)]
-      }
+      compileOleanAndC leanFile oleanFile cFile leanPath rootDir leanArgs
     catch e =>
       -- print compile errors early
       IO.eprintln e
       throw e
+  return { artifact, maxMTime, task }
 
-  let res := { maxMTime, task := task }
-  modify fun st => { st with modTasks := st.modTasks.insert mod res }
-  return res
+def buildO (oFile : FilePath) 
+(cInfo : BuildInfo FilePath) (leancArgs : Array String := #[]) 
+: IO (BuildInfo FilePath) := do
+  -- skip if we have an up-to-date .o
+  try 
+    let cMTime := cInfo.maxMTime
+    if (← oFile.metadata).modified >= cMTime then 
+      return {artifact := oFile, maxMTime := cMTime, task := Task.pure (Except.ok ()) }
+  catch
+    | IO.Error.noFileOrDirectory .. => pure ()
+    | e => throw e
+  -- compile it otherwise
+  let task ← IO.mapTask (t := cInfo.task) fun x => do
+    IO.ofExcept x  -- propagate failure from building .c
+    try
+      compileO oFile cInfo.artifact leancArgs
+    catch e =>
+      -- print compile errors early
+      IO.eprintln e
+      throw e
+  return {artifact := oFile, maxMTime := cInfo.maxMTime, task }
 
-def buildModules (cfg : BuildConfig) (mods : List Name) : IO Unit := do
-  let moreDepsMTime := (← cfg.moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
-  let rs ← mods.mapM buildModule |>.run { toBuildConfig := cfg, moreDepsMTime } |>.run' {}
-  for r in rs do
-    if let Except.error _ ← IO.wait r.task then
-      -- actual error has already been printed above
-      throw <| IO.userError "Build failed."
+-- # Build Modules
 
-def buildImports (pkg : Package) (deps : List Package) (imports leanArgs : List String := []) : IO Unit := do
-  let imports := imports.map (·.toName)
-  let localImports := imports.filter (·.getRoot == pkg.module)
-  if localImports != [] then
-    if ← FilePath.pathExists "Makefile" then
-      let oleans := localImports.map fun i =>
-        Lean.modToFilePath buildPath i "olean" |>.toString
-      execMake pkg deps oleans leanArgs
-    else
-      buildModules (mkBuildConfig pkg deps leanArgs) localImports
+structure BuildContext where
+  package       : Package
+  leanPath      : String
+  -- things that should also trigger rebuilds
+  -- ex. olean roots of dependencies
+  moreDeps      : List FilePath
+  buildParents  : List Name := []
+  moreDepsMTime : IO.FS.SystemTime
 
-def buildPkg (pkg : Package) (deps : List Package) (makeArgs leanArgs : List String := []) : IO Unit := do
-  if makeArgs != [] || (← FilePath.pathExists "Makefile") then
-    execMake pkg deps makeArgs leanArgs
-  else
-    buildModules (mkBuildConfig pkg deps leanArgs) [pkg.module]
+structure BuildState where
+  buildInfos : NameMap ModuleBuildInfo := ∅
 
-def buildDeps (pkg : Package) (makeArgs leanArgs : List String := []) : IO (List Package) := do
+abbrev BuildM := ReaderT BuildContext <| StateT BuildState IO
+
+partial def buildModule (mod : Name) : BuildM ModuleBuildInfo := do
+  let ctx ← read
+  let pkg := ctx.package
+
+  -- detect cyclic imports
+  if ctx.buildParents.contains mod then
+    let cycle := mod :: (ctx.buildParents.partition (· != mod)).1 ++ [mod]
+    let cycle := cycle.map (s!"  {·}")
+    throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
+
+  -- return previous result if already visited
+  if let some info := (← get).buildInfos.find? mod then
+    return info
+
+  -- deduce lean file
+  let leanFile := ctx.package.modToSource mod
+
+  -- parse imports
+  let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
+  let directLocalImports := imports.map (·.module) |>.filter (·.getRoot == pkg.module)
+
+  -- recursively build local dependencies
+  let depInfos ← directLocalImports.mapM fun i =>
+    withReader (fun ctx => { ctx with buildParents := mod :: ctx.buildParents }) <|
+      buildModule i
+
+  -- calculate transitive `maxMTime`
+  let leanMData ← leanFile.metadata
+  let depMTimes ← depInfos.mapM (·.maxMTime)
+  let maxMTime := List.maximum? (leanMData.modified :: ctx.moreDepsMTime :: depMTimes) |>.get!
+
+  -- do build
+  let cFile := pkg.modToC mod
+  let oleanFile := pkg.modToOlean mod
+  let info ← buildOleanAndC leanFile oleanFile cFile 
+    depInfos maxMTime ctx.leanPath pkg.dir pkg.leanArgs
+  modify fun st => { st with buildInfos := st.buildInfos.insert mod info }
+  return info
+
+def mkBuildContext (pkg : Package) (deps : List Package) : IO BuildContext := do
+  let moreDeps := deps.map (·.oleanRoot)
+  let moreDepsMTime := (← moreDeps.mapM (·.metadata)).map (·.modified) |>.maximum? |>.getD ⟨0, 0⟩
+  let leanPath := SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
+  return { package := pkg, leanPath, moreDeps, moreDepsMTime }
+
+def buildPackageModulesCore 
+(pkg : Package) (deps : List Package) : IO (ModuleBuildInfo × BuildState) := do
+  let crx ← mkBuildContext pkg deps
+  buildModule pkg.module |>.run crx |>.run {}
+
+def buildPackageModuleDAG 
+(pkg : Package) (deps : List Package) : IO (NameMap ModuleBuildInfo) := do
+  (← buildPackageModulesCore pkg deps).2.buildInfos
+
+-- # Configure/Build Packages
+
+def buildPackageModules 
+(pkg : Package) (deps : List Package) : IO PUnit := do
+  let (info, _) ← buildPackageModulesCore pkg deps
+  if let Except.error _ ← IO.wait info.task then
+    -- actual error has already been printed above
+    throw <| IO.userError "Build failed."
+
+def buildDeps (pkg : Package) : IO (List Package) := do
   let deps ← solveDeps pkg
   for dep in deps do
     -- build recursively
     -- TODO: share build of common dependencies
     let depDeps ← solveDeps dep
-    buildPkg dep depDeps makeArgs leanArgs
+    buildPackageModules pkg deps
   return deps
 
-def configure (pkg : Package) : IO Unit :=
+def configure (pkg : Package) : IO Unit := do
   discard <| buildDeps pkg
 
-def printPaths (pkg : Package) (imports leanArgs : List String := []) : IO Unit := do
+def build (pkg : Package) : IO Unit := do
   let deps ← buildDeps pkg
-  buildImports pkg deps imports leanArgs
+  buildPackageModules pkg deps
+
+-- # Build Package Lib/Bin
+
+def buildPackageOFiles (pkg : Package) (buildMap : NameMap ModuleBuildInfo)
+: IO (List FilePath) := do 
+  let oInfos ← buildMap.toList.mapM fun (mod, info) => 
+    let oFile := pkg.modToO mod
+    buildO oFile {info with artifact := info.cFile} pkg.leancArgs
+  oInfos.mapM fun info => do
+    IO.ofExcept (← IO.wait info.task)
+    info.artifact
+
+def buildStaticLib (pkg : Package) : IO FilePath := do
+  let deps ← buildDeps pkg
+  let buildMap ← buildPackageModuleDAG pkg deps
+  let oFiles ← buildPackageOFiles pkg buildMap
+  compileLib pkg.staticLibFile oFiles.toArray
+  pkg.staticLibFile
+
+def buildBin (pkg : Package) : IO FilePath := do
+  let deps ← solveDeps pkg
+  let depLibs ← deps.mapM buildStaticLib
+  let buildMap ← buildPackageModuleDAG pkg deps
+  let oFiles ← buildPackageOFiles pkg buildMap
+  compileBin pkg.binFile (oFiles ++ depLibs).toArray pkg.linkArgs
+  pkg.binFile
+
+-- # Print Paths
+
+def buildModulesInPackage (pkg : Package) (deps : List Package) (mods : List Name) : IO Unit := do
+  let ctx ← mkBuildContext pkg deps
+  let rs ← mods.mapM buildModule |>.run ctx |>.run' {}
+  for r in rs do
+    if let Except.error _ ← IO.wait r.task then
+      -- actual error has already been printed above
+      throw <| IO.userError "Build failed."
+
+def buildImports 
+(pkg : Package) (deps : List Package) (imports : List String := []) 
+: IO Unit := do
+  let imports := imports.map (·.toName)
+  let localImports := imports.filter (·.getRoot == pkg.module)
+  buildModulesInPackage pkg deps localImports
+
+def printPaths (pkg : Package) (imports : List String := []) : IO Unit := do
+  let deps ← buildDeps pkg
+  buildImports pkg deps imports
   IO.println <| SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
   IO.println <| SearchPath.toString <| pkg.sourceDir :: deps.map (·.sourceDir)
 
-private def relPathToUnixString (path : FilePath) : String :=
-  if Platform.isWindows then
-    path.toString.map fun c => if c == '\\' then '/' else c
-  else
-    path.toString
-
-def build (pkg : Package) (makeArgs leanArgs : List String := []) : IO Unit := do
-  if makeArgs.contains "bin" then
-    let deps ← buildDeps pkg ["lib"]
-    let depLibs := " ".intercalate <| deps.map (relPathToUnixString ·.staticLibPath)
-    buildPkg pkg deps (s!"LINK_OPTS=\"{depLibs}\"" :: makeArgs) leanArgs
-  else
-    let deps ← buildDeps pkg
-    buildPkg pkg deps makeArgs leanArgs
diff --git a/Lake/Cli.lean b/Lake/Cli.lean
index aa3f558679..3daddd06db 100644
--- a/Lake/Cli.lean
+++ b/Lake/Cli.lean
@@ -68,16 +68,18 @@ def getRootPkg : IO Package := do
       leanVersionString ++ ", but package requires " ++ cfg.leanVersion ++ "\n"
   return ⟨".", cfg⟩
 
-def cli : (cmd : String) → (lakeArgs leanArgs : List String) → IO Unit
-| "init",         [name],         []        => init name
-| "configure",    [],             []        => do configure (← getRootPkg)
-| "print-paths",  imports,        leanArgs  => do printPaths (← getRootPkg) imports leanArgs
-| "build",        makeArgs,       leanArgs  => do build (← getRootPkg) makeArgs leanArgs
-| "help",         ["init"],       []        => IO.println helpInit
-| "help",         ["configure"],  []        => IO.println helpConfigure
-| "help",         ["build"],      []        => IO.println helpBuild
-| "help",         _,              []        => IO.println usage
-| _,              _,              _         => throw <| IO.userError usage
+def cli : (cmd : String) → (lakeArgs pkgArgs : List String) → IO Unit
+| "init",         [name],         []  => init name
+| "configure",    [],             []  => do configure (← getRootPkg)
+| "print-paths",  imports,        []  => do printPaths (← getRootPkg) imports
+| "build",        [],             []  => do build (← getRootPkg)
+| "build-bin",    [],             []  => do discard <| buildBin (← getRootPkg) 
+| "build-lib",    [],             []  => do discard <| buildStaticLib (← getRootPkg)
+| "help",         ["init"],       []  => IO.println helpInit
+| "help",         ["configure"],  []  => IO.println helpConfigure
+| "help",         ["build"],      []  => IO.println helpBuild
+| "help",         _,              []  => IO.println usage
+| _,              _,              _   => throw <| IO.userError usage
 
 private def splitCmdlineArgsCore : List String → List String × List String
 | [] => ([], [])
diff --git a/Lake/Compile.lean b/Lake/Compile.lean
new file mode 100644
index 0000000000..5e7014e2ff
--- /dev/null
+++ b/Lake/Compile.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2021 Mac Malone. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mac Malone
+-/
+import Lake.Proc
+
+namespace Lake
+open System
+
+def compileOleanAndC
+(leanFile oleanFile cFile : FilePath) 
+(leanPath : String := "") (rootDir : FilePath := ".") (leanArgs : Array String := #[])
+: IO Unit := do
+  if let some dir := cFile.parent then IO.FS.createDirAll dir
+  if let some dir := oleanFile.parent then IO.FS.createDirAll dir
+  execCmd {
+    cmd := "lean"
+    args := leanArgs ++ #[
+      "-R", rootDir.toString, "-o", oleanFile.toString, "-c",  
+      cFile.toString, leanFile.toString
+    ]
+    env := #[("LEAN_PATH", leanPath)]
+  }
+
+def compileO
+(oFile cFile : FilePath) (leancArgs : Array String := #[])
+: IO Unit := do
+  if let some dir := oFile.parent then IO.FS.createDirAll dir
+  execCmd {
+    cmd := "leanc"
+    args := #["-c", "-o", oFile.toString, cFile.toString] ++ leancArgs
+  }
+
+def compileBin
+(binFile : FilePath) (oFiles : Array FilePath) (linkArgs : Array String := #[])
+: IO Unit := do
+  if let some dir := binFile.parent then IO.FS.createDirAll dir
+  execCmd {
+    cmd := "leanc"
+    args := #["-o", binFile.toString] ++ oFiles.map toString ++ linkArgs
+  }
+
+def compileLib
+(libFile : FilePath) (oFiles : Array FilePath)
+: IO Unit := do
+  if let some dir := libFile.parent then IO.FS.createDirAll dir
+  execCmd {
+    cmd := "ar"
+    args := #["rcs", libFile.toString] ++ oFiles.map toString
+  }
diff --git a/Lake/Make.lean b/Lake/Make.lean
deleted file mode 100644
index 5a542fe091..0000000000
--- a/Lake/Make.lean
+++ /dev/null
@@ -1,59 +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, Mac Malone
--/
-import Lake.Proc
-import Lake.Package
-
-open System
-
-namespace Lake
-
-def lockfile : FilePath := buildPath / ".lake-lock"
-
-partial def withLockFile (x : IO α) : IO α := do
-  acquire
-  try
-    x
-  finally
-    IO.FS.removeFile lockfile
-  where
-    acquire (firstTime := true) := do
-      IO.FS.createDirAll lockfile.parent.get!
-      try
-        -- TODO: lock file should ideally contain PID
-        if !Platform.isWindows then
-          discard <| IO.FS.Handle.mkPrim lockfile "wx"
-        else
-          -- `x` mode doesn't seem to work on Windows even though it's listed at
-          -- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160
-          -- ...? Let's use the slightly racy approach then.
-          if ← lockfile.pathExists then
-            throw <| IO.Error.alreadyExists 0 ""
-          discard <| IO.FS.Handle.mk lockfile IO.FS.Mode.write
-      catch
-        | IO.Error.alreadyExists _ _ => do
-          if firstTime then
-            IO.eprintln s!"Waiting for prior lake invocation to finish... (remove '{lockfile}' if stuck)"
-          IO.sleep (ms := 300)
-          acquire (firstTime := false)
-        | e => throw e
-
-def execMake
-(pkg : Package) (deps : List Package) (makeArgs leanArgs : List String := [])
-: IO Unit := withLockFile do
-  let timeoutArgs :=
-    match pkg.timeout with
-    | some t => ["-T", toString t]
-    | none => []
-  let leanOptsStr := " ".intercalate <| timeoutArgs ++ leanArgs
-  let leanPathStr := SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
-  let makeArgsStr := " ".intercalate makeArgs
-  let moreDepsStr := " ".intercalate <| deps.map (·.oleanRoot.toString)
-  let mut spawnArgs := {
-    cmd := "sh"
-    cwd := pkg.dir
-    args := #["-c", s!"leanmake PKG={pkg.module} LEAN_OPTS=\"{leanOptsStr}\" LEAN_PATH=\"{leanPathStr}\" {makeArgsStr} MORE_DEPS+=\"{moreDepsStr}\" >&2"]
-  }
-  execCmd spawnArgs
diff --git a/Lake/Package.lean b/Lake/Package.lean
index ac1fe046e5..3c37090375 100644
--- a/Lake/Package.lean
+++ b/Lake/Package.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
 -/
 import Lean.Data.Name
+import Lean.Elab.Import
 import Lake.LeanVersion
 
 open Lean System
@@ -26,6 +27,9 @@ structure PackageConfig where
   name : String
   version : String
   leanVersion : String := leanVersionString
+  leanArgs : Array String := #[]
+  leancArgs : Array String := #[]
+  linkArgs : Array String := #[]
   timeout : Option Nat := none
   module : Name := name.capitalize
   dependencies : List Dependency := []
@@ -50,6 +54,15 @@ def moduleName (self : Package) :=
 def dependencies (self : Package) :=
   self.config.dependencies
 
+def leanArgs (self : Package) :=
+  self.config.leanArgs
+
+def leancArgs (self : Package) :=
+  self.config.leancArgs
+
+def linkArgs (self : Package) :=
+  self.config.linkArgs
+
 def timeout (self : Package) :=
   self.config.timeout
 
@@ -59,29 +72,56 @@ def sourceDir (self : Package) :=
 def sourceRoot (self : Package) :=
   self.sourceDir / self.moduleName
 
+def modToSource (mod : Name) (self : Package) :=
+  Lean.modToFilePath self.sourceDir mod "lean"
+
 def buildDir (self : Package) :=
   self.dir / Lake.buildPath
 
+def oleanDir (self : Package) :=
+  self.buildDir
+
+def oleanRoot (self : Package) :=
+  self.oleanDir / FilePath.withExtension self.moduleName "olean"
+
+def modToOlean (mod : Name) (self : Package) :=
+  Lean.modToFilePath self.oleanDir mod "olean"
+
+def tempBuildDir (self : Package) :=
+  self.dir / tempBuildPath
+
+def cDir (self : Package) :=
+  self.tempBuildDir
+
+def modToC (mod : Name) (self : Package) :=
+  Lean.modToFilePath self.cDir mod "c"
+
+def oDir (self : Package) :=
+  self.tempBuildDir
+
+def modToO (mod : Name) (self : Package) :=
+  Lean.modToFilePath self.oDir mod "o"
+
 def binDir (self : Package) :=
   self.buildDir / "bin"
 
 def binName (self : Package) :=
   self.moduleName
 
-def binPath (self : Package) :=
-  self.binDir / FilePath.withExtension self.binName FilePath.exeExtension
+def binFileName (self : Package) : FilePath :=
+  FilePath.withExtension self.binName FilePath.exeExtension
+
+def binFile (self : Package) :=
+  self.binDir / self.binFileName
 
 def libDir (self : Package) :=
   self.buildDir / "lib"
 
-def staticLibFile (self : Package) :=
+def staticLibName (self : Package) :=
+  self.moduleName
+
+def staticLibFileName (self : Package) :=
   s!"lib{self.module}.a"
 
-def staticLibPath (self : Package) :=
-  self.libDir / self.staticLibFile
-
-def oleanDir (self : Package) :=
-  self.dir / Lake.buildPath
-
-def oleanRoot (self : Package) :=
-  self.oleanDir / FilePath.withExtension self.moduleName "olean"
+def staticLibFile (self : Package) :=
+  self.libDir / self.staticLibFileName
diff --git a/Lake/Resolve.lean b/Lake/Resolve.lean
index 85a6d02dd9..95211eb027 100644
--- a/Lake/Resolve.lean
+++ b/Lake/Resolve.lean
@@ -30,7 +30,6 @@ def materialize (pkgDir : FilePath) (dep : Dependency) : IO FilePath :=
   match dep.src with
   | Source.path dir => do
     let depdir := pkgDir / dir
-    IO.eprintln s!"{dep.name}: using local path {depdir}"
     depdir
   | Source.git url rev branch => do
     let depdir := pkgDir / depsPath / dep.name
diff --git a/README.md b/README.md
index 3972fba499..15f70b5c6f 100644
--- a/README.md
+++ b/README.md
@@ -58,10 +58,10 @@ def package : Lake.PackageConfig := {
 }
 ```
 
-We can use the command `lake build bin` to build the module (and its dependencies, if it has them) and a native executable. The latter of which will be written to `build/bin`.
+We can use the command `lake build-bin` to build the package (and its dependencies, if it has them) into a native executable. The result will be placed in to `build/bin`.
 
 ```
-$ lake build bin
+$ lake build-bin
 ...
 $ ./build/bin/Hello
 Hello, world!
diff --git a/build-msys2.sh b/build-msys2.sh
index 99ef39c4bb..06c3e42b7a 100644
--- a/build-msys2.sh
+++ b/build-msys2.sh
@@ -1 +1 @@
-leanpkg build bin LINK_OPTS=-Wl,--export-all
+leanpkg build bin LINK_OPTS=-Wl,--export-all "$@"
diff --git a/build-unix.sh b/build-unix.sh
index b1f67e21cc..1d82876db7 100644
--- a/build-unix.sh
+++ b/build-unix.sh
@@ -1 +1 @@
-leanpkg build bin LINK_OPTS=-rdynamic
+leanpkg build bin LINK_OPTS=-rdynamic "$@"
diff --git a/examples/hello/package.sh b/examples/hello/package.sh
index dfeb2433bc..b6449c2dd0 100644
--- a/examples/hello/package.sh
+++ b/examples/hello/package.sh
@@ -1 +1 @@
-../../build/bin/Lake build bin
+../../build/bin/Lake build-bin
diff --git a/examples/helloDeps/package.sh b/examples/helloDeps/package.sh
index 285426058b..4a895847e5 100644
--- a/examples/helloDeps/package.sh
+++ b/examples/helloDeps/package.sh
@@ -1,2 +1,3 @@
 cd foo
-../../../build/bin/Lake build bin
+echo "in directory 'foo'"
+../../../build/bin/Lake build-bin