diff --git a/Lake/Build/Facets.lean b/Lake/Build/Facets.lean index 29f9922..681cab0 100644 --- a/Lake/Build/Facets.lean +++ b/Lake/Build/Facets.lean @@ -34,15 +34,20 @@ instance [DynamicType ModuleData facet α] : CoeDep WfName facet (ModuleFacet α ⟨facet, eq_dynamic_type⟩ namespace Module -abbrev binFacet := &`lean.bin +abbrev leanBinFacet := &`lean.bin abbrev oleanFacet := &`olean abbrev ileanFacet := &`ilean abbrev cFacet := &`lean.c abbrev oFacet := &`lean.o -abbrev dynlibFacet := &`lean.dynlib +abbrev dynlibFacet := &`dynlib end Module -/-- Lean binary build (`olean`, `ilean` files) -/ +/-- +The core compilation / elaboration of the Lean file via `lean`, +which produce the Lean binaries of the module (i.e., `olean` and `ilean`). +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. +-/ module_data lean.bin : ActiveOpaqueTarget /-- The `olean` file produced by `lean` -/ @@ -58,7 +63,7 @@ module_data lean.c : ActiveFileTarget module_data lean.o : ActiveFileTarget /-- Shared library for `--load-dynlib` -/ -module_data lean.dynlib : ActiveFileTarget +module_data dynlib : ActiveFileTarget -- ## Package Facets diff --git a/Lake/Build/Imports.lean b/Lake/Build/Imports.lean index 5a4bf5a..e7be6d9 100644 --- a/Lake/Build/Imports.lean +++ b/Lake/Build/Imports.lean @@ -44,10 +44,8 @@ def Package.buildImportsAndDeps (imports : List String) (self : Package) : Build let (res, bStore) ← EStateT.run BuildStore.empty <| mods.mapM fun mod => if mod.shouldPrecompile then buildIndexTop mod.dynlib <&> (·.withoutInfo) - else if mod.isLeanOnly then - buildIndexTop mod.leanBin else - buildIndexTop mod.c <&> (·.withoutInfo) + buildIndexTop mod.leanBin let importTargets ← failOnBuildCycle res let dynlibTargets := bStore.collectModuleFacetArray Module.dynlibFacet let externLibTargets := bStore.collectSharedExternLibs diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean index 63d8bd0..5077915 100644 --- a/Lake/Build/Index.lean +++ b/Lake/Build/Index.lean @@ -91,20 +91,11 @@ the initial set of Lake module facets (e.g., `lean.{imports, c, o, dynlib]`). ModuleBuildMap.empty (m := m) -- Compute unique imports (direct × transitive) |>.insert importFacet (mkModuleFacetBuild (·.recParseImports)) - -- Build module (`.olean` and `.ilean`) - |>.insert binFacet (mkModuleFacetBuild (fun mod => do - mod.recBuildLean !mod.isLeanOnly - )) - |>.insert oleanFacet (mkModuleFacetBuild (fun mod => do - mod.recBuildLean (!mod.isLeanOnly) <&> (·.withInfo mod.oleanFile) - )) - |>.insert ileanFacet (mkModuleFacetBuild (fun mod => do - mod.recBuildLean (!mod.isLeanOnly) <&> (·.withInfo mod.ileanFile) - )) - -- Build module `.c` (and `.olean` and `.ilean`) - |>.insert cFacet (mkModuleFacetBuild <| fun mod => do - mod.recBuildLean true <&> (·.withInfo mod.cFile) - ) + -- Build module (`.olean`, `.ilean`, and possibly `.c`) + |>.insert leanBinFacet (mkModuleFacetBuild (·.recBuildLean .leanBin)) + |>.insert oleanFacet (mkModuleFacetBuild (·.recBuildLean .olean)) + |>.insert ileanFacet (mkModuleFacetBuild (·.recBuildLean .ilean)) + |>.insert cFacet (mkModuleFacetBuild (·.recBuildLean .c)) -- Build module `.o` |>.insert oFacet (mkModuleFacetBuild <| fun mod => do mod.mkOTarget (Target.active (← mod.c.recBuild)) |>.activate diff --git a/Lake/Build/IndexTargets.lean b/Lake/Build/IndexTargets.lean index fbeabae..c387a64 100644 --- a/Lake/Build/IndexTargets.lean +++ b/Lake/Build/IndexTargets.lean @@ -45,7 +45,7 @@ def LeanLib.buildModules (self : LeanLib) (facet : WfName) buildMods.catchFailure fun _ => pure <| failure @[inline] protected def LeanLib.leanTarget (self : LeanLib) : OpaqueTarget := - Target.opaque <| self.buildModules Module.binFacet + Target.opaque <| self.buildModules Module.leanBinFacet @[inline] protected def Package.leanLibTarget (self : Package) : OpaqueTarget := self.builtinLib.leanTarget diff --git a/Lake/Build/Info.lean b/Lake/Build/Info.lean index 6144e39..a404000 100644 --- a/Lake/Build/Info.lean +++ b/Lake/Build/Info.lean @@ -152,7 +152,7 @@ abbrev facet (facet : WfName) (self : Module) : BuildInfo := variable (self : Module) abbrev imports := self.facet importFacet -abbrev leanBin := self.facet binFacet +abbrev leanBin := self.facet leanBinFacet abbrev olean := self.facet oleanFacet abbrev ilean := self.facet ileanFacet abbrev c := self.facet cFacet diff --git a/Lake/Build/Module.lean b/Lake/Build/Module.lean index 141697d..eac7380 100644 --- a/Lake/Build/Module.lean +++ b/Lake/Build/Module.lean @@ -15,24 +15,32 @@ namespace Lake -- # Solo Module Targets def Module.soloTarget (mod : Module) (dynlibs : Array FilePath) -(dynlibPath : SearchPath) (depTarget : BuildTarget x) (c := true) : OpaqueTarget := +(dynlibPath : SearchPath) (depTarget : BuildTarget x) (leanOnly : Bool) : OpaqueTarget := Target.opaque <| depTarget.bindOpaqueSync fun depTrace => do let argTrace : BuildTrace := pureHash mod.leanArgs let srcTrace : BuildTrace ← computeTrace mod.leanFile let modTrace := (← getLeanTrace).mix <| argTrace.mix <| srcTrace.mix depTrace let modUpToDate ← modTrace.checkAgainstFile mod mod.traceFile - if c then + if leanOnly then + unless modUpToDate do + compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none + (← getOleanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) + else let cUpToDate ← modTrace.checkAgainstFile mod.cFile mod.cTraceFile unless modUpToDate && cUpToDate do compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile mod.cFile (← getOleanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) modTrace.writeToFile mod.cTraceFile - else - unless modUpToDate do - compileLeanModule mod.leanFile mod.oleanFile mod.ileanFile none - (← getOleanPath) mod.rootDir dynlibs dynlibPath mod.leanArgs (← getLean) modTrace.writeToFile mod.traceFile - return depTrace + return mixTrace (← computeTrace mod) depTrace + +def Module.mkOleanTarget (modTarget : BuildTarget x) (self : Module) : FileTarget := + Target.mk self.oleanFile <| modTarget.bindOpaqueSync fun depTrace => + return mixTrace (← computeTrace self.oleanFile) depTrace + +def Module.mkIleanTarget (modTarget : BuildTarget x) (self : Module) : FileTarget := + Target.mk self.ileanFile <| modTarget.bindOpaqueSync fun depTrace => + return mixTrace (← computeTrace self.ileanFile) depTrace def Module.mkCTarget (modTarget : BuildTarget x) (self : Module) : FileTarget := Target.mk self.cFile <| modTarget.bindOpaqueSync fun _ => @@ -113,38 +121,58 @@ def recBuildExternalDynlibs (pkgs : Array Package) variable [MonadLiftT BuildM m] +/-- Possible artifacts of the `lean` command. -/ +inductive LeanArtifact +| leanBin | olean | ilean | c +deriving Inhabited, Repr, DecidableEq + /-- Recursively build a module and its (transitive, local) imports, -optionally outputting a `.c` file as well if `c` is set to `true`. +optionally outputting a `.c` file if the modules' is not lean-only or the +requested artifact is `c`. Returns an active target producing the requested +artifact. -/ -@[specialize] def Module.recBuildLean (mod : Module) (c : Bool) -: IndexT m ActiveOpaqueTarget := do +@[specialize] def Module.recBuildLean (mod : Module) (art : LeanArtifact) +: IndexT m (ActiveBuildTarget (if art = .leanBin then PUnit else FilePath)) := do have : MonadLift BuildM m := ⟨liftM⟩ + let leanOnly := mod.isLeanOnly ∧ art ≠ .c + + -- Compute and build dependencies let extraDepTarget ← mod.pkg.extraDep.recBuild let (imports, _) ← mod.imports.recBuild let (modTargets, pkgTargets, libDirs) ← recBuildPrecompileDynlibs mod.pkg imports - -- Note: Lean wants the external library symbols before module symbols + -- NOTE: Lean wants the external library symbols before module symbols let dynlibsTarget ← ActiveTarget.collectArray <| pkgTargets ++ modTargets - let importTarget ← - if c then - ActiveTarget.collectOpaqueArray - <| ← imports.mapM (·.c.recBuild) - else - ActiveTarget.collectOpaqueArray - <| ← imports.mapM (·.leanBin.recBuild) + let importTarget ← ActiveTarget.collectOpaqueArray + <| ← imports.mapM (·.leanBin.recBuild) let depTarget := Target.active <| ← extraDepTarget.mixOpaqueAsync <| ← dynlibsTarget.mixOpaqueAsync importTarget let dynlibs := dynlibsTarget.info.map (FilePath.mk s!"lib{·}.{sharedLibExt}") - let modTarget ← mod.soloTarget dynlibs libDirs.toList depTarget c |>.activate + + -- Build Module + let modTarget ← mod.soloTarget dynlibs libDirs.toList depTarget leanOnly |>.activate + + -- Save All Resulting Targets & Return Requested One store mod.leanBin.key modTarget - store mod.olean.key <| modTarget.withInfo mod.oleanFile - store mod.ilean.key <| modTarget.withInfo mod.ileanFile - if c then + let oleanTarget ← mod.mkOleanTarget (Target.active modTarget) |>.activate + store mod.olean.key <| oleanTarget + let ileanTarget ← mod.mkIleanTarget (Target.active modTarget) |>.activate + store mod.ilean.key <| ileanTarget + if h : leanOnly then + have : art ≠ .c := h.2 + return match art with + | .leanBin => modTarget + | .olean => oleanTarget + | .ilean => ileanTarget + else let cTarget ← mod.mkCTarget (Target.active modTarget) |>.activate store mod.c.key cTarget - return cTarget.withoutInfo - else - return modTarget + return match art with + | .leanBin => modTarget + | .olean => oleanTarget + | .ilean => ileanTarget + | .c => cTarget + /-- Recursively parse the Lean files of a module and its imports diff --git a/Lake/CLI/Build.lean b/Lake/CLI/Build.lean index ba755d0..b82796f 100644 --- a/Lake/CLI/Build.lean +++ b/Lake/CLI/Build.lean @@ -27,7 +27,7 @@ def parsePackageSpec (ws : Workspace) (spec : String) : Except CliError Package open Module in def resolveModuleTarget (ws : Workspace) (mod : Module) (facet : String) : Except CliError OpaqueTarget := if facet.isEmpty || facet == "bin" then - return mod.facetTarget binFacet + return mod.facetTarget leanBinFacet else if facet == "ilean" then return mod.facetTarget ileanFacet else if facet == "olean" then diff --git a/Lake/Config/ModuleFacetConfig.lean b/Lake/Config/ModuleFacetConfig.lean index 2f22a9e..48c12bf 100644 --- a/Lake/Config/ModuleFacetConfig.lean +++ b/Lake/Config/ModuleFacetConfig.lean @@ -23,7 +23,7 @@ structure ModuleFacetConfig where data_eq_target : ModuleData name = ActiveBuildTarget resultType instance : Inhabited ModuleFacetConfig := ⟨{ - name := &`lean.bin + name := Module.leanBinFacet resultType := PUnit build := default data_eq_target := eq_dynamic_type