feat: leanpkg build without external dependencies

src/Init/Core.lean

@@ -114,6 +114,7 @@ notation "∅"     => EmptyCollection.emptyCollection
 /- Remark: tasks have an efficient implementation in the runtime. -/
 structure Task (α : Type u) : Type u where
   pure :: (get : α)
+  deriving Inhabited
 
 attribute [extern "lean_task_pure"] Task.pure
 attribute [extern "lean_task_get_own"] Task.get

src/Init/System/IO.lean

@@ -111,6 +111,14 @@ constant mapTask (f : α → IO β) (t : Task α) (prio := Task.Priority.default
 @[extern "lean_io_bind_task"]
 constant bindTask (t : Task α) (f : α → IO (Task (Except IO.Error β))) (prio := Task.Priority.default) : IO (Task (Except IO.Error β))
 
+def mapTasks (f : List α → IO β) (tasks : List (Task α)) (prio := Task.Priority.default) : IO (Task (Except IO.Error β)) :=
+  go tasks []
+where
+  go
+    | t::ts, as =>
+      IO.bindTask t (fun a => go ts (a :: as)) prio
+    | [], as => IO.asTask (f as.reverse) prio
+
 /-- Check if the task's cancellation flag has been set by calling `IO.cancel` or dropping the last reference to the task. -/
 @[extern "lean_io_check_canceled"] constant checkCanceled : IO Bool
 
@@ -283,7 +291,7 @@ inductive FileType where
 structure SystemTime where
   sec  : Int
   nsec : UInt32
-  deriving Repr, BEq, Ord
+  deriving Repr, BEq, Ord, Inhabited
 
 structure Metadata where
   --permissions : ...

src/Lean/Util/Path.lean

@@ -16,11 +16,13 @@ open System
 def realPathNormalized (p : FilePath) : IO FilePath := do
   (← IO.realPath p).normalize
 
-variable (base : FilePath) in
-def modPathToFilePath : Name → FilePath
-  | Name.str p h _              => modPathToFilePath p / h
-  | Name.anonymous              => base
-  | Name.num p _ _              => panic! "ill-formed import"
+def modToFilePath (base : FilePath) (mod : Name) (ext : String) : FilePath :=
+  go mod |>.withExtension ext
+where
+  go : Name → FilePath
+  | Name.str p h _ => go p / h
+  | Name.anonymous => base
+  | Name.num p _ _ => panic! "ill-formed import"
 
 /-- A `.olean' search path. -/
 abbrev SearchPath := System.SearchPath
@@ -33,7 +35,7 @@ def findWithExt (sp : SearchPath) (ext : String) (mod : Name) : IO (Option FileP
   let pkg := mod.getRoot.toString
   let root? ← sp.findM? fun p =>
     (p / pkg).isDir <||> ((p / pkg).withExtension ext).pathExists
-  return root?.map (modPathToFilePath · mod |>.withExtension ext)
+  return root?.map (modToFilePath · mod ext)
 
 end SearchPath
 

src/Leanpkg.lean

@@ -5,6 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich
 -/
 import Leanpkg.Resolve
 import Leanpkg.Git
+import Leanpkg.Build
 
 open System
 
@@ -68,7 +69,7 @@ def configure : IO Configuration := do
         args := #["build"]
       }
   return {
-    leanPath    := SearchPath.toString <| paths.map (fun (p : FilePath) => p / "build")
+    leanPath    := SearchPath.toString <| paths.map (· / Build.buildPath)
     leanSrcPath := SearchPath.toString paths
   }
 
@@ -98,13 +99,21 @@ def buildImports (imports : List String) (leanArgs : List String) : IO Unit := d
   let root ← getRootPart
   let localImports := imports.filter (·.getRoot == root)
   if localImports != [] then
-    let oleans := localImports.map fun i => Lean.modPathToFilePath ⟨"build"⟩ i |>.withExtension "olean" |>.toString
-    execMake oleans leanArgs cfg.leanPath
+    if ← FilePath.pathExists "Makefile" then
+      let oleans := localImports.map fun i => Lean.modToFilePath "build" i "olean" |>.toString
+      execMake oleans leanArgs cfg.leanPath
+    else
+      Build.buildModules root localImports leanArgs cfg.leanPath
   IO.println cfg.leanPath
   IO.println cfg.leanSrcPath
 
 def build (makeArgs leanArgs : List String) : IO Unit := do
-  execMake makeArgs leanArgs (← configure).leanPath
+  let cfg ← configure
+  let root ← getRootPart
+  if makeArgs != [] || (← FilePath.pathExists "Makefile") then
+    execMake (s!"PKG={root}" :: makeArgs) leanArgs cfg.leanPath
+  else
+    Build.buildModules root [root] leanArgs cfg.leanPath
 
 def initGitignoreContents :=
   "/build

src/Leanpkg/Build.lean

@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Sebastian Ullrich
+-/
+import Lean.Data.Name
+import Lean.Elab.Import
+import Leanpkg.Proc
+
+open Lean
+open System
+
+namespace Leanpkg.Build
+
+def buildPath : FilePath := "build"
+def tempBuildPath := buildPath / "temp"
+
+structure Context where
+  pkg      : Name
+  leanArgs : List String
+  leanPath : String
+  parents  : List Name := []
+
+structure Result where
+  maxMTime : IO.FS.SystemTime
+  task     : Task (Except IO.Error Unit)
+  deriving Inhabited
+
+structure State where
+  modTasks : NameMap Result := ∅
+
+abbrev BuildM := ReaderT Context <| StateT State IO
+
+partial def buildModule (mod : Name) : BuildM Result := do
+  let ctx ← read
+  if ctx.parents.contains mod then
+    -- cyclic import
+    let cycle := ctx.parents.dropWhile (· != mod) ++ [mod]
+    let cycle := cycle.reverse.map (s!"  {·}")
+    throw <| IO.userError s!"import cycle detected:\n{"\n".intercalate cycle}"
+
+  if let some r := (← get).modTasks.find? mod then
+    -- already visited
+    return r
+
+  let leanFile := modToFilePath "." mod "lean"
+  let leanMData ← leanFile.metadata
+
+  -- recursively build dependencies and calculate transitive `maxMTime`
+  let (imports, _, _) ← Elab.parseImports (← IO.FS.readFile leanFile) leanFile.toString
+  let mut deps := #[]
+  let mut maxMTime := leanMData.modified
+  for i in imports do
+    if i.module.getRoot == ctx.pkg then
+      let dep ← withReader (fun ctx => { ctx with parents := mod :: ctx.parents }) do
+        buildModule i.module
+      if dep.maxMTime > maxMTime then
+        maxMTime := dep.maxMTime
+      deps := deps.push dep
+
+  -- check whether we have an up-to-date .olean
+  let oleanFile := modToFilePath buildPath mod "olean"
+  try
+    if (← oleanFile.metadata).modified >= maxMTime then
+      let r := { maxMTime, task := Task.pure (Except.ok ()) }
+      modify fun st => { st with modTasks := st.modTasks.insert mod r }
+      return r
+  catch
+    | IO.Error.noFileOrDirectory .. => pure ()
+    | e                             => throw e
+
+  let task ← IO.mapTasks (tasks := deps.map (·.task) |>.toList) fun rs => do
+    if let some e := rs.findSome? (fun | Except.error e => some e | Except.ok _ => none) then
+      -- propagate failure
+      throw e
+    try
+      let cFile := modToFilePath tempBuildPath mod "c"
+      IO.createDirAll oleanFile.parent.get!
+      IO.createDirAll cFile.parent.get!
+      execCmd {
+        cmd := (← IO.appDir) / "lean" |>.withExtension FilePath.exeExtension |>.toString
+        args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString]
+        env := #[("LEAN_PATH", ctx.leanPath)]
+      }
+    catch e =>
+      -- print errors early
+      IO.eprintln e
+      throw e
+
+  let r := { maxMTime, task := task }
+  modify fun st => { st with modTasks := st.modTasks.insert mod r }
+  return r
+
+def buildModules (pkg : Name) (mods : List Name) (leanArgs : List String) (leanPath : String) : IO Unit := do
+  let rs ← mods.mapM buildModule |>.run { pkg, leanArgs, leanPath } |>.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."
+
+end Leanpkg.Build

tests/leanpkg/b/B.lean

@@ -1,5 +1,6 @@
 import A
-import B.Foo
+import B.Bar
+import B.Baz
 
 def main : IO Unit :=
   IO.println s!"Hello, {foo} {name}!"

tests/leanpkg/b/B/Bar.lean

@@ -0,0 +1,3 @@
+import B.Foo
+
+def bar := "bar"

tests/leanpkg/b/B/Baz.lean

@@ -0,0 +1,3 @@
+import B.Foo
+
+def baz := "baz"