fix: properly trace module imports

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
 

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

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

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

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

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

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

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