feat: lake: seperate leanir job

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

Author: tydeu

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

src/lake/Lake/Build/Actions.lean

@@ -26,14 +26,26 @@ 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)
   (arts : ModuleArtifacts)
   (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)

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,28 +97,39 @@ 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.
   -/
   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
 

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