diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean index 49d656273e..40ef44a3cf 100644 --- a/Lake/Build/Facets.lean +++ b/Lake/Build/Facets.lean @@ -47,9 +47,8 @@ instance [FamilyDef ModuleData facet α] : CoeDep Name facet (ModuleFacet α) := /-- The core compilation / elaboration of the Lean file via `lean`, -which produce the Lean binaries of the module (i.e., `olean` and `ilean`). +which produce the Lean binaries of the module (i.e., `olean`, `ilean`, `c`). It is thus the facet used by default for building imports of a module. -Also, if the module is not lean-only, it produces `c` files as well. -/ abbrev Module.leanBinFacet := `bin module_data bin : BuildJob Unit diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 05fdaf629c..f16292ca19 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -13,7 +13,7 @@ namespace Lake def Module.buildUnlessUpToDate (mod : Module) (dynlibPath : SearchPath) (dynlibs : Array FilePath) -(depTrace : BuildTrace) (leanOnly : Bool) : BuildM BuildTrace := do +(depTrace : BuildTrace) : BuildM BuildTrace := do let isOldMode ← getIsOldMode let argTrace : BuildTrace := pureHash mod.leanArgs let srcTrace : BuildTrace ← computeTrace mod.leanFile @@ -24,21 +24,9 @@ def Module.buildUnlessUpToDate (mod : Module) else modTrace.checkAgainstFile mod mod.traceFile let name := mod.name.toString - if leanOnly then - unless modUpToDate do - compileLeanModule name mod.leanFile mod.oleanFile mod.ileanFile none - (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) - else - let cUpToDate ← - if isOldMode then - pure modUpToDate - else - (modUpToDate && ·) <$> modTrace.checkAgainstFile mod.cFile mod.cTraceFile - unless cUpToDate do - compileLeanModule name mod.leanFile mod.oleanFile mod.ileanFile mod.cFile - (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) - unless isOldMode do - modTrace.writeToFile mod.cTraceFile + unless modUpToDate do + compileLeanModule name mod.leanFile mod.oleanFile mod.ileanFile mod.cFile + (← getLeanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) unless isOldMode do modTrace.writeToFile mod.traceFile return mixTrace (← computeTrace mod) depTrace @@ -118,12 +106,9 @@ def Module.precompileImportsFacetConfig : ModuleFacetConfig precompileImportsFac mkFacetConfig (·.recComputePrecompileImports) /-- -Recursively build a module and its (transitive, local) imports, -optionally outputting a `.c` file if not `leanOnly`. +Recursively build a module and its (transitive, local) imports. -/ -def Module.recBuildLeanCore (mod : Module) -(leanOnly : Bool) : IndexBuildM (BuildJob Unit) := do - +private def Module.recBuildLeanCore (mod : Module) : IndexBuildM (BuildJob Unit) := do -- Compute and build dependencies let imports ← mod.imports.fetch let extraDepJob ← mod.pkg.extraDep.fetch @@ -136,79 +121,46 @@ def Module.recBuildLeanCore (mod : Module) let externDynlibsJob ← BuildJob.collectArray externJobs let modDynlibsJob ← BuildJob.collectArray modJobs - -- Build Module - show SchedulerM _ from do - extraDepJob.bindAsync fun _ _ => do - importJob.bindAsync fun _ importTrace => do - modDynlibsJob.bindAsync fun modDynlibs modTrace => do - externDynlibsJob.bindSync fun externDynlibs externTrace => do - let depTrace := importTrace.mix <| modTrace.mix externTrace - /- - Requirements: - * Lean wants the external library symbols before module symbols. - * Unix requires the file extension of the dynlib. - * For some reason, building from the Lean server requires full paths. - Everything else loads fine with just the augmented library path. - * Linux still needs the augmented path to resolve nested dependencies in dynlibs. - -/ - let dynlibPath := libDirs ++ externDynlibs.filterMap (·.dir?) |>.toList - let dynlibs := externDynlibs.map (·.path) ++ modDynlibs.map (·.path) - let trace ← mod.buildUnlessUpToDate dynlibPath dynlibs depTrace leanOnly - return ((), trace) - -/-- Possible artifacts of the `lean` command. -/ -inductive LeanArtifact -| none | olean | ilean | c -deriving Inhabited, Repr, DecidableEq - -/-- -Recursively build a module using `recBuildLeanCore`, outputting a -`.c` file if the module is not lean-only or the requested artifact is `c`. -Returns a build job producing the requested artifact. --/ -def Module.recBuildLean (mod : Module) (art : LeanArtifact) -: IndexBuildM (BuildJob (if art = .none then Unit else FilePath)) := do - let leanOnly := mod.isLeanOnly ∧ art ≠ .c - let modJob ← mod.recBuildLeanCore leanOnly - -- Save All Resulting Jobs & Return Requested One - store mod.leanBin.key modJob - let oleanJob ← modJob.bindSync fun _ depTrace => - return (mod.oleanFile, mixTrace (← computeTrace mod.oleanFile) depTrace) - store mod.olean.key <| oleanJob - let ileanJob ← modJob.bindSync fun _ depTrace => - return (mod.ileanFile, mixTrace (← computeTrace mod.ileanFile) depTrace) - store mod.ilean.key <| ileanJob - if h : leanOnly then - have : art ≠ .c := h.2 - return match art with - | .none => modJob - | .olean => oleanJob - | .ilean => ileanJob - else - let cJob ← modJob.bindSync fun _ _ => - return (mod.cFile, mixTrace (← computeTrace mod.cFile) (← getLeanTrace)) - store mod.c.key cJob - return match art with - | .none => modJob - | .olean => oleanJob - | .ilean => ileanJob - | .c => cJob + extraDepJob.bindAsync fun _ _ => do + importJob.bindAsync fun _ importTrace => do + modDynlibsJob.bindAsync fun modDynlibs modTrace => do + externDynlibsJob.bindSync fun externDynlibs externTrace => do + let depTrace := importTrace.mix <| modTrace.mix externTrace + /- + Requirements: + * Lean wants the external library symbols before module symbols. + * Unix requires the file extension of the dynlib. + * For some reason, building from the Lean server requires full paths. + Everything else loads fine with just the augmented library path. + * Linux still needs the augmented path to resolve nested dependencies in dynlibs. + -/ + let dynlibPath := libDirs ++ externDynlibs.filterMap (·.dir?) |>.toList + let dynlibs := externDynlibs.map (·.path) ++ modDynlibs.map (·.path) + let trace ← mod.buildUnlessUpToDate dynlibPath dynlibs depTrace + return ((), trace) /-- The `ModuleFacetConfig` for the builtin `leanBinFacet`. -/ def Module.leanBinFacetConfig : ModuleFacetConfig leanBinFacet := - mkFacetJobConfig (·.recBuildLean .none) + mkFacetJobConfig (·.recBuildLeanCore) /-- The `ModuleFacetConfig` for the builtin `oleanFacet`. -/ def Module.oleanFacetConfig : ModuleFacetConfig oleanFacet := - mkFacetJobConfig (·.recBuildLean .olean) + mkFacetJobConfig fun mod => do + (← mod.leanBin.fetch).bindSync fun _ depTrace => + return (mod.oleanFile, mixTrace (← computeTrace mod.oleanFile) depTrace) /-- The `ModuleFacetConfig` for the builtin `ileanFacet`. -/ def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet := - mkFacetJobConfig (·.recBuildLean .ilean) + mkFacetJobConfig fun mod => do + (← mod.leanBin.fetch).bindSync fun _ depTrace => + return (mod.ileanFile, depTrace) /-- The `ModuleFacetConfig` for the builtin `cFacet`. -/ def Module.cFacetConfig : ModuleFacetConfig cFacet := - mkFacetJobConfig (·.recBuildLean .c) + mkFacetJobConfig fun mod => do + (← mod.leanBin.fetch).bindSync fun _ _ => + -- do content-aware hashing so that we avoid recompiling unchanged C files + return (mod.cFile, ← computeTrace mod.cFile) /-- Recursively build the module's object file from its C file produced by `lean`. -/ def Module.recBuildLeanO (self : Module) : IndexBuildM (BuildJob FilePath) := do diff --git a/Lake/Config/Module.lean b/Lake/Config/Module.lean index 481e07a92c..9f884e8f85 100644 --- a/Lake/Config/Module.lean +++ b/Lake/Config/Module.lean @@ -78,9 +78,6 @@ abbrev pkg (self : Module) : Package := @[inline] def cFile (self : Module) : FilePath := self.irPath "c" -@[inline] def cTraceFile (self : Module) : FilePath := - self.irPath "c.trace" - @[inline] def oFile (self : Module) : FilePath := self.irPath "o"