max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: purify BuildModule somewhat + associated cleanup

Browse source
This commit is contained in:
tydeu 2021-09-05 18:05:45 -04:00
parent 6863bb8095
commit 8601c0fe78
5 changed files with 118 additions and 98 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake.lean
View file

@ -5,8 +5,6 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
-/
import Lake.Cli
import Lake.SearchPath
-- API file not imported elsewhere; imported here to force build
import Lake.BuildTargets
def main (args : List String) : IO UInt32 := do
try

2
Lake/BuildBin.lean
View file

@ -49,7 +49,7 @@ protected def ActivePackageTarget.binTarget
def Package.binTarget (self : Package) : FileTarget :=
Target.mk self.binFile do
let depTargets ← self.buildDepTargets
let pkgTarget ← self.buildTargetWithDepTargets depTargets
let pkgTarget ← self.buildOleanAndCTargetsWithDepTargets depTargets
pkgTarget.binTarget depTargets >>= (·.materializeAsync)
def buildBin (pkg : Package) : IO PUnit :=

125
Lake/BuildModule.lean
View file

@ -18,40 +18,38 @@ namespace Lake
-- # Targets
abbrev OleanTarget := ActiveFileTarget
structure ModuleTargetInfo where
structure OleanAndC where
oleanFile : FilePath
cFile : FilePath
deriving Inhabited
namespace ModuleArtifact
namespace OleanAndC
protected def getMTime (self : ModuleTargetInfo) : IO MTime := do
protected def getMTime (self : OleanAndC) : IO MTime := do
return mixTrace (← getMTime self.oleanFile) (← getMTime self.cFile)
instance : GetMTime ModuleTargetInfo := ⟨ModuleArtifact.getMTime⟩
instance : GetMTime OleanAndC := ⟨OleanAndC.getMTime⟩
protected def computeHash (self : ModuleTargetInfo) : IO Hash := do
protected def computeHash (self : OleanAndC) : IO Hash := do
return mixTrace (← computeHash self.oleanFile) (← computeHash self.cFile)
instance : ComputeHash ModuleTargetInfo := ⟨ModuleArtifact.computeHash⟩
instance : ComputeHash OleanAndC := ⟨OleanAndC.computeHash⟩
end ModuleArtifact
end OleanAndC
abbrev ActiveModuleTarget := ActiveBuildTarget ModuleTargetInfo
abbrev ActiveOleanAndCTarget := ActiveBuildTarget OleanAndC
namespace ActiveModuleTarget
namespace ActiveOleanAndCTarget
def oleanFile (self : ActiveModuleTarget) := self.info.oleanFile
def oleanTarget (self : ActiveModuleTarget) : ActiveFileTarget :=
def oleanFile (self : ActiveOleanAndCTarget) := self.info.oleanFile
def oleanTarget (self : ActiveOleanAndCTarget) : ActiveFileTarget :=
self.withInfo self.oleanFile
def cFile (self : ActiveModuleTarget) := self.info.cFile
def cTarget (self : ActiveModuleTarget) : ActiveFileTarget :=
def cFile (self : ActiveOleanAndCTarget) := self.info.cFile
def cTarget (self : ActiveOleanAndCTarget) : ActiveFileTarget :=
self.withInfo self.cFile
end ActiveModuleTarget
end ActiveOleanAndCTarget
-- # Trace Checking
@ -72,38 +70,51 @@ def checkModuleTrace [GetMTime i] (info : i)
-- # Module Builders
def mkModuleTarget [GetMTime i] [ComputeHash i] (info : i)
(leanFile hashFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget)
(build : BuildM PUnit) : BuildM (ActiveBuildTarget i) := do
ActiveTarget.mk info <| ← depTarget.mapOpaqueAsync fun depTrace => do
def moduleTarget [GetMTime i] [ComputeHash i] (info : i)
(leanFile hashFile : FilePath) (contents : String) (depTarget : BuildTarget x)
(build : BuildM PUnit) : BuildTarget i :=
Target.mk info <| depTarget.mapOpaqueAsync fun depTrace => do
let (upToDate, trace) ← checkModuleTrace info leanFile hashFile contents depTrace
if upToDate then
BuildTrace.fromHash <| (← computeHash info).mix depTrace.hash
else
build
IO.FS.writeFile hashFile trace.hash.toString
let newTrace : BuildTrace ← liftM <| computeTrace info
let newTrace : BuildTrace ← liftM <| computeTrace info
newTrace.mix depTrace
def fetchModuleTarget (pkg : Package) (moreOleanDirs : List FilePath)
(mod : Name) (leanFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget)
: BuildM ActiveModuleTarget := do
let cFile := pkg.modToC mod
let oleanFile := pkg.modToOlean mod
let info := ModuleTargetInfo.mk oleanFile cFile
let hashFile := pkg.modToHashFile mod
let oleanDirs := pkg.oleanDir :: moreOleanDirs
mkModuleTarget info leanFile hashFile contents depTarget <|
compileOleanAndC leanFile oleanFile cFile oleanDirs pkg.rootDir pkg.leanArgs
def moduleOleanAndCTarget
(leanFile cFile oleanFile hashFile : FilePath)
(oleanDirs : List FilePath) (contents : String) (depTarget : BuildTarget x)
(rootDir : FilePath := ".") (leanArgs : Array String := #[]) :=
moduleTarget (OleanAndC.mk oleanFile cFile) leanFile hashFile contents depTarget <|
compileOleanAndC leanFile oleanFile cFile oleanDirs rootDir leanArgs
def fetchModuleOleanTarget (pkg : Package) (moreOleanDirs : List FilePath)
(mod : Name) (leanFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget)
: BuildM OleanTarget := do
let oleanFile := pkg.modToOlean mod
let hashFile := pkg.modToHashFile mod
let oleanDirs := pkg.oleanDir :: moreOleanDirs
mkModuleTarget oleanFile leanFile hashFile contents depTarget <|
compileOlean leanFile oleanFile oleanDirs pkg.rootDir pkg.leanArgs
def moduleOleanTarget
(leanFile oleanFile hashFile : FilePath)
(oleanDirs : List FilePath) (contents : String) (depTarget : BuildTarget x)
(rootDir : FilePath := ".") (leanArgs : Array String := #[]) :=
moduleTarget oleanFile leanFile hashFile contents depTarget <|
compileOlean leanFile oleanFile oleanDirs rootDir leanArgs
protected def Package.moduleOleanAndCTarget
(self : Package) (moreOleanDirs : List FilePath) (mod : Name)
(leanFile : FilePath) (contents : String) (depTarget : BuildTarget x) :=
let cFile := self.modToC mod
let oleanFile := self.modToOlean mod
let hashFile := self.modToHashFile mod
let oleanDirs := self.oleanDir :: moreOleanDirs
moduleOleanAndCTarget leanFile cFile oleanFile hashFile oleanDirs contents
depTarget self.rootDir self.leanArgs
protected def Package.moduleOleanTarget
(self : Package) (moreOleanDirs : List FilePath) (mod : Name)
(leanFile : FilePath) (contents : String) (depTarget : BuildTarget x) :=
let oleanFile := self.modToOlean mod
let hashFile := self.modToHashFile mod
let oleanDirs := self.oleanDir :: moreOleanDirs
moduleOleanTarget leanFile oleanFile hashFile oleanDirs contents depTarget
self.rootDir self.leanArgs
-- # Recursive Fetching
@ -126,32 +137,34 @@ def recFetchModuleWithLocalImports (pkg : Package)
let importTargets ← imports.mapM fetch
build mod leanFile contents importTargets
def recFetchModuleTargetWithLocalImports [Monad m] [MonadLiftT BuildM m]
(pkg : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
: RecFetch Name ActiveModuleTarget m :=
recFetchModuleWithLocalImports pkg fun mod leanFile contents importTargets => do
let allDepsTarget ← depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets
fetchModuleTarget pkg moreOleanDirs mod leanFile contents allDepsTarget
def Package.recFetchModuleOleanAndCTargetWithLocalImports [Monad m] [MonadLiftT BuildM m]
(self : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
: RecFetch Name ActiveOleanAndCTarget m :=
recFetchModuleWithLocalImports self fun mod leanFile contents importTargets => do
let allDepsTarget := Target.active <| ←
depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets
self.moduleOleanAndCTarget moreOleanDirs mod leanFile contents allDepsTarget |>.run
def recFetchModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m]
(pkg : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
: RecFetch Name OleanTarget m :=
recFetchModuleWithLocalImports pkg fun mod leanFile contents importTargets => do
let allDepsTarget ← depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets
fetchModuleOleanTarget pkg moreOleanDirs mod leanFile contents allDepsTarget
def Package.recFetchModuleOleanTargetWithLocalImports [Monad m] [MonadLiftT BuildM m]
(self : Package) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
: RecFetch Name ActiveFileTarget m :=
recFetchModuleWithLocalImports self fun mod leanFile contents importTargets => do
let allDepsTarget := Target.active <| ←
depTarget.mixOpaqueAsync <| ← ActiveTarget.collectOpaqueList importTargets
self.moduleOleanTarget moreOleanDirs mod leanFile contents allDepsTarget |>.run
-- ## Definitions
abbrev ModuleFetchM (α) :=
-- equivalent to `RBTopT (cmp := Name.quickCmp) Name ActiveModuleTarget BuildM`.
-- equivalent to `RBTopT (cmp := Name.quickCmp) Name α BuildM`.
-- phrased this way to use `NameMap`
EStateT (List Name) (NameMap α) BuildM
abbrev ModuleFetch (α) :=
RecFetch Name α (ModuleFetchM α)
abbrev OleanTargetFetch := ModuleFetch OleanTarget
abbrev ModuleTargetFetch := ModuleFetch ActiveModuleTarget
abbrev OleanTargetFetch := ModuleFetch ActiveFileTarget
abbrev OleanAndCTargetFetch := ModuleFetch ActiveOleanAndCTarget
abbrev OleanTargetMap := NameMap OleanTarget
abbrev ModuleTargetMap := NameMap ActiveModuleTarget
abbrev OleanTargetMap := NameMap ActiveFileTarget
abbrev OleanAndCTargetMap := NameMap ActiveOleanAndCTarget

80
Lake/BuildPackage.lean
View file

@ -17,65 +17,65 @@ namespace Lake
-- # Build Target
abbrev ActivePackageTarget := ActiveBuildTarget (Package × ModuleTargetMap)
abbrev ActivePackageTarget := ActiveBuildTarget (Package × NameMap ActiveOleanAndCTarget)
namespace ActivePackageTarget
def package (self : ActivePackageTarget) :=
self.info.1
def moduleTargetMap (self : ActivePackageTarget) : ModuleTargetMap :=
def moduleTargetMap (self : ActivePackageTarget) : NameMap ActiveOleanAndCTarget :=
self.info.2
def moduleTargets (self : ActivePackageTarget) : Array (Name × ActiveModuleTarget) :=
def moduleTargets (self : ActivePackageTarget) : Array (Name × ActiveOleanAndCTarget) :=
self.moduleTargetMap.fold (fun arr k v => arr.push (k, v)) #[]
end ActivePackageTarget
-- # Build Modules
def Package.buildModuleTargetDAGFor
(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
(self : Package) : BuildM (ActiveModuleTarget × ModuleTargetMap) := do
let fetch := recFetchModuleTargetWithLocalImports self moreOleanDirs depTarget
def Package.buildModuleOleanAndCTargetDAG
(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
(self : Package) : BuildM (ActiveOleanAndCTarget × OleanAndCTargetMap) := do
let fetch := self.recFetchModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget
failOnImportCycle <| ← buildRBTop fetch mod |>.run {}
def Package.buildOleanTargetDAGFor
(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
(self : Package) : BuildM (OleanTarget × OleanTargetMap) := do
def Package.buildModuleOleanTargetDAG
(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x)
(self : Package) : BuildM (ActiveFileTarget × OleanTargetMap) := do
let fetch := recFetchModuleOleanTargetWithLocalImports self moreOleanDirs depTarget
failOnImportCycle <| ← buildRBTop fetch mod |>.run {}
def Package.buildModuleTargetDAG
(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
self.buildModuleTargetDAGFor self.moduleRoot moreOleanDirs depTarget
def Package.buildOleanAndCTargetDAG
(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) :=
self.buildModuleOleanAndCTargetDAG self.moduleRoot moreOleanDirs depTarget
def Package.buildOleanTargetDAG
(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
self.buildOleanTargetDAGFor self.moduleRoot moreOleanDirs depTarget
(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) :=
self.buildModuleOleanTargetDAG self.moduleRoot moreOleanDirs depTarget
def Package.buildModuleTargets
def Package.buildOleanAndCTargets
(mods : List Name) (moreOleanDirs : List FilePath)
(depTarget : ActiveOpaqueTarget) (self : Package)
: BuildM (List ActiveModuleTarget) := do
let fetch : ModuleTargetFetch :=
recFetchModuleTargetWithLocalImports self moreOleanDirs depTarget
(depTarget : ActiveBuildTarget x) (self : Package)
: BuildM (List ActiveOleanAndCTarget) := do
let fetch : OleanAndCTargetFetch :=
self.recFetchModuleOleanAndCTargetWithLocalImports moreOleanDirs depTarget
failOnImportCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {}
def Package.buildOleanTargets
(mods : List Name) (moreOleanDirs : List FilePath)
(depTarget : ActiveOpaqueTarget) (self : Package)
: BuildM (List OleanTarget) := do
(depTarget : ActiveBuildTarget x) (self : Package)
: BuildM (List ActiveFileTarget) := do
let fetch : OleanTargetFetch :=
recFetchModuleOleanTargetWithLocalImports self moreOleanDirs depTarget
self.recFetchModuleOleanTargetWithLocalImports moreOleanDirs depTarget
failOnImportCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {}
def Package.buildRootModuleTarget
(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
self.buildModuleTargets [self.moduleRoot] moreOleanDirs depTarget |>.map (·.get! 0)
def Package.buildRootOleanAndCTarget
(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) :=
self.buildOleanAndCTargets [self.moduleRoot] moreOleanDirs depTarget |>.map (·.get! 0)
def Package.buildRootOleanTarget
(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
(moreOleanDirs : List FilePath) (depTarget : ActiveBuildTarget x) (self : Package) :=
self.buildOleanTargets [self.moduleRoot] moreOleanDirs depTarget |>.map (·.get! 0)
-- # Configure/Build Packages
@ -86,24 +86,30 @@ def Package.buildDepTargetWith
let depTarget ← ActiveTarget.collectOpaqueList depTargets
extraDepTarget.mixOpaqueAsync depTarget
def Package.buildTargetWithDepTargetsFor
def Package.buildModuleOleanAndCTargetWithDepTargets
(mod : Name) (depTargets : List ActivePackageTarget) (self : Package)
: BuildM ActivePackageTarget := do
let depTarget ← self.buildDepTargetWith depTargets
let moreOleanDirs := depTargets.map (·.package.oleanDir)
let (target, targetMap) ← self.buildModuleTargetDAGFor mod moreOleanDirs depTarget
let (target, targetMap) ← self.buildModuleOleanAndCTargetDAG mod moreOleanDirs depTarget
return target.withInfo ⟨self, targetMap⟩
def Package.buildTargetWithDepTargets
def Package.buildOleanAndCTargetsWithDepTargets
(depTargets : List ActivePackageTarget) (self : Package) : BuildM ActivePackageTarget :=
self.buildTargetWithDepTargetsFor self.moduleRoot depTargets
self.buildModuleOleanAndCTargetWithDepTargets self.moduleRoot depTargets
/--
The main package build function.
It resolves the package's dependencies and recursively builds them.
For each package, it compiles its modules into `.olean` and `.c` files.
-/
partial def Package.buildTarget (self : Package) : BuildM ActivePackageTarget := do
let deps ← solveDeps self
-- build dependencies recursively
-- TODO: share build of common dependencies
let depTargets ← deps.mapM (·.buildTarget)
self.buildTargetWithDepTargets depTargets
self.buildOleanAndCTargetsWithDepTargets depTargets
def Package.buildDepTargets (self : Package) : BuildM (List ActivePackageTarget) := do
let deps ← solveDeps self
@ -130,22 +136,22 @@ def build (pkg : Package) : IO PUnit :=
-- # Print Paths
def Package.buildOleanTargetsWithDeps
def Package.buildModuleOleanTargetsWithDeps
(deps : List Package) (mods : List Name) (self : Package)
: BuildM (List OleanTarget) := do
: BuildM (List ActiveFileTarget) := do
let moreOleanDirs := deps.map (·.oleanDir)
let depTarget ← self.buildDepTargetWith <| ← deps.mapM (·.buildTarget)
self.buildOleanTargets mods moreOleanDirs depTarget
def Package.buildOleansWithDeps
def Package.buildModuleOleansWithDeps
(deps : List Package) (mods : List Name) (self : Package) :=
self.buildOleanTargetsWithDeps deps mods >>= (·.forM (discard ·.materialize))
self.buildModuleOleanTargetsWithDeps deps mods >>= (·.forM (discard ·.materialize))
def printPaths (pkg : Package) (imports : List String := []) : IO Unit := do
let deps ← solveDeps pkg
unless imports.isEmpty do
let imports := imports.map (·.toName)
let localImports := imports.filter (·.getRoot == pkg.moduleRoot)
runBuild <| pkg.buildOleansWithDeps deps localImports
runBuild <| pkg.buildModuleOleansWithDeps deps localImports
IO.println <| SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
IO.println <| SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir)

7
Lake/Target.lean
View file

@ -49,12 +49,15 @@ protected def bindAsync [BindAsync m n] (self : ActiveTarget i n α) (f : i →
protected def bindOpaqueAsync [BindAsync m n] (self : ActiveTarget i n α) (f : α → m (n β)) : m (n β) :=
bindAsync self.task f
def materializeAsync [Pure m] (self : ActiveTarget i n t) : m (n t) :=
pure self.task
def materialize [Await n m] (self : ActiveTarget i n t) : m t :=
await self.task
def mixOpaqueAsync
[MixTrace t] [Monad m] [Pure n] [BindAsync m n]
(t1 t2 : ActiveTarget i n t) : m (ActiveTarget PUnit n t) := do
(t1 : ActiveTarget α n t) (t2 : ActiveTarget β n t) : m (ActiveTarget PUnit n t) := do
ActiveTarget.opaque <| ←
t1.bindOpaqueAsync fun tr1 =>
t2.bindOpaqueAsync fun tr2 =>
@ -135,7 +138,7 @@ def build [Await n m] [Functor m] [Bind m] (self : Target i m n t) : m i := do
def mixOpaqueAsync
[MixTrace t] [Monad m] [Pure n] [BindAsync m n]
(t1 t2 : Target i m n t) : Target PUnit m n t :=
(t1 : Target α m n t) (t2 : Target β m n t) : Target PUnit m n t :=
Target.opaque do
let tk1 ← t1.materializeAsync
let tk2 ← t2.materializeAsync