From 1e41c10c4c7752d41eff93c60031ebfd6f13d434 Mon Sep 17 00:00:00 2001
From: Mac Malone <mac@lean-fro.org>
Date: Mon, 24 Aug 2026 09:09:45 +0000
Subject: [PATCH 1/3] feat: lake: seperate `leanir` job

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 src/LeanIR.lean                          |   4 +
 src/lake/Lake/Build/Actions.lean         |  30 +--
 src/lake/Lake/Build/Facets.lean          |  24 +-
 src/lake/Lake/Build/Infos.lean           |   7 +
 src/lake/Lake/Build/Module.lean          | 304 ++++++++++++++++++-----
 src/lake/Lake/Build/ModuleArtifacts.lean |  11 +-
 src/lake/Lake/Config/Module.lean         |  10 +
 tests/lake/tests/noRelease/test.sh       |   2 +-
 8 files changed, 297 insertions(+), 95 deletions(-)

diff --git a/src/LeanIR.lean b/src/LeanIR.lean
index a95112b90e8b..b947239218fc 100644
--- a/src/LeanIR.lean
+++ b/src/LeanIR.lean
@@ -11,6 +11,7 @@ import all Lean.Util.Path
 import all Lean.Environment
 import Lean.Compiler.Options
 import Lean.Compiler.IR.CompilerM
+import Lean.Compiler.ModPkgExt
 
 import all Lean.Compiler.CSimpAttr
 import Lean.Compiler.LCNF.EmitC
@@ -90,6 +91,9 @@ public def main (args : List String) : IO UInt32 := do
     -- level exported because otherwise we would try to load the current module's `.ir`
     finalizeImport (leakEnv := true) (loadExts := false) (level := .exported) (loadIRSig := true) s imports opts
   let env := env.setMainModule modName
+  -- `finalizeImport` above runs with `loadExts := false`, so the package recorded by `lean` in
+  -- `modPkgExt` is not restored. Native symbols are prefixed by it, so take it from the setup.
+  let env := env.setModulePackage setup.package?
 
   let initExt {α β σ} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) : IO Environment := do
     let s := ext.toEnvExtension.getState env
diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index 88a4677a9f1f..9fe2e99cfb41 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/src/lake/Lake/Build/Actions.lean
@@ -26,6 +26,19 @@ open Lean hiding SearchPath
 
 namespace Lake
 
+public def compileLeanIR
+  (setupFile irFile cFile : FilePath)
+  (leanPath : SearchPath := [])
+  (leanir : FilePath := "leanir")
+: LogIO Unit := do
+  createParentDirs irFile
+  createParentDirs cFile
+  proc {
+    cmd := leanir.toString
+    args := #[setupFile.toString, irFile.toString, cFile.toString]
+    env := #[("LEAN_PATH", leanPath.toString)]
+  }
+
 public def compileLeanModule
   (leanFile relLeanFile : FilePath)
   (setup : ModuleSetup) (setupFile : FilePath)
@@ -33,7 +46,6 @@ public def compileLeanModule
   (leanArgs : Array String := #[])
   (leanPath : SearchPath := [])
   (lean : FilePath := "lean")
-  (leanir : FilePath := "leanir")
 : LogIO Unit := do
   let mut args := leanArgs.push leanFile.toString
   if let some oleanFile := arts.olean? then
@@ -91,22 +103,6 @@ public def compileLeanModule
     failure
   else if out.exitCode ≠ 0 || hasErrors then
     error s!"Lean exited with code {out.exitCode}"
-  if postponeCompile then
-    if let (some irFile, some cFile) := (arts.ir?, arts.c?) then
-      createParentDirs irFile
-      createParentDirs cFile
-      try
-        proc {
-          cmd := leanir.toString
-          args := #[setupFile.toString, irFile.toString, cFile.toString]
-          env := #[
-            ("LEAN_PATH", leanPath.toString)
-          ]
-        }
-      catch e =>
-        if let some oleanFile := arts.olean? then
-          removeFileIfExists oleanFile
-        throw e
 
 public def compileO
   (oFile srcFile : FilePath)
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index e758d6506c9c..12539283a568 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/src/lake/Lake/Build/Facets.lean
@@ -80,6 +80,10 @@ public structure ModuleImportInfo where
   allTransTrace : BuildTrace
   /-- Transitive import trace for an `import` of the module without the module system enabled. -/
   legacyTransTrace : BuildTrace
+  /-- The trace produced by mixing the `leanir` traces of `directArts` with their transitive imports. -/
+  irSigTrace : BuildTrace
+  /-- Transitive import trace for a `leanir` run over an importer of the module. -/
+  irSigTransTrace : BuildTrace
   deriving Inhabited
 
 /-- **For internal use only.** Information about the imports of this module. -/
@@ -93,8 +97,16 @@ public structure ModuleExportInfo where
   arts : ImportArtifacts
   /-- The trace of the module's public olean. -/
   artsTrace : BuildTrace
-  /-- The trace of the module's public olean and IR. -/
+  /-- Transitive import trace for an `import` of the module with the module system enabled. -/
+  transTrace : BuildTrace
+  deriving Inhabited
+
+/-- Information useful to importers of a module. Includes IR. -/
+public structure ModuleMetaExportInfo extends ModuleExportInfo where
+  /-- The trace of the module's public olean and IR (i.e., what a `meta import` needs). -/
   metaArtsTrace : BuildTrace
+  /-- The trace of the module's public olean and IR signature (i.e., what `leanir` needs). -/
+  irSigArtsTrace : BuildTrace
   /--
   Artifacts directly needed for an `import` of the module from a module without the module
   system enabled or `import all` of the module from a module with it enabled.
@@ -102,19 +114,22 @@ public structure ModuleExportInfo where
   allArts : ImportArtifacts
   /-- The trace produced by mixing the traces of `allArts`. -/
   allArtsTrace : BuildTrace
-  /-- Transitive import trace for an `import` of the module with the module system enabled. -/
-  transTrace : BuildTrace
   /-- Transitive import trace for a `meta import` of the module. -/
   metaTransTrace : BuildTrace
   /-- Transitive import trace for an `import all` of the module. -/
   allTransTrace : BuildTrace
   /-- Transitive import trace for an `import` of the module without the module system enabled. -/
   legacyTransTrace : BuildTrace
+  /-- Transitive import trace for a `leanir` run over an importer of the module. -/
+  irSigTransTrace : BuildTrace
   deriving Inhabited
 
 /-- **For internal use only.** Information useful to importers of this module. -/
 builtin_facet exportInfo : Module => ModuleExportInfo
 
+/-- **For internal use only.** Information useful to `meta` importers of this module. -/
+builtin_facet metaExportInfo : Module => ModuleMetaExportInfo
+
 /-- Artifacts directly needed for an `import` of this module with the module system enabled. -/
 builtin_facet importArts : Module => ImportArtifacts
 
@@ -132,6 +147,9 @@ Its trace just includes its dependencies.
 -/
 builtin_facet leanArts : Module => ModuleOutputArtifacts
 
+/-- The artifacts of a Lean module's code generation (e.g., `.ir.sig`, `.ir`, `.c`). -/
+builtin_facet irArts : Module => ModuleOutputArtifacts
+
 /-- A compressed archive (produced via `leantar`) of the module's build artifacts. -/
 builtin_facet ltar : Module => FilePath
 
diff --git a/src/lake/Lake/Build/Infos.lean b/src/lake/Lake/Build/Infos.lean
index cc9e9d546b7e..e95f7e82366c 100644
--- a/src/lake/Lake/Build/Infos.lean
+++ b/src/lake/Lake/Build/Infos.lean
@@ -83,6 +83,7 @@ builtin_facet imports : Module => Array Module
 /-- Dynamic information computed about a module before building. -/
 public structure ModulePreSetup where
   trace : BuildTrace
+  irSigTrace : BuildTrace
   srcMTime : MTime
   srcFile : FilePath
   isModule : Bool
@@ -181,6 +182,9 @@ namespace Module
 @[inherit_doc exportInfoFacet] public abbrev exportInfo (self : Module) :=
   self.facetCore exportInfoFacet
 
+@[inherit_doc metaExportInfoFacet] public abbrev metaExportInfo (self : Module) :=
+  self.facetCore metaExportInfoFacet
+
 @[inherit_doc importArtsFacet] public abbrev importArts (self : Module) :=
   self.facetCore importArtsFacet
 
@@ -190,6 +194,9 @@ namespace Module
 @[inherit_doc leanArtsFacet] public abbrev leanArts (self : Module) :=
   self.facetCore leanArtsFacet
 
+@[inherit_doc irArtsFacet] public abbrev irArts (self : Module) :=
+  self.facetCore irArtsFacet
+
 @[inherit_doc oleanFacet] public abbrev olean (self : Module) :=
   self.facetCore oleanFacet
 
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index b334824d652c..6e4a2d088784 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -10,6 +10,7 @@ public import Lake.Config.FacetConfig
 public import Lake.Build.Job.Monad
 public import Lake.Build.Infos
 import Lean.Elab.ParseImportsFast
+public import Lean.Compiler.Options
 import Lake.Util.Proc
 import Lake.Build.Job.Register
 import Lake.Build.Common
@@ -22,6 +23,26 @@ open System Lean
 
 namespace Lake
 
+/--
+Whether the module's code generation is deferred to a separate `leanir` step (the `irArts` facet)
+rather than performed by `lean` during elaboration.
+
+It is opt-in via `compiler.postponeCompile` and only meaningful under the module system.
+-/
+@[inline] def ModulePreSetup.postponeCompile (self : ModulePreSetup) : Bool :=
+  Compiler.compiler.postponeCompile.get self.leanOptions.toOptions
+
+/--
+Fetches the information importers of the module need, including its IR.
+
+Importers need the IR because the language server imports at the `.server` level, where every
+import's IR is loaded (see `Lean.importModulesCore`). When code generation is postponed, only
+`metaExportInfo` can report it.
+-/
+-- TODO: Do not always include IR
+@[inline] def Module.fetchExportInfo (self : Module) : FetchM (Job ModuleMetaExportInfo) :=
+  self.metaExportInfo.fetch
+
 /-! ## Facet Builds
 Build function definitions for a module's builtin facets.
 -/
@@ -275,7 +296,7 @@ where
       let metaVisited := if needsMeta then metaVisited.insert mod.name else metaVisited
       -- Widest level seen so far, never below an existing entry's (no demotion).
       let wantAll := allVisited.contains mod.name || existing?.any (·.oleanPrivate?.isSome)
-      let info ← (← mod.exportInfo.fetch).await
+      let info ← (← mod.fetchExportInfo).await
       let s := s.insert mod.name (if wantAll then info.allArts else info.arts)
       let input ← (← mod.input.fetch).await
       -- `import all`/`meta import` are transitive. Propagate both flags to children.
@@ -301,9 +322,11 @@ def ModuleImportInfo.nil (modName : Name) : ModuleImportInfo where
   metaTransTrace := .nil s!"{modName} transitive imports (meta)"
   allTransTrace := .nil s!"{modName} transitive imports (all)"
   legacyTransTrace := .nil s!"{modName} transitive imports (legacy)"
+  irSigTrace := .nil s!"imports (leanir)"
+  irSigTransTrace := .nil s!"{modName} transitive imports (leanir)"
 
-def ModuleExportInfo.disambiguationHash
-  (self : ModuleExportInfo) (nonModule : Bool) (imp : Import)
+def ModuleMetaExportInfo.disambiguationHash
+  (self : ModuleMetaExportInfo) (nonModule : Bool) (imp : Import)
 : Hash :=
   if nonModule then
     self.legacyTransTrace.hash.mix self.allArtsTrace.hash
@@ -316,7 +339,7 @@ def ModuleExportInfo.disambiguationHash
 
 def ModuleImportInfo.addImport
   (info : ModuleImportInfo) (nonModule : Bool)
-  (imp : Import) (expInfo : ModuleExportInfo)
+  (imp : Import) (expInfo : ModuleMetaExportInfo)
 : ModuleImportInfo :=
   let info :=
     if nonModule then
@@ -373,6 +396,42 @@ def ModuleImportInfo.addImport
       |>.mix expInfo.metaArtsTrace.withoutInputs
       |>.withoutInputs
   }
+  /-
+  `leanir` reads the `.ir.sig` of every import with data and the full `.ir` of those `import all`ed
+  (`importModulesCore` with `loadIRSig`, which also ignores `meta`). As at the root of that import
+  it has data for every direct import, `irSigTrace` mixes one in unconditionally, whereas
+  `irSigTransTrace` mixes in only the exported ones, as for `transTrace`.
+  -/
+  let info :=
+    if nonModule || imp.importAll then
+      {info with
+        irSigTrace := info.irSigTrace
+          |>.mix expInfo.allTransTrace
+          |>.mix expInfo.allArtsTrace.withoutInputs
+      }
+    else
+      {info with
+        irSigTrace := info.irSigTrace
+          |>.mix expInfo.irSigTransTrace
+          |>.mix expInfo.irSigArtsTrace.withoutInputs
+      }
+  let info :=
+    if !imp.isExported then
+      info
+    else if imp.importAll then
+      {info with
+        irSigTransTrace := info.irSigTransTrace
+          |>.mix expInfo.allTransTrace
+          |>.mix expInfo.allArtsTrace.withoutInputs
+          |>.withoutInputs
+      }
+    else
+      {info with
+        irSigTransTrace := info.irSigTransTrace
+          |>.mix expInfo.irSigTransTrace
+          |>.mix expInfo.irSigArtsTrace.withoutInputs
+          |>.withoutInputs
+      }
   if imp.isExported then
     if imp.isMeta then
       {info with
@@ -429,7 +488,7 @@ def fetchImportInfo
       --   logError s!"{fileName}: cannot `import all` \
       --     the module `{imp.module}` from the package `{mod.pkg.discriminant}`"
       --   return .error
-      let importJob ← mod.exportInfo.fetch
+      let importJob ← mod.fetchExportInfo
       return s.zipWith (sync := true) (·.addImport nonModule imp ·) importJob
     else
       -- Remark: We've decided to disable this check for now
@@ -450,7 +509,7 @@ def fetchImportInfo
       --   logError msg
       --   return .error
       let mods : Vector Module n := .mk mods rfl
-      let expInfosJob ← Job.collectVector <$> mods.mapM (·.exportInfo.fetch)
+      let expInfosJob ← Job.collectVector <$> mods.mapM (·.fetchExportInfo)
       s.bindM (sync := true) fun impInfo => do
       expInfosJob.mapM (sync := true) fun expInfos => do
         let expInfo := expInfos[0]
@@ -482,56 +541,80 @@ def noPrivateOLeanError :=
 def noIRError :=
   "No `.ir` generated. Ensure the module system is enabled."
 
+def noIRSigError :=
+  "No `.ir.sig` generated. Ensure the module system is enabled."
+
+def noCError :=
+  "No `.c` generated. This may be a bug in Lean or Lake."
+
 /-- Computes the import artifacts and transitive import trace of a module's imports. -/
 def Module.computeExportInfo (mod : Module) : FetchM (Job ModuleExportInfo) := do
   (← mod.leanArts.fetch).mapM (sync := true) fun arts => do
     let input ← (← mod.input.fetch).await
     let importInfo ← (← mod.importInfo.fetch).await
     let artsTrace := BuildTrace.nil s!"{mod.name}:importArts"
+    return {
+      srcTrace := input.trace
+      arts := ⟨#[#[arts.olean.path]]⟩
+      artsTrace := artsTrace.mix arts.olean.trace
+      transTrace := importInfo.transTrace
+    }
+
+/-- The `ModuleFacetConfig` for the builtin `exportInfoFacet`. -/
+public def Module.exportInfoFacetConfig : ModuleFacetConfig exportInfoFacet :=
+  mkFacetJobConfig computeExportInfo (buildable := false)
+
+/-- Like `computeExportInfo`, but includes IR produced by a postponed code generation. -/
+private def Module.computeMetaExportInfo (mod : Module) : FetchM (Job ModuleMetaExportInfo) := do
+  let irJob ← mod.irArts.fetch
+  let expInfoJob ← mod.exportInfo.fetch
+  irJob.bindM (sync := true) fun arts =>
+  expInfoJob.mapM (sync := true) fun info => do
+    let importInfo ← (← mod.importInfo.fetch).await
     let metaArtsTrace := BuildTrace.nil s!"{mod.name}:importArts (meta)"
+    let irSigArtsTrace := BuildTrace.nil s!"{mod.name}:importArts (leanir)"
     let allArtsTrace := BuildTrace.nil s!"{mod.name}:importAllArts"
-    let olean := arts.olean
-    if input.header.isModule then
+    if arts.isModule then
       let some oleanServer := arts.oleanServer?
         | error noServerOLeanError
+      let some oleanPrivate := arts.oleanPrivate?
+        | error noPrivateOLeanError
       let some irSig := arts.irSig?
-        | error noIRError
+        | error noIRSigError
       let some ir := arts.ir?
         | error noIRError
-      let some oleanPrivate := arts.oleanPrivate?
-        | error noPrivateOLeanError
-      return {
-        srcTrace := input.trace
+      return {info with
         -- NOTE: always includes `.server` and full `.ir` as this data is used by the server and we
         -- do not distinguish between it and cmdline build here (TODO: this is too dangerous!)
-        arts := .ofArrays #[#[olean.path, oleanServer.path], #[irSig.path, ir.path]]
-        artsTrace := artsTrace.mix olean.trace
-        metaArtsTrace := metaArtsTrace.mix olean.trace |>.mix irSig.trace |>.mix ir.trace
-        allArts := .ofArrays #[#[olean.path, oleanServer.path, oleanPrivate.path], #[irSig.path, ir.path]]
+        arts := .ofArrays #[#[arts.olean.path, oleanServer.path], #[irSig.path, ir.path]]
+        metaArtsTrace := metaArtsTrace.mix arts.olean.trace |>.mix irSig.trace |>.mix ir.trace
+        irSigArtsTrace := irSigArtsTrace.mix arts.olean.trace |>.mix irSig.trace
+        allArts := .ofArrays #[#[arts.olean.path, oleanServer.path, oleanPrivate.path], #[irSig.path, ir.path]]
         allArtsTrace := allArtsTrace.mix
-          olean.trace |>.mix oleanServer.trace |>.mix oleanPrivate.trace |>.mix irSig.trace |>.mix ir.trace
+          arts.olean.trace |>.mix oleanServer.trace |>.mix oleanPrivate.trace
+          |>.mix irSig.trace |>.mix ir.trace
         transTrace := importInfo.transTrace
         metaTransTrace := importInfo.metaTransTrace
         allTransTrace := importInfo.allTransTrace
         legacyTransTrace := importInfo.legacyTransTrace
+        irSigTransTrace := importInfo.irSigTransTrace
       }
     else
-      return {
-        srcTrace := input.trace
-        arts := ⟨#[#[olean.path]]⟩
-        artsTrace := artsTrace.mix olean.trace
-        metaArtsTrace := metaArtsTrace.mix olean.trace
-        allArts := ⟨#[#[olean.path]]⟩
-        allArtsTrace:= allArtsTrace.mix olean.trace
+      return {info with
+        metaArtsTrace := metaArtsTrace.mix arts.olean.trace
+        irSigArtsTrace := irSigArtsTrace.mix arts.olean.trace
+        allArts := ⟨#[#[arts.olean.path]]⟩
+        allArtsTrace:= allArtsTrace.mix arts.olean.trace
         transTrace := importInfo.transTrace
         metaTransTrace := importInfo.metaTransTrace
         allTransTrace := importInfo.allTransTrace
         legacyTransTrace := importInfo.legacyTransTrace
+        irSigTransTrace := importInfo.irSigTransTrace
       }
 
-/-- The `ModuleFacetConfig` for the builtin `exportInfoFacet`. -/
-public def Module.exportInfoFacetConfig : ModuleFacetConfig exportInfoFacet :=
-  mkFacetJobConfig computeExportInfo (buildable := false)
+/-- The `ModuleFacetConfig` for the builtin `metaExportInfoFacet`. -/
+public def Module.metaExportInfoFacetConfig : ModuleFacetConfig metaExportInfoFacet :=
+  mkFacetJobConfig computeMetaExportInfo (buildable := false)
 
 /-- The `ModuleFacetConfig` for the builtin `importArtsFacet`. -/
 public def Module.importArtsFacetConfig : ModuleFacetConfig importArtsFacet :=
@@ -542,7 +625,7 @@ public def Module.importArtsFacetConfig : ModuleFacetConfig importArtsFacet :=
 /-- The `ModuleFacetConfig` for the builtin `importAllArtsFacet`. -/
 public def Module.importAllArtsFacetConfig : ModuleFacetConfig importAllArtsFacet :=
   mkFacetJobConfig fun mod =>
-    return (← mod.exportInfo.fetch).mapOk (sync := true) fun i s =>
+    return (← mod.metaExportInfo.fetch).mapOk (sync := true) fun i s =>
       .ok i.arts {s with trace := i.allArtsTrace}
 
 /--
@@ -627,6 +710,7 @@ def Module.recFetchPreSetup (mod : Module) : FetchM (Job ModulePreSetup) := ensu
       isModule := input.header.isModule
       directImports := input.imports
       directImportArts := info.directArts
+      irSigTrace := info.irSigTrace
       dynlibs, plugins, leanOptions
     }
 where
@@ -721,7 +805,8 @@ public def Module.cacheOutputHashes (mod : Module) : IO PUnit := do
     cacheFileHash mod.irSigFile
   if (← mod.irFile.pathExists)  then
     cacheFileHash mod.irFile
-  cacheFileHash mod.cFile
+  if (← mod.cFile.pathExists) then
+    cacheFileHash mod.cFile
   if Lean.Internal.hasLLVMBackend () then
     cacheFileHash mod.bcFile
 
@@ -736,7 +821,7 @@ def ModuleOutputDescrs.resolve
     irSig? := ← descrs.irSig?.mapM resolve
     ir? := ← descrs.ir?.mapM resolve
     ilean := ← resolve descrs.ilean
-    c := ← resolve descrs.c
+    c? := ← descrs.c?.mapM resolve
     ltar? := ← descrs.ltar?.mapM resolve
   }
   if Lean.Internal.hasLLVMBackend () then
@@ -784,17 +869,17 @@ instance : ResolveOutputs ModuleOutputs := ⟨resolveModuleOutputs⟩
 
 /-- Save module build artifacts to the local Lake cache. -/
 def Module.cacheOutputArtifacts
-  (mod : Module)  (isModule : Bool) (useLocalFile : Bool)
+  (mod : Module)  (isModule : Bool) (useLocalFile : Bool) (postponesCompile : Bool)
 : JobM ModuleOutputArtifacts := do
   return {
     isModule
     olean := ← cache mod.oleanFile "olean"
     oleanServer? := ← cacheIf? isModule mod.oleanServerFile "olean.server"
     oleanPrivate? := ← cacheIf? isModule mod.oleanPrivateFile "olean.private"
-    irSig? := ← cacheIf? isModule mod.irSigFile "ir.sig"
-    ir? := ← cacheIf? isModule mod.irFile "ir"
+    irSig? := ← cacheIf? (isModule && !postponesCompile) mod.irSigFile "ir.sig"
+    ir? := ← cacheIf? (isModule && !postponesCompile) mod.irFile "ir"
     ilean := ← cache mod.ileanFile "ilean"
-    c := ← cache mod.cFile "c"
+    c? := ← cacheIf? (!(isModule && postponesCompile)) mod.cFile "c"
     bc? := ← cacheIf? (Lean.Internal.hasLLVMBackend ()) mod.bcFile "bc"
     ltar? := ← cacheIf? (← mod.ltarFile.pathExists) mod.ltarFile "ltar"
   }
@@ -823,46 +908,59 @@ def Module.restoreAllArtifacts (mod : Module) (cached : ModuleOutputArtifacts) :
     ilean := ← restoreArtifact mod.ileanFile cached.ilean
     irSig? := ← restoreSome mod.irSigFile cached.irSig?
     ir? := ← restoreSome mod.irFile cached.ir?
-    c := ← restoreArtifact mod.cFile cached.c
+    c? := ← restoreSome mod.cFile cached.c?
     bc? := ← restoreSome mod.bcFile cached.bc?
     ltar? := ← restoreSome mod.ltarFile cached.ltar?
   }
 where
   @[inline] restoreSome file art? := art?.mapM (restoreArtifact file ·)
 
-public def Module.checkArtifactsExist (self : Module) (isModule : Bool) : BaseIO Bool := do
+public def Module.checkArtifactsExist
+  (self : Module) (isModule : Bool) (skipIR := isModule && self.postponeCompile)
+: BaseIO Bool := do
   unless (← self.oleanFile.pathExists) do return false
   unless (← self.ileanFile.pathExists) do return false
-  unless (← self.cFile.pathExists) do return false
   if Lean.Internal.hasLLVMBackend () then
     unless (← self.bcFile.pathExists) do return false
   if isModule then
     unless (← self.oleanServerFile.pathExists) do return false
     unless (← self.oleanPrivateFile.pathExists) do return false
-    unless (← self.irSigFile.pathExists) do return false
-    unless (← self.irFile.pathExists) do return false
+  -- When code generation is postponed, `irArts` produces the IR and `.c` on its own schedule.
+  unless skipIR do
+    unless (← self.cFile.pathExists) do return false
+    if isModule then
+      unless (← self.irSigFile.pathExists) do return false
+      unless (← self.irFile.pathExists) do return false
   return true
 
-public protected def Module.checkExists (self : Module) (isModule : Bool) : BaseIO Bool := do
-  self.ltarFile.pathExists <||> self.checkArtifactsExist isModule
+public protected def Module.checkExists
+  (self : Module) (isModule : Bool) (skipIR := isModule && self.postponeCompile)
+: BaseIO Bool := do
+  self.ltarFile.pathExists <||> self.checkArtifactsExist isModule skipIR
 
 @[deprecated Module.checkExists +typeChanged (since := "2025-03-04")]
 public instance : CheckExists Module := ⟨Module.checkExists (isModule := false)⟩
 
-public protected def Module.getMTime (self : Module) (isModule : Bool) : IO MTime := do
+public protected def Module.getMTime
+  (self : Module) (isModule : Bool) (skipIR := isModule && self.postponeCompile)
+: IO MTime := do
   try
     let mut mtime :=
       (← getMTime self.oleanFile)
       |> max (← getMTime self.ileanFile)
-      |> max (← getMTime self.cFile)
     if Lean.Internal.hasLLVMBackend () then
       mtime := max mtime (← getMTime self.bcFile)
     if isModule then
       mtime := mtime
       |> max (← getMTime self.oleanServerFile)
       |> max (← getMTime self.oleanPrivateFile)
-      |> max (← getMTime self.irSigFile)
-      |> max (← getMTime self.irFile)
+    -- When code generation is postponed, `irArts` produces the IR and `.c` on its own schedule.
+    unless skipIR do
+      mtime := max mtime (← getMTime self.cFile)
+      if isModule then
+        mtime := mtime
+        |> max (← getMTime self.irSigFile)
+        |> max (← getMTime self.irFile)
     return mtime
   catch e =>
     try getMTime self.ltarFile catch
@@ -880,7 +978,7 @@ def ModuleOutputArtifacts.setMTime (self : ModuleOutputArtifacts) (mtime : MTime
     ilean := {self.ilean with mtime}
     irSig? := self.irSig?.map ({· with mtime})
     ir? := self.ir?.map ({· with mtime})
-    c := {self.c with mtime}
+    c? := self.c?.map ({· with mtime})
     bc? := self.bc?.map ({· with mtime})
   }
 
@@ -895,16 +993,29 @@ def Module.mkArtifacts (mod : Module) (srcFile : FilePath) (isModule : Bool) : M
   c? := mod.cFile
   bc? := if Lean.Internal.hasLLVMBackend () then some mod.bcFile else none
 
-def Module.computeArtifacts (mod : Module) (isModule : Bool) : FetchM ModuleOutputArtifacts :=
+def Module.computeIRArtifacts (mod : Module) (elabArts : ModuleOutputArtifacts)  : FetchM ModuleOutputArtifacts :=
+  return {elabArts with
+    irSig? := some <| ← compute mod.irSigFile "ir.sig"
+    ir? := some <| ← compute mod.irFile "ir"
+    c? := some <| ← compute mod.cFile "c"
+  }
+where
+  @[inline] compute file ext := do
+    -- Note: Lean produces LF-only line endings for `.c` and `.ilean`, so no normalization.
+    computeArtifact file ext (text := false)
+
+def Module.computeArtifacts
+  (mod : Module) (isModule : Bool) (skipIR : Bool)
+: FetchM ModuleOutputArtifacts :=
   return {
     isModule
     olean := ← compute mod.oleanFile "olean"
     oleanServer? := ← computeIf isModule mod.oleanServerFile "olean.server"
     oleanPrivate? := ← computeIf isModule mod.oleanPrivateFile "olean.private"
     ilean := ← compute mod.ileanFile "ilean"
-    irSig? := ← computeIf isModule mod.irSigFile "ir.sig"
-    ir? := ← computeIf isModule mod.irFile "ir"
-    c := ← compute mod.cFile "c"
+    irSig? := ← computeIf (isModule && !skipIR) mod.irSigFile "ir.sig"
+    ir? := ← computeIf (isModule && !skipIR) mod.irFile "ir"
+    c? := ← computeIf (!(isModule && skipIR)) mod.cFile "c"
     bc? := ← computeIf (Lean.Internal.hasLLVMBackend ()) mod.bcFile "bc"
   }
 where
@@ -916,9 +1027,11 @@ where
 
 instance : ToOutputJson ModuleOutputArtifacts := ⟨(toJson ·.descrs)⟩
 
-def Module.packLtar (self : Module) (arts : ModuleOutputArtifacts) : JobM Artifact := do
+def Module.packLtar
+  (self : Module) (arts : ModuleOutputArtifacts)
+: JobM Artifact := do
   let arts ← id do
-    if (← self.checkArtifactsExist arts.isModule) then
+    if (← self.checkArtifactsExist arts.isModule arts.c?.isNone) then
       return arts
     else self.restoreAllArtifacts arts
   let args ← id do
@@ -944,7 +1057,8 @@ def Module.packLtar (self : Module) (arts : ModuleOutputArtifacts) : JobM Artifa
       args := addArt args "0" art
     if let some art := arts.ir? then
       args := addArt args "0" art
-    args := addArt args "1" arts.c
+    if let some art := arts.c? then
+      args := addArt args "1" art
     if Lean.Internal.hasLLVMBackend () then
       let some art := arts.bc?
         | error "LLVM backend enabled but module outputs lack bitcode"
@@ -996,9 +1110,9 @@ def Module.buildLean
   let arts := mod.mkArtifacts presetup.srcFile presetup.isModule
   mod.clearOutputArtifacts
   compileLeanModule presetup.srcFile relSrcFile setup mod.setupFile arts args
-    (← getLeanPath) (← getLean) (← getLeanir)
+    (← getLeanPath) (← getLean)
   mod.clearOutputHashes
-  mod.computeArtifacts setup.isModule
+  mod.computeArtifacts setup.isModule presetup.postponeCompile
 
 /--
 Recursively build a Lean module.
@@ -1038,7 +1152,7 @@ where
         -- end up in the build directory and, if writable, the cache
         let arts ← mod.restoreAllArtifacts {arts with ltar? := some ltar}
         if (← mod.pkg.isArtifactCacheWritable) then
-          let arts ← mod.cacheOutputArtifacts presetup.isModule restoreAll
+          let arts ← mod.cacheOutputArtifacts presetup.isModule restoreAll presetup.postponeCompile
           -- Note: Cache service metadata is not preserved on an output update because it would
           -- result in downloading module outputs that are not available on the remote.
           (← getLakeCache).writeOutputs mod.pkg.cacheScope inputHash arts.descrs (overwrite := true)
@@ -1059,8 +1173,8 @@ where
       return .inl arts
   fetchCore (presetup : ModulePreSetup) : JobM ModuleOutputArtifacts := do
     let depTrace ← getTrace
-    have : GetMTime Module := ⟨Module.getMTime (isModule := presetup.isModule)⟩
-    have : CheckExists Module := ⟨Module.checkExists (isModule := presetup.isModule)⟩
+    have : GetMTime Module := ⟨(·.getMTime presetup.isModule presetup.postponeCompile)⟩
+    have : CheckExists Module := ⟨(·.checkExists presetup.isModule presetup.postponeCompile)⟩
     let savedTrace ← readTraceFile mod.traceFile
     if (← mod.pkg.isArtifactCacheWritable) then
       let restore ← mod.pkg.restoreAllArtifacts
@@ -1070,7 +1184,7 @@ where
       | .inr savedTrace =>
         let status ← savedTrace.replayIfUpToDate' (oldTrace := presetup.srcMTime) mod depTrace
         if status.isUpToDate then
-          unless (← mod.checkArtifactsExist presetup.isModule) do
+          unless (← mod.checkArtifactsExist presetup.isModule presetup.postponeCompile) do
             -- Restoring from the archive stamps the trace with the current input
             -- hash, so only do it on a verified hash match; an mtime-only match
             -- leaves the hash unconfirmed, so rebuild instead.
@@ -1081,22 +1195,22 @@ where
         else
           discard <| mod.buildLean presetup
         if status.isCacheable then
-          let arts ← mod.cacheOutputArtifacts presetup.isModule restore
+          let arts ← mod.cacheOutputArtifacts presetup.isModule restore presetup.postponeCompile
           (← getLakeCache).writeOutputs mod.pkg.cacheScope depTrace.hash arts.descrs
           return arts
         else
-          mod.computeArtifacts presetup.isModule
+          mod.computeArtifacts presetup.isModule presetup.postponeCompile
     else
       let status ← savedTrace.replayIfUpToDate' (oldTrace := presetup.srcMTime) mod depTrace
       if status.isUpToDate then
-        unless (← mod.checkArtifactsExist presetup.isModule) do
+        unless (← mod.checkArtifactsExist presetup.isModule presetup.postponeCompile) do
           -- As above: restore only on a verified hash match; an mtime-only match
           -- rebuilds instead.
           if status == .hashUpToDate then
             mod.unpackLtar mod.ltarFile depTrace.hash
           else
             discard <| mod.buildLean presetup
-        mod.computeArtifacts presetup.isModule
+        mod.computeArtifacts presetup.isModule presetup.postponeCompile
       else
         if (← mod.pkg.isArtifactCacheReadable) then
           match (← fetchFromCache? presetup savedTrace true) with
@@ -1104,7 +1218,7 @@ where
               return arts
           | .inr savedTrace =>
             if (← savedTrace.replayIfUpToDate (oldTrace := presetup.srcMTime) mod depTrace) then
-              mod.computeArtifacts presetup.isModule
+              mod.computeArtifacts presetup.isModule presetup.postponeCompile
             else
               mod.buildLean presetup
         else
@@ -1181,19 +1295,69 @@ public def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
       addTrace art.trace
       return art.path
 
+/--
+Recursively fetch the module's code generation artifacts.
+
+Unless code generation was postponed, elaboration already produced them. Otherwise, `leanir` runs
+once elaboration (`leanArts`) has produced the `.olean`.
+-/
+private def Module.recBuildIRArts (mod : Module) : FetchM (Job ModuleOutputArtifacts) := do
+  withRegisterJob s!"{mod.name}:irArts" do
+  let elabJob ← mod.leanArts.fetch
+  elabJob.mapM (sync := true) fun elabArts => do
+    unless elabArts.c?.isNone do
+      return elabArts
+    -- Already complete because `elabArts` waits on it
+    let presetup ← (← mod.presetup.fetch).await
+    let depTrace := BuildTrace.nil s!"{mod.name} (leanir)"
+      |>.mix (← importAllTrace elabArts) |>.mix presetup.irSigTrace
+    buildUnlessUpToDate (oldTrace := presetup.srcMTime) mod.irFile depTrace mod.irTraceFile do
+      createParentDirs mod.irSetupFile
+      let irSetup ← mkModuleSetup mod presetup
+      IO.FS.writeFile mod.irSetupFile (toJson irSetup).pretty
+      compileLeanIR mod.irSetupFile mod.irFile mod.cFile (← getLeanPath) (← getLeanir)
+    mod.computeIRArtifacts elabArts
+where
+  importAllTrace arts := do
+    let allArtsTrace := BuildTrace.nil s!"{mod.name}:importAllArts"
+    if arts.isModule then
+      let some oleanServer := arts.oleanServer?
+        | error noServerOLeanError
+      let some oleanPrivate := arts.oleanPrivate?
+        | error noPrivateOLeanError
+      return allArtsTrace.mix
+          arts.olean.trace |>.mix oleanServer.trace |>.mix oleanPrivate.trace
+    else
+      return allArtsTrace.mix arts.olean.trace
+
+/-- The `ModuleFacetConfig` for the builtin `irArtsFacet`. -/
+public def Module.irArtsFacetConfig : ModuleFacetConfig irArtsFacet :=
+  mkFacetJobConfig recBuildIRArts
+
+@[inline] def Module.fetchIRArtCore
+  (facet : String) (f : ModuleOutputArtifacts → Option Artifact) (errMsg : String) (mod : Module)
+: FetchM (Job FilePath) := do
+  (← mod.irArts.fetch).mapM (sync := true) fun arts => do
+    let some art := f arts
+      | error errMsg
+    newTrace s!"{mod.name.toString}:{facet}"
+    addTrace art.trace
+    return art.path
+
 /-- The `ModuleFacetConfig` for the builtin `irSigFacet`. -/
 public def Module.irSigFacetConfig : ModuleFacetConfig irSigFacet :=
-  mkFacetJobConfig <| fetchOLeanCore "ir.sig" (·.irSig?) noIRError
+  mkFacetJobConfig <| fetchIRArtCore "ir.sig" (·.irSig?) noIRError
 
 /-- The `ModuleFacetConfig` for the builtin `irFacet`. -/
 public def Module.irFacetConfig : ModuleFacetConfig irFacet :=
-  mkFacetJobConfig <| fetchOLeanCore "ir" (·.ir?) noIRError
+  mkFacetJobConfig <| fetchIRArtCore "ir" (·.ir?) noIRError
 
 /-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
 public def Module.cFacetConfig : ModuleFacetConfig cFacet :=
   mkFacetJobConfig fun mod => do
-    (← mod.leanArts.fetch).mapM (sync := true) fun arts => do
-      let art := arts.c
+    (← mod.irArts.fetch).mapM (sync := true) fun arts => do
+      let some art := arts.c?
+        | error noCError
       /-
       Avoid recompiling unchanged C files.
       C files are assumed to only incorporate their own content
@@ -1392,9 +1556,11 @@ public def Module.initFacetConfigs : DNameMap ModuleFacetConfig :=
   |>.insert depHashFacet depHashFacetConfig
   |>.insert depsFacet depsFacetConfig
   |>.insert leanArtsFacet leanArtsFacetConfig
+  |>.insert irArtsFacet irArtsFacetConfig
   |>.insert importArtsFacet importArtsFacetConfig
   |>.insert importAllArtsFacet importAllArtsFacetConfig
   |>.insert exportInfoFacet exportInfoFacetConfig
+  |>.insert metaExportInfoFacet metaExportInfoFacetConfig
   |>.insert ltarFacet ltarFacetConfig
   |>.insert oleanFacet oleanFacetConfig
   |>.insert oleanServerFacet oleanServerFacetConfig
diff --git a/src/lake/Lake/Build/ModuleArtifacts.lean b/src/lake/Lake/Build/ModuleArtifacts.lean
index 023c77ff5189..c6814e21718b 100644
--- a/src/lake/Lake/Build/ModuleArtifacts.lean
+++ b/src/lake/Lake/Build/ModuleArtifacts.lean
@@ -22,7 +22,7 @@ public structure ModuleOutputDescrs where
   ilean : ArtifactDescr
   irSig? : Option ArtifactDescr := none
   ir? : Option ArtifactDescr := none
-  c : ArtifactDescr
+  c? : Option ArtifactDescr := none
   bc? : Option ArtifactDescr := none
   ltar? : Option ArtifactDescr := none
 
@@ -43,7 +43,8 @@ public protected def ModuleOutputDescrs.toJson (self : ModuleOutputDescrs) : Jso
     obj := obj.insert "rs" irSig
   if let some ir := self.ir? then
     obj := obj.insert "r" ir
-  obj := obj.insert "c" self.c
+  if let some c := self.c? then
+    obj := obj.insert "c" c
   if let some bc := self.bc? then
     obj := obj.insert "b" bc
   if let some ltar := self.ltar? then
@@ -65,7 +66,7 @@ public protected def ModuleOutputDescrs.fromJson? (val : Json) : Except String M
     ilean := ← obj.get "i"
     irSig? := ← obj.get? "rs"
     ir? := ← obj.get? "r"
-    c := ← obj.get "c"
+    c? := ← obj.get? "c"
     bc? := ← obj.get? "b"
     ltar? := ← obj.get? "l"
   }
@@ -81,7 +82,7 @@ public structure ModuleOutputArtifacts where
   ilean : Artifact
   irSig? : Option Artifact := none
   ir? : Option Artifact := none
-  c : Artifact
+  c? : Option Artifact := none
   bc? : Option Artifact := none
   ltar? : Option Artifact := none
 
@@ -94,6 +95,6 @@ public def ModuleOutputArtifacts.descrs (arts : ModuleOutputArtifacts) : ModuleO
   ilean := arts.ilean.descr
   irSig? := arts.irSig?.map (·.descr)
   ir? := arts.ir?.map (·.descr)
-  c := arts.c.descr
+  c? := arts.c?.map (·.descr)
   bc? := arts.bc?.map (·.descr)
   ltar? := arts.ltar?.map (·.descr)
diff --git a/src/lake/Lake/Config/Module.lean b/src/lake/Lake/Config/Module.lean
index 44b2427b486b..11dc2fb773f9 100644
--- a/src/lake/Lake/Config/Module.lean
+++ b/src/lake/Lake/Config/Module.lean
@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lake.Config.LeanLib
+public import Lean.Compiler.Options
 
 namespace Lake
 open Lean System
@@ -119,6 +120,9 @@ public abbrev pkg (self : Module) : Package :=
 @[inline] public def traceFile (self : Module) : FilePath :=
   self.leanLibPath "trace"
 
+@[inline] public def irTraceFile (self : Module) : FilePath :=
+  self.leanLibPath "ir.trace"
+
 @[inline] public def irPath (ext : String) (self : Module) : FilePath :=
   self.filePath self.pkg.irDir ext
 
@@ -128,6 +132,9 @@ public abbrev pkg (self : Module) : Package :=
 @[inline] public def setupFile (self : Module) : FilePath :=
   self.irPath "setup.json"
 
+@[inline] public def irSetupFile (self : Module) : FilePath :=
+  self.irPath "irsetup.json"
+
 @[inline] public def cFile (self : Module) : FilePath :=
   self.irPath "c"
 
@@ -191,6 +198,9 @@ public def dynlibSuffix := "-1"
 @[inline] public def leanOptions (self : Module) : LeanOptions :=
   self.lib.leanOptions
 
+@[inline] public def postponeCompile (self : Module) : Bool :=
+  Compiler.compiler.postponeCompile.get self.leanOptions.toOptions
+
 @[inline] public def leanArgs (self : Module) : Array String :=
   self.lib.leanArgs
 
diff --git a/tests/lake/tests/noRelease/test.sh b/tests/lake/tests/noRelease/test.sh
index 5643c25d4a49..bc864b4fdf76 100755
--- a/tests/lake/tests/noRelease/test.sh
+++ b/tests/lake/tests/noRelease/test.sh
@@ -97,7 +97,7 @@ EOF
 # Test that releases do not contaminate downstream jobs
 echo "# TEST: Downstream job contamination"
 test_out_diff <(cat << 'EOF'
-Build completed successfully (5 jobs).
+Build completed successfully (6 jobs).
 EOF
 ) build Test
 

From d58f43f4bf0ca8348500281b729d9553a20d4b6a Mon Sep 17 00:00:00 2001
From: Mac Malone <mac@lean-fro.org>
Date: Mon, 24 Aug 2026 09:10:41 +0000
Subject: [PATCH 2/3] test: postpone compile

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 tests/lake/tests/moduleCodegen/Eval.lean     |  5 ++
 tests/lake/tests/moduleCodegen/Main.lean     |  5 ++
 tests/lake/tests/moduleCodegen/Test.lean     |  3 +
 tests/lake/tests/moduleCodegen/Test/A.lean   |  7 +++
 tests/lake/tests/moduleCodegen/Test/B.lean   |  5 ++
 tests/lake/tests/moduleCodegen/Test/C.lean   |  5 ++
 tests/lake/tests/moduleCodegen/clean.sh      |  3 +
 tests/lake/tests/moduleCodegen/lakefile.toml | 13 +++++
 tests/lake/tests/moduleCodegen/test.sh       | 60 ++++++++++++++++++++
 9 files changed, 106 insertions(+)
 create mode 100644 tests/lake/tests/moduleCodegen/Eval.lean
 create mode 100644 tests/lake/tests/moduleCodegen/Main.lean
 create mode 100644 tests/lake/tests/moduleCodegen/Test.lean
 create mode 100644 tests/lake/tests/moduleCodegen/Test/A.lean
 create mode 100644 tests/lake/tests/moduleCodegen/Test/B.lean
 create mode 100644 tests/lake/tests/moduleCodegen/Test/C.lean
 create mode 100755 tests/lake/tests/moduleCodegen/clean.sh
 create mode 100644 tests/lake/tests/moduleCodegen/lakefile.toml
 create mode 100755 tests/lake/tests/moduleCodegen/test.sh

diff --git a/tests/lake/tests/moduleCodegen/Eval.lean b/tests/lake/tests/moduleCodegen/Eval.lean
new file mode 100644
index 000000000000..309ab054a2f0
--- /dev/null
+++ b/tests/lake/tests/moduleCodegen/Eval.lean
@@ -0,0 +1,5 @@
+module
+
+import Test.A
+
+#eval twice 21
diff --git a/tests/lake/tests/moduleCodegen/Main.lean b/tests/lake/tests/moduleCodegen/Main.lean
new file mode 100644
index 000000000000..c4094c88a85c
--- /dev/null
+++ b/tests/lake/tests/moduleCodegen/Main.lean
@@ -0,0 +1,5 @@
+module
+
+import Test.C
+
+public def main : IO Unit := IO.println (viaImportAll 20)
diff --git a/tests/lake/tests/moduleCodegen/Test.lean b/tests/lake/tests/moduleCodegen/Test.lean
new file mode 100644
index 000000000000..4dc337d8e799
--- /dev/null
+++ b/tests/lake/tests/moduleCodegen/Test.lean
@@ -0,0 +1,3 @@
+module
+
+public import Test.C
diff --git a/tests/lake/tests/moduleCodegen/Test/A.lean b/tests/lake/tests/moduleCodegen/Test/A.lean
new file mode 100644
index 000000000000..0dd4cf664c84
--- /dev/null
+++ b/tests/lake/tests/moduleCodegen/Test/A.lean
@@ -0,0 +1,7 @@
+module
+
+private def offset : Nat := 1
+
+@[inline] public def addOffset (n : Nat) : Nat := n + offset
+
+public def twice (n : Nat) : Nat := n + n
diff --git a/tests/lake/tests/moduleCodegen/Test/B.lean b/tests/lake/tests/moduleCodegen/Test/B.lean
new file mode 100644
index 000000000000..f74140548556
--- /dev/null
+++ b/tests/lake/tests/moduleCodegen/Test/B.lean
@@ -0,0 +1,5 @@
+module
+
+import Test.A
+
+public def viaImport (n : Nat) : Nat := addOffset (twice n)
diff --git a/tests/lake/tests/moduleCodegen/Test/C.lean b/tests/lake/tests/moduleCodegen/Test/C.lean
new file mode 100644
index 000000000000..6f92393fed00
--- /dev/null
+++ b/tests/lake/tests/moduleCodegen/Test/C.lean
@@ -0,0 +1,5 @@
+module
+
+import all Test.B
+
+public def viaImportAll (n : Nat) : Nat := viaImport n + 1
diff --git a/tests/lake/tests/moduleCodegen/clean.sh b/tests/lake/tests/moduleCodegen/clean.sh
new file mode 100755
index 000000000000..3f789d9f7ba2
--- /dev/null
+++ b/tests/lake/tests/moduleCodegen/clean.sh
@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+rm -rf work
+rm -f produced.out
diff --git a/tests/lake/tests/moduleCodegen/lakefile.toml b/tests/lake/tests/moduleCodegen/lakefile.toml
new file mode 100644
index 000000000000..2942887d25f6
--- /dev/null
+++ b/tests/lake/tests/moduleCodegen/lakefile.toml
@@ -0,0 +1,13 @@
+name = "codegen"
+defaultTargets = ["codegen"]
+
+[leanOptions]
+experimental.module = true
+compiler.postponeCompile = true
+
+[[lean_lib]]
+name = "Test"
+
+[[lean_exe]]
+name = "codegen"
+root = "Main"
diff --git a/tests/lake/tests/moduleCodegen/test.sh b/tests/lake/tests/moduleCodegen/test.sh
new file mode 100755
index 000000000000..d1f69d9e4e05
--- /dev/null
+++ b/tests/lake/tests/moduleCodegen/test.sh
@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+# ---
+# This test covers `compiler.postponeCompile`, under which Lake defers a module system module's
+# code generation to a separate `leanir` step producing its `.ir.sig`, `.ir`, and `.c`.
+# ---
+
+# The rebuild tests below edit the sources, so work on a copy
+copy_to_work lakefile.toml Main.lean Test.lean Test Eval.lean
+
+# Elaboration alone does not generate code
+test_run build Test.A
+test_cmd_fails test -f .lake/build/ir/Test/A.c
+
+# Each module's code generation is a job of its own
+echo "# TEST: code generation"
+test_out "Built Test.A:irArts" build Test.A:c -v
+test_cmd test -f .lake/build/lib/lean/Test/A.ir.sig
+test_cmd test -f .lake/build/lib/lean/Test/A.ir
+test_out "Built Test.B:irArts" build Test.B:c -v
+test_run build Test.C:c
+
+# An import's IR must be provided even for a plain `import`, as the language server loads it
+test_cmd grep -F 'Test/A.ir"' .lake/build/ir/Test/B.setup.json
+test_cmd grep -F 'Test/A.ir"' .lake/build/ir/Test/B.irsetup.json
+
+# The server allows `#eval` on a plainly imported definition, so it must be able to run it
+echo "# TEST: server eval across a plain import"
+echo '$' lake setup-file Eval.lean
+"$LAKE" setup-file Eval.lean > eval.setup.json
+test_cmd_eq 42 lean --setup eval.setup.json -DElab.inServer=true Eval.lean
+
+# The generated code links and runs
+echo "# TEST: link and run"
+test_run build codegen
+test_cmd_eq 42 ./.lake/build/bin/codegen
+
+# ---
+# Tests that `leanir` is only rerun when needed
+# ---
+
+test_run build Test.A:c Test.B:c Test.C:c --no-build
+
+# A non-inlinable definition's body is part of the module's IR, but not of its `.ir.sig`
+echo "# TEST: irArts on a value edit"
+test_cmd sed_i 's/n + n/n + n + 0/' Test/A.lean
+test_out "Built Test.A:irArts" build Test.A:c -v
+# importers read only the `.ir.sig`, so their own IR is unaffected
+test_run build Test.B:c Test.C:c --no-build
+
+# A new public definition changes the `.ir.sig` as well
+echo "# TEST: irArts on an interface edit"
+test_run build Test.A:c Test.B:c Test.C:c
+test_cmd sed_i 's/^private def offset/public def extra : Nat := 7\nprivate def offset/' Test/A.lean
+test_out "Built Test.A:irArts" build Test.A:c -v
+test_out "Built Test.B:irArts" build Test.B:c -v
+

From 14bc481ec13277a82c9f2585213c9208dd782b79 Mon Sep 17 00:00:00 2001
From: Mac Malone <mac@lean-fro.org>
Date: Sat, 29 Aug 2026 00:43:19 +0000
Subject: [PATCH 3/3] chore: touchups

---
 src/LeanIR.lean                        |   4 +-
 src/lake/Lake/Build/Module.lean        | 129 ++++++++++---------------
 tests/lake/tests/moduleCodegen/test.sh |  14 ++-
 3 files changed, 60 insertions(+), 87 deletions(-)

diff --git a/src/LeanIR.lean b/src/LeanIR.lean
index b947239218fc..ccc78e5cae54 100644
--- a/src/LeanIR.lean
+++ b/src/LeanIR.lean
@@ -91,8 +91,8 @@ public def main (args : List String) : IO UInt32 := do
     -- level exported because otherwise we would try to load the current module's `.ir`
     finalizeImport (leakEnv := true) (loadExts := false) (level := .exported) (loadIRSig := true) s imports opts
   let env := env.setMainModule modName
-  -- `finalizeImport` above runs with `loadExts := false`, so the package recorded by `lean` in
-  -- `modPkgExt` is not restored. Native symbols are prefixed by it, so take it from the setup.
+  -- As the environment imports the module to compile, it does not inherit its package.
+  -- Take it from the setup.
   let env := env.setModulePackage setup.package?
 
   let initExt {α β σ} [Inhabited σ] (ext : PersistentEnvExtension α β σ) (env : Environment) : IO Environment := do
diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 6e4a2d088784..0404ae2b0c87 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/src/lake/Lake/Build/Module.lean
@@ -10,7 +10,6 @@ public import Lake.Config.FacetConfig
 public import Lake.Build.Job.Monad
 public import Lake.Build.Infos
 import Lean.Elab.ParseImportsFast
-public import Lean.Compiler.Options
 import Lake.Util.Proc
 import Lake.Build.Job.Register
 import Lake.Build.Common
@@ -358,95 +357,71 @@ def ModuleImportInfo.addImport
           {info with directArts := info.directArts.insert imp.module expInfo.arts}
         else
           info
-      if imp.isMeta then
-        {info with trace := info.trace.mix expInfo.metaTransTrace |>.mix expInfo.metaArtsTrace.withoutInputs}
-      else
-        {info with trace := info.trace.mix expInfo.transTrace |>.mix expInfo.artsTrace.withoutInputs}
+      {info with trace :=
+        if imp.isMeta then
+          info.trace.mix expInfo.metaTransTrace |>.mix expInfo.metaArtsTrace.withoutInputs
+        else
+          info.trace.mix expInfo.transTrace |>.mix expInfo.artsTrace.withoutInputs
+      }
   let info := {info with
     legacyTransTrace := info.legacyTransTrace
-      |>.mix expInfo.legacyTransTrace
-      |>.mix expInfo.allArtsTrace.withoutInputs
-      |>.withoutInputs
+    |>.mix expInfo.legacyTransTrace
+    |>.mix expInfo.allArtsTrace.withoutInputs
+    |>.withoutInputs
+  }
+  let info := {info with
+    allTransTrace :=
+      if imp.importAll then
+        info.allTransTrace
+        |>.mix expInfo.allTransTrace
+        |>.mix expInfo.allArtsTrace.withoutInputs
+        |>.withoutInputs
+      else if imp.isMeta then
+        info.allTransTrace
+        |>.mix expInfo.metaTransTrace
+        |>.mix expInfo.metaArtsTrace.withoutInputs
+        |>.withoutInputs
+      else
+        info.allTransTrace
+        |>.mix expInfo.transTrace
+        |>.mix expInfo.artsTrace.withoutInputs
+        |>.withoutInputs
   }
-  let info :=
-    if imp.importAll then
-      {info with
-        allTransTrace := info.allTransTrace
-          |>.mix expInfo.allTransTrace
-          |>.mix expInfo.allArtsTrace.withoutInputs
-          |>.withoutInputs
-      }
-    else if imp.isMeta then
-      {info with
-        allTransTrace := info.allTransTrace
-          |>.mix expInfo.metaTransTrace
-          |>.mix expInfo.metaArtsTrace.withoutInputs
-          |>.withoutInputs
-      }
-    else
-      {info with
-        allTransTrace := info.allTransTrace
-          |>.mix expInfo.transTrace
-          |>.mix expInfo.artsTrace.withoutInputs
-          |>.withoutInputs
-      }
   let info := {info with
     metaTransTrace := info.metaTransTrace
-      |>.mix expInfo.metaTransTrace
-      |>.mix expInfo.metaArtsTrace.withoutInputs
-      |>.withoutInputs
+    |>.mix expInfo.metaTransTrace
+    |>.mix expInfo.metaArtsTrace.withoutInputs
+    |>.withoutInputs
+  }
+  let info := {info with
+    irSigTrace :=
+      if nonModule || imp.importAll then
+        info.irSigTrace
+        |>.mix expInfo.allTransTrace
+        |>.mix expInfo.allArtsTrace.withoutInputs
+      else
+        info.irSigTrace
+        |>.mix expInfo.irSigTransTrace
+        |>.mix expInfo.irSigArtsTrace.withoutInputs
   }
-  /-
-  `leanir` reads the `.ir.sig` of every import with data and the full `.ir` of those `import all`ed
-  (`importModulesCore` with `loadIRSig`, which also ignores `meta`). As at the root of that import
-  it has data for every direct import, `irSigTrace` mixes one in unconditionally, whereas
-  `irSigTransTrace` mixes in only the exported ones, as for `transTrace`.
-  -/
-  let info :=
-    if nonModule || imp.importAll then
-      {info with
-        irSigTrace := info.irSigTrace
-          |>.mix expInfo.allTransTrace
-          |>.mix expInfo.allArtsTrace.withoutInputs
-      }
-    else
-      {info with
-        irSigTrace := info.irSigTrace
-          |>.mix expInfo.irSigTransTrace
-          |>.mix expInfo.irSigArtsTrace.withoutInputs
-      }
-  let info :=
-    if !imp.isExported then
-      info
-    else if imp.importAll then
-      {info with
-        irSigTransTrace := info.irSigTransTrace
-          |>.mix expInfo.allTransTrace
-          |>.mix expInfo.allArtsTrace.withoutInputs
-          |>.withoutInputs
-      }
-    else
-      {info with
-        irSigTransTrace := info.irSigTransTrace
-          |>.mix expInfo.irSigTransTrace
-          |>.mix expInfo.irSigArtsTrace.withoutInputs
-          |>.withoutInputs
-      }
   if imp.isExported then
-    if imp.isMeta then
-      {info with
-        transTrace := info.transTrace
+    {info with
+      transTrace :=
+        if imp.isMeta then
+          info.transTrace
           |>.mix expInfo.metaTransTrace
           |>.mix expInfo.metaArtsTrace.withoutInputs
           |>.withoutInputs
-      }
-    else
-      {info with
-        transTrace := info.transTrace
+        else
+          info.transTrace
           |>.mix expInfo.transTrace
           |>.mix expInfo.artsTrace.withoutInputs
           |>.withoutInputs
-      }
+      irSigTransTrace := info.irSigTransTrace
+      |>.mix expInfo.irSigTransTrace
+      |>.mix expInfo.irSigArtsTrace.withoutInputs
+      |>.withoutInputs
+    }
   else
     info
 
diff --git a/tests/lake/tests/moduleCodegen/test.sh b/tests/lake/tests/moduleCodegen/test.sh
index d1f69d9e4e05..16e103df6514 100755
--- a/tests/lake/tests/moduleCodegen/test.sh
+++ b/tests/lake/tests/moduleCodegen/test.sh
@@ -13,19 +13,19 @@ copy_to_work lakefile.toml Main.lean Test.lean Test Eval.lean
 
 # Elaboration alone does not generate code
 test_run build Test.A
-test_cmd_fails test -f .lake/build/ir/Test/A.c
+test_exp ! -f .lake/build/ir/Test/A.c
 
 # Each module's code generation is a job of its own
 echo "# TEST: code generation"
 test_out "Built Test.A:irArts" build Test.A:c -v
-test_cmd test -f .lake/build/lib/lean/Test/A.ir.sig
-test_cmd test -f .lake/build/lib/lean/Test/A.ir
+test_exp -f .lake/build/lib/lean/Test/A.ir.sig
+test_exp -f .lake/build/lib/lean/Test/A.ir
 test_out "Built Test.B:irArts" build Test.B:c -v
 test_run build Test.C:c
 
 # An import's IR must be provided even for a plain `import`, as the language server loads it
-test_cmd grep -F 'Test/A.ir"' .lake/build/ir/Test/B.setup.json
-test_cmd grep -F 'Test/A.ir"' .lake/build/ir/Test/B.irsetup.json
+match_text 'Test/A.ir"' .lake/build/ir/Test/B.setup.json
+match_text 'Test/A.ir"' .lake/build/ir/Test/B.irsetup.json
 
 # The server allows `#eval` on a plainly imported definition, so it must be able to run it
 echo "# TEST: server eval across a plain import"
@@ -35,8 +35,7 @@ test_cmd_eq 42 lean --setup eval.setup.json -DElab.inServer=true Eval.lean
 
 # The generated code links and runs
 echo "# TEST: link and run"
-test_run build codegen
-test_cmd_eq 42 ./.lake/build/bin/codegen
+test_eq 42 exe codegen
 
 # ---
 # Tests that `leanir` is only rerun when needed
@@ -57,4 +56,3 @@ test_run build Test.A:c Test.B:c Test.C:c
 test_cmd sed_i 's/^private def offset/public def extra : Nat := 7\nprivate def offset/' Test/A.lean
 test_out "Built Test.A:irArts" build Test.A:c -v
 test_out "Built Test.B:irArts" build Test.B:c -v
-