feat: build and print-paths now build only oleans
This commit is contained in:
tydeu
parent
ac1cc9e62c
commit
4ce8716b99
3 changed files with 173 additions and 87 deletions
|
|
@ -16,18 +16,29 @@ open Lean hiding SearchPath
|
|||
|
||||
namespace Lake
|
||||
|
||||
-- # Build Target
|
||||
-- # Targets
|
||||
|
||||
abbrev OleanTarget := ActiveFileTarget
|
||||
|
||||
structure ModuleArtifact where
|
||||
oleanFile : FilePath
|
||||
cFile : FilePath
|
||||
deriving Inhabited
|
||||
|
||||
protected def ModuleArtifact.getMTime (self : ModuleArtifact) : IO MTime := do
|
||||
return max (← getMTime self.oleanFile) (← getMTime self.cFile)
|
||||
namespace ModuleArtifact
|
||||
|
||||
protected def getMTime (self : ModuleArtifact) : IO MTime := do
|
||||
return mixTrace (← getMTime self.oleanFile) (← getMTime self.cFile)
|
||||
|
||||
instance : GetMTime ModuleArtifact := ⟨ModuleArtifact.getMTime⟩
|
||||
|
||||
protected def computeHash (self : ModuleArtifact) : IO Hash := do
|
||||
return mixTrace (← computeHash self.oleanFile) (← computeHash self.cFile)
|
||||
|
||||
instance : ComputeHash ModuleArtifact := ⟨ModuleArtifact.computeHash⟩
|
||||
|
||||
end ModuleArtifact
|
||||
|
||||
abbrev ModuleTarget := ActiveBuildTarget ModuleArtifact
|
||||
|
||||
namespace ModuleTarget
|
||||
|
|
@ -58,65 +69,96 @@ def checkIfSameHash (hash : Hash) (file : FilePath) : IO Bool :=
|
|||
def skipIf [Pure m] [Pure n] (cond : Bool) (build : m (n PUnit)) : m (n PUnit) := do
|
||||
if cond then pure (pure ()) else build
|
||||
|
||||
-- # Build Modules
|
||||
def checkModuleTrace [GetMTime a] (artifact : a)
|
||||
(leanFile hashFile : FilePath) (contents : String) (depTrace : LakeTrace)
|
||||
: IO (Bool × LakeTrace) := do
|
||||
let leanMTime ← getMTime leanFile
|
||||
let leanHash := Hash.compute contents
|
||||
let maxMTime := max leanMTime depTrace.mtime
|
||||
let fullHash := Hash.mix leanHash depTrace.hash
|
||||
let sameHash ← checkIfSameHash fullHash hashFile
|
||||
try
|
||||
discard <| getMTime artifact -- ensure the artifact actually exists
|
||||
let mtime := ite sameHash 0 maxMTime
|
||||
(sameHash, ⟨fullHash, mtime⟩)
|
||||
catch _ =>
|
||||
(false, ⟨fullHash, maxMTime⟩)
|
||||
|
||||
-- # Module Builders
|
||||
|
||||
def fetchModuleTarget (pkg : Package) (moreOleanDirs : List FilePath)
|
||||
(mod : Name) (leanFile : FilePath) (contents : String) (depTarget : ActiveOpaqueTarget)
|
||||
: BuildM ModuleTarget := do
|
||||
let cFile := pkg.modToC mod
|
||||
let oleanFile := pkg.modToOlean mod
|
||||
let artifact := ModuleArtifact.mk oleanFile cFile
|
||||
let hashFile := pkg.modToHashFile mod
|
||||
let oleanDirs := pkg.oleanDir :: moreOleanDirs
|
||||
let (upToDate, trace) ← checkModuleTrace artifact leanFile hashFile contents depTarget.trace
|
||||
ActiveTarget.mk artifact trace <| ← skipIf upToDate <| depTarget.andThen do
|
||||
compileOleanAndC leanFile oleanFile cFile oleanDirs pkg.rootDir pkg.leanArgs
|
||||
IO.FS.writeFile hashFile trace.hash.toString
|
||||
|
||||
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
|
||||
let (upToDate, trace) ← checkModuleTrace oleanFile leanFile hashFile contents depTarget.trace
|
||||
ActiveTarget.mk oleanFile trace <| ← skipIf upToDate <| depTarget.andThen do
|
||||
compileOlean leanFile oleanFile oleanDirs pkg.rootDir pkg.leanArgs
|
||||
IO.FS.writeFile hashFile trace.hash.toString
|
||||
|
||||
-- # Recursive Fetching
|
||||
|
||||
/-
|
||||
Produces a recursive module target fetcher that
|
||||
builds the target module after waiting for `depTargets` to materialize
|
||||
and recursively fetching its local imports (relative to `pkg`).
|
||||
|
||||
The module is built with the configuration from `pkg` and
|
||||
a `LEAN_PATH` that includes `oleanDirs`.
|
||||
builds the target module after recursively fetching its local imports
|
||||
(relative to `pkg`).
|
||||
-/
|
||||
def fetchModuleWithLocalImports
|
||||
(pkg : Package) (oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
|
||||
{m} [Monad m] [MonadLiftT BuildM m] [MonadExceptOf IO.Error m] : RecFetch Name ModuleTarget m :=
|
||||
def recFetchModuleWithLocalImports (pkg : Package)
|
||||
[Monad m] [MonadLiftT BuildM m] (build : Name → FilePath → String → List α → m α)
|
||||
: RecFetch Name α m := fun mod fetch => do
|
||||
have : MonadLift BuildM m := ⟨liftM⟩
|
||||
let leanPath := SearchPath.toString <| pkg.oleanDir :: oleanDirs
|
||||
fun mod fetch => do
|
||||
let leanFile := pkg.modToSrc mod
|
||||
let contents ← liftM (m := BuildM) <| IO.FS.readFile leanFile
|
||||
-- parse direct local imports
|
||||
let (imports, _, _) ← Elab.parseImports contents leanFile.toString
|
||||
let imports := imports.map (·.module) |>.filter (·.getRoot == pkg.moduleRoot)
|
||||
-- we fetch the import targets even if a rebuild is not required
|
||||
-- because other build processes (ex. `.o`) rely on the map being complete
|
||||
let importTargets ← imports.mapM fetch
|
||||
-- calculate trace
|
||||
let leanMTime ← getMTime leanFile
|
||||
let leanHash := Hash.compute contents
|
||||
let depTrace := mixTrace depTarget.trace
|
||||
(mixTraceList <| importTargets.map (·.trace))
|
||||
let maxMTime := max leanMTime depTrace.mtime
|
||||
let fullHash := Hash.mix leanHash depTrace.hash
|
||||
let hashFile := pkg.modToHashFile mod
|
||||
let sameHash ← checkIfSameHash fullHash hashFile
|
||||
let mtime := ite sameHash 0 maxMTime
|
||||
-- construct target
|
||||
let cFile := pkg.modToC mod
|
||||
let oleanFile := pkg.modToOlean mod
|
||||
let depTasks := depTarget.task :: importTargets.map (·.task)
|
||||
ActiveTarget.mk ⟨oleanFile, cFile⟩ ⟨fullHash, mtime⟩ <| ←
|
||||
skipIf sameHash <| afterTaskList (m := BuildM) depTasks do
|
||||
compileOleanAndC leanFile oleanFile cFile leanPath pkg.rootDir pkg.leanArgs
|
||||
IO.FS.writeFile hashFile fullHash.toString
|
||||
let leanFile := pkg.modToSrc mod
|
||||
let contents ← IO.FS.readFile leanFile
|
||||
-- parse direct local imports
|
||||
let (imports, _, _) ← Elab.parseImports contents leanFile.toString
|
||||
let imports := imports.map (·.module) |>.filter (·.getRoot == pkg.moduleRoot)
|
||||
-- we fetch the import targets even if a rebuild is not required
|
||||
-- because other build processes (ex. `.o`) rely on the map being complete
|
||||
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 ModuleTarget m :=
|
||||
recFetchModuleWithLocalImports pkg fun mod leanFile contents importTargets => do
|
||||
let importTarget ← ActiveOpaqueTarget.collectList importTargets
|
||||
let allDepTarget ← depTarget.andThenTargetAsync importTarget
|
||||
fetchModuleTarget pkg moreOleanDirs mod leanFile contents allDepTarget
|
||||
|
||||
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 importTarget ← ActiveOpaqueTarget.collectList importTargets
|
||||
let allDepTarget ← depTarget.andThenTargetAsync importTarget
|
||||
fetchModuleOleanTarget pkg moreOleanDirs mod leanFile contents allDepTarget
|
||||
|
||||
-- ## Definitions
|
||||
|
||||
abbrev ModuleM (α) :=
|
||||
-- equivalent to `RBTopT (cmp := Name.quickCmp) Name ModuleTarget BuildM`.
|
||||
-- phrased this way to use `NameMap`
|
||||
EStateT (List Name) (NameMap α) BuildM
|
||||
|
||||
abbrev ModuleFetch (α) :=
|
||||
RecFetch Name α (ModuleM α)
|
||||
|
||||
abbrev OleanTargetFetch := ModuleFetch OleanTarget
|
||||
abbrev ModuleTargetFetch := ModuleFetch ModuleTarget
|
||||
|
||||
abbrev OleanTargetMap := NameMap OleanTarget
|
||||
abbrev ModuleTargetMap := NameMap ModuleTarget
|
||||
|
||||
/-
|
||||
Equivalent to `RBTopT (cmp := Name.quickCmp) Name ModuleTarget BuildM`.
|
||||
Phrased this way to use `ModuleTargetMap`.
|
||||
-/
|
||||
abbrev ModuleTargetM :=
|
||||
EStateT (List Name) ModuleTargetMap BuildM
|
||||
|
||||
abbrev ModuleTargetFetch :=
|
||||
RecFetch Name ModuleTarget ModuleTargetM
|
||||
|
||||
def failOnCycle : Except (List Name) α → BuildM α
|
||||
| Except.ok a => a
|
||||
| Except.error cycle => do
|
||||
let cycle := cycle.map (s!" {·}")
|
||||
let msg := s!"import cycle detected:\n{"\n".intercalate cycle}"
|
||||
BuildM.logError msg
|
||||
throw <| IO.userError msg
|
||||
|
|
|
|||
|
|
@ -35,32 +35,63 @@ end PackageTarget
|
|||
-- # Build Modules
|
||||
|
||||
def Package.buildModuleTargetDAGFor
|
||||
(mod : Name) (oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
|
||||
(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
|
||||
(self : Package) : BuildM (ModuleTarget × ModuleTargetMap) := do
|
||||
let fetch := fetchModuleWithLocalImports self oleanDirs depTarget
|
||||
failOnCycle <| ← buildRBTop fetch mod |>.run {}
|
||||
let fetch := recFetchModuleTargetWithLocalImports self moreOleanDirs depTarget
|
||||
failOnImportCycle <| ← buildRBTop fetch mod |>.run {}
|
||||
|
||||
def Package.buildOleanTargetDAGFor
|
||||
(mod : Name) (moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget)
|
||||
(self : Package) : BuildM (OleanTarget × OleanTargetMap) := do
|
||||
let fetch := recFetchModuleOleanTargetWithLocalImports self moreOleanDirs depTarget
|
||||
failOnImportCycle <| ← buildRBTop fetch mod |>.run {}
|
||||
|
||||
def Package.buildModuleTargetDAG
|
||||
(oleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
|
||||
self.buildModuleTargetDAGFor self.moduleRoot oleanDirs depTarget
|
||||
(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
|
||||
self.buildModuleTargetDAGFor self.moduleRoot moreOleanDirs depTarget
|
||||
|
||||
def Package.buildOleanTargetDAG
|
||||
(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
|
||||
self.buildOleanTargetDAGFor self.moduleRoot moreOleanDirs depTarget
|
||||
|
||||
def Package.buildModuleTargets
|
||||
(mods : List Name) (oleanDirs : List FilePath)
|
||||
(mods : List Name) (moreOleanDirs : List FilePath)
|
||||
(depTarget : ActiveOpaqueTarget) (self : Package)
|
||||
: BuildM (List ModuleTarget) := do
|
||||
let fetch : ModuleTargetFetch := fetchModuleWithLocalImports self oleanDirs depTarget
|
||||
failOnCycle <| ← mods.mapM (buildRBTop fetch) |>.run' {}
|
||||
let fetch : ModuleTargetFetch :=
|
||||
recFetchModuleTargetWithLocalImports self 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
|
||||
let fetch : OleanTargetFetch :=
|
||||
recFetchModuleOleanTargetWithLocalImports self 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.buildRootOleanTarget
|
||||
(moreOleanDirs : List FilePath) (depTarget : ActiveOpaqueTarget) (self : Package) :=
|
||||
self.buildOleanTargets [self.moduleRoot] moreOleanDirs depTarget |>.map (·.get! 0)
|
||||
|
||||
-- # Configure/Build Packages
|
||||
|
||||
def Package.buildDepTargetWith
|
||||
(depTargets : List PackageTarget) (self : Package) : BuildM ActiveOpaqueTarget := do
|
||||
let extraDepTarget ← self.buildExtraDepTarget
|
||||
let depTarget ← ActiveOpaqueTarget.collectList depTargets
|
||||
depTarget.andThenTargetAsync extraDepTarget
|
||||
|
||||
def Package.buildTargetWithDepTargetsFor
|
||||
(mod : Name) (depTargets : List PackageTarget) (self : Package)
|
||||
: BuildM PackageTarget := do
|
||||
let extraDepTarget ← self.buildExtraDepTarget
|
||||
let depTarget ← ActiveOpaqueTarget.collectList depTargets
|
||||
let allDepsTarget ← extraDepTarget.andThenTargetAsync depTarget
|
||||
let oleanDirs := depTargets.map (·.package.oleanDir)
|
||||
let (target, targetMap) ← self.buildModuleTargetDAGFor mod oleanDirs allDepsTarget
|
||||
let depTarget ← self.buildDepTargetWith depTargets
|
||||
let moreOleanDirs := depTargets.map (·.package.oleanDir)
|
||||
let (target, targetMap) ← self.buildModuleTargetDAGFor mod moreOleanDirs depTarget
|
||||
return {target with artifact := ⟨self, targetMap⟩}
|
||||
|
||||
def Package.buildTargetWithDepTargets
|
||||
|
|
@ -88,32 +119,33 @@ def configure (pkg : Package) : IO Unit :=
|
|||
runBuild pkg.buildDeps
|
||||
|
||||
def Package.build (self : Package) : BuildM PUnit := do
|
||||
(← self.buildTarget).materialize
|
||||
let depTargets ← self.buildDepTargets
|
||||
let depTarget ← self.buildDepTargetWith depTargets
|
||||
let moreOleanDirs := depTargets.map (·.package.oleanDir)
|
||||
let target ← self.buildRootOleanTarget moreOleanDirs depTarget
|
||||
target.materialize
|
||||
|
||||
def build (pkg : Package) : IO PUnit :=
|
||||
runBuild pkg.build
|
||||
|
||||
-- # Print Paths
|
||||
|
||||
def Package.buildModuleTargetsWithDeps
|
||||
(deps : List Package) (mods : List Name) (self : Package)
|
||||
: BuildM (List ModuleTarget) := do
|
||||
let oleanDirs := deps.map (·.oleanDir)
|
||||
let extraDepTarget ← self.buildExtraDepTarget
|
||||
let depTarget ← ActiveOpaqueTarget.collectList <| ← deps.mapM (·.buildTarget)
|
||||
let allDepsTarget ← extraDepTarget.andThenTargetAsync depTarget
|
||||
self.buildModuleTargets mods oleanDirs allDepsTarget
|
||||
def Package.buildOleanTargetsWithDeps
|
||||
(deps : List Package) (mods : List Name) (self : Package)
|
||||
: BuildM (List OleanTarget) := do
|
||||
let moreOleanDirs := deps.map (·.oleanDir)
|
||||
let depTarget ← self.buildDepTargetWith <| ← deps.mapM (·.buildTarget)
|
||||
self.buildOleanTargets mods moreOleanDirs depTarget
|
||||
|
||||
def Package.buildModulesWithDeps
|
||||
(deps : List Package) (mods : List Name) (self : Package)
|
||||
: BuildM PUnit := do
|
||||
(← self.buildModuleTargetsWithDeps deps mods).forM (·.materialize)
|
||||
def Package.buildOleansWithDeps
|
||||
(deps : List Package) (mods : List Name) (self : Package) :=
|
||||
self.buildOleanTargetsWithDeps deps mods >>= (·.forM (·.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.buildModulesWithDeps deps localImports
|
||||
runBuild <| pkg.buildOleansWithDeps deps localImports
|
||||
IO.println <| SearchPath.toString <| pkg.oleanDir :: deps.map (·.oleanDir)
|
||||
IO.println <| SearchPath.toString <| pkg.srcDir :: deps.map (·.srcDir)
|
||||
|
|
|
|||
|
|
@ -26,8 +26,20 @@ def proc (args : IO.Process.SpawnArgs) : BuildM PUnit := do
|
|||
BuildM.logError msg -- log errors early
|
||||
throw <| IO.userError msg
|
||||
|
||||
def compileOlean (leanFile oleanFile : FilePath)
|
||||
(oleanDirs : List FilePath := []) (rootDir : FilePath := ".") (leanArgs : Array String := #[])
|
||||
: BuildM PUnit := do
|
||||
createParentDirs oleanFile
|
||||
proc {
|
||||
cmd := "lean"
|
||||
args := leanArgs ++ #[
|
||||
"-R", rootDir.toString, "-o", oleanFile.toString, leanFile.toString
|
||||
]
|
||||
env := #[("LEAN_PATH", SearchPath.toString oleanDirs)]
|
||||
}
|
||||
|
||||
def compileOleanAndC (leanFile oleanFile cFile : FilePath)
|
||||
(leanPath : String := "") (rootDir : FilePath := ".") (leanArgs : Array String := #[])
|
||||
(oleanDirs : List FilePath := []) (rootDir : FilePath := ".") (leanArgs : Array String := #[])
|
||||
: BuildM PUnit := do
|
||||
createParentDirs cFile
|
||||
createParentDirs oleanFile
|
||||
|
|
@ -37,7 +49,7 @@ def compileOleanAndC (leanFile oleanFile cFile : FilePath)
|
|||
"-R", rootDir.toString, "-o", oleanFile.toString, "-c",
|
||||
cFile.toString, leanFile.toString
|
||||
]
|
||||
env := #[("LEAN_PATH", leanPath)]
|
||||
env := #[("LEAN_PATH", SearchPath.toString oleanDirs)]
|
||||
}
|
||||
|
||||
def compileO (oFile cFile : FilePath)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue