feat: basic precompiled modules + builtin module facets

closes leanprover#47

Lake/Build/Actions.lean

@@ -34,7 +34,8 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
 def compileLeanModule (leanFile : FilePath)
 (oleanFile? ileanFile? cFile? : Option FilePath)
 (oleanPath : SearchPath := []) (rootDir : FilePath := ".")
-(leanArgs : Array String := #[]) (lean : FilePath := "lean")
+(dynlibs : Array FilePath := #[]) (leanArgs : Array String := #[])
+(lean : FilePath := "lean")
 : BuildM PUnit := do
   let mut args := leanArgs ++
     #[leanFile.toString, "-R", rootDir.toString]
@@ -47,8 +48,10 @@ def compileLeanModule (leanFile : FilePath)
   if let some cFile := cFile? then
     createParentDirs cFile
     args := args ++ #["-c", cFile.toString]
+  for dynlib in dynlibs do
+    args := args.push s!"--load-dynlib={dynlib}"
   proc {
-    args,
+    args
     cmd := lean.toString
     env := #[("LEAN_PATH", oleanPath.toString)]
   }

Lake/Build/Binary.lean

@@ -6,70 +6,51 @@ Authors: Mac Malone
 import Lake.Build.Package
 import Lake.Build.Targets
 
-open System
+open Std System
 open Lean (Name NameMap)
 
 namespace Lake
 
--- # Build Package .o Files
-
-def Package.oFileTargetsOf
-(targetMap : ModuleMap ActiveOpaqueTarget) (self : Package) : Array FileTarget :=
-  targetMap.fold (fun arr k v => arr.push (k, v)) #[] |>.filterMap fun (key, target) =>
-    if key.facet == `lean.c && self.isLocalModule key.module then
-      let mod : Module := ⟨self, key.module⟩
-      let target := Target.active <| target.withInfo mod.cFile
-      leanOFileTarget mod.oFile target self.moreLeancArgs
-    else
-      none
-
-def Module.mkOTarget (modTarget : OpaqueTarget) (self : Module) : FileTarget :=
-  leanOFileTarget self.oFile (self.mkCTarget modTarget) self.leancArgs
-
-def Module.oTarget (self : Module) : FileTarget :=
-  self.mkOTarget <| self.leanBinTarget (c := true)
-
 -- # Build Package Static Lib
 
-def Package.mkStaticLibTarget (self : Package) (lib : LeanLibConfig) : FileTarget :=
+def Package.localTargetsOf (map : NameMap (ActiveBuildTarget α)) (self : Package) : Array (BuildTarget α) :=
+  map.fold (fun a n v => if self.isLocalModule n then a.push (Target.active v) else a) #[]
+
+def Package.mkStaticLibTarget (lib : LeanLibConfig) (self : Package) : FileTarget :=
   let libFile := self.libDir / lib.staticLibFileName
   BuildTarget.mk' libFile do
-    let depTarget ← self.buildExtraDepsTarget
-    let mods ← self.getLibModuleArray lib
-    let moduleTargetMap ← buildModuleMap mods $
-      recBuildModuleTargetWithDeps depTarget (c := true)
-    let oFileTargets := self.oFileTargetsOf moduleTargetMap
-    staticLibTarget libFile oFileTargets |>.materializeAsync
+    withExtraDepTarget (← self.buildExtraDepsTarget) do
+      let mods ← self.getLibModuleArray lib
+      let oFileTargets := self.localTargetsOf <| ← buildModuleMap mods &`lean.o
+      staticLibTarget libFile oFileTargets |>.materializeAsync
 
 protected def Package.staticLibTarget (self : Package) : FileTarget :=
   self.mkStaticLibTarget self.builtinLibConfig
 
 -- # Build Package Shared Lib
 
 def Package.linkTargetsOf
-(targetMap : ModuleMap ActiveOpaqueTarget) (self : Package) : LakeM (Array FileTarget) := do
+(targetMap : NameMap ActiveFileTarget) (self : Package) : LakeM (Array FileTarget) := do
   let collect dep recurse := do
-      let pkg := (← findPackage? dep.name).get!
-      pkg.dependencies.forM fun dep => discard <| recurse dep
-      return pkg.oFileTargetsOf targetMap ++ pkg.externLibTargets
-  let ⟨x, map⟩ ← RBTopT.run (cmp := Name.quickCmp) <| self.dependencies.forM fun dep =>
-    discard <| buildTop collect Dependency.name dep
+    let pkg := (← findPackage? dep.name).get!
+    pkg.dependencies.forM fun dep => discard <| recurse dep
+    return pkg.localTargetsOf targetMap ++ pkg.externLibTargets
+  let ⟨x, map⟩ ← EStateT.run (mkRBMap _ _ Name.quickCmp) <|
+    self.dependencies.forM fun dep => discard <| buildTop Dependency.name collect dep
   match x with
   | Except.ok _ =>
     let ts := map.fold (fun acc _ vs => acc ++ vs) #[]
-    return self.oFileTargetsOf targetMap ++ self.externLibTargets ++ ts
+    return self.localTargetsOf targetMap ++ self.externLibTargets ++ ts
   | Except.error _ => panic! "dependency cycle emerged after resolution"
 
 def Package.mkSharedLibTarget (self : Package) (lib : LeanLibConfig) : FileTarget :=
   let libFile := self.libDir / lib.sharedLibFileName
   BuildTarget.mk' libFile do
-    let depTarget ← self.buildExtraDepsTarget
-    let mods ← self.getLibModuleArray lib
-    let moduleTargetMap ← buildModuleMap mods $
-      recBuildModuleTargetWithDeps depTarget (c := true)
-    let linkTargets ← self.linkTargetsOf moduleTargetMap
-    let target := leanSharedLibTarget libFile linkTargets lib.linkArgs
-    target.materializeAsync
+    withExtraDepTarget (← self.buildExtraDepsTarget) do
+      let mods ← self.getLibModuleArray lib
+      let linkTargets ← self.linkTargetsOf <| ← buildModuleMap mods &`lean.o
+      let target := leanSharedLibTarget libFile linkTargets lib.linkArgs
+      target.materializeAsync
 
 protected def Package.sharedLibTarget (self : Package) : FileTarget :=
   self.mkSharedLibTarget self.builtinLibConfig
@@ -79,20 +60,19 @@ protected def Package.sharedLibTarget (self : Package) : FileTarget :=
 def Package.mkExeTarget (self : Package) (exe : LeanExeConfig) : FileTarget :=
   let exeFile := self.binDir / exe.fileName
   BuildTarget.mk' exeFile do
-    let root : Module := ⟨self, exe.root⟩
-    let depTarget ← self.buildExtraDepsTarget
-    let moduleTargetMap ← buildModuleMap #[root] $
-      recBuildModuleTargetWithDeps depTarget (c := true)
-    let pkgLinkTargets ← self.linkTargetsOf moduleTargetMap
-    let linkTargets :=
-      if self.isLocalModule exe.root then
-        pkgLinkTargets
-      else
-        let rootTarget := moduleTargetMap.find? (root.key `lean) |>.get!
-        let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
-        #[rootLinkTarget] ++ pkgLinkTargets
-    let target := leanExeTarget exeFile linkTargets exe.linkArgs
-    target.materializeAsync
+    let root : Module := ⟨self, WfName.ofName exe.root⟩
+    withExtraDepTarget (← self.buildExtraDepsTarget) do
+      let cTargetMap ← buildModuleMap #[root] &`lean.c
+      let pkgLinkTargets ← self.linkTargetsOf cTargetMap
+      let linkTargets :=
+        if self.isLocalModule exe.root then
+          pkgLinkTargets
+        else
+          let rootTarget := cTargetMap.find? root.name |>.get!
+          let rootLinkTarget := root.mkOTarget <| Target.active rootTarget
+          #[rootLinkTarget] ++ pkgLinkTargets
+      let target := leanExeTarget exeFile linkTargets exe.linkArgs
+      target.materializeAsync
 
 protected def Package.exeTarget (self : Package) : FileTarget :=
   self.mkExeTarget self.builtinExeConfig

Lake/Build/Context.lean

@@ -13,9 +13,16 @@ import Lake.Build.Trace
 open System
 namespace Lake
 
+/-- The `Task` monad for Lake builds. -/
+abbrev BuildTask := OptionIOTask
+
+/-- A Lake build job. -/
+abbrev Job := BuildTask BuildTrace
+
 /-- A Lake context with some additional caching for builds. -/
 structure BuildContext extends Context where
   leanTrace : BuildTrace
+  extraDepJob : Job := pure nilTrace
 
 /-- A transformer to equip a monad with a `BuildContext`. -/
 abbrev BuildT := ReaderT BuildContext
@@ -26,12 +33,6 @@ abbrev SchedulerM := BuildT <| LogT BaseIO
 /-- The monad for Lake builds. -/
 abbrev BuildM := BuildT <| MonadLogT BaseIO OptionIO
 
-/-- The `Task` monad for Lake builds. -/
-abbrev BuildTask := OptionIOTask
-
-/-- A Lake build job. -/
-abbrev Job := BuildTask BuildTrace
-
 instance : MonadError BuildM := ⟨MonadLog.error⟩
 instance : MonadLift IO BuildM := ⟨MonadError.runIO⟩