adapt Lake

Author: Kha

src/Lean/Environment.lean

@@ -1923,10 +1923,12 @@ def ModuleArtifacts.oleanParts (arts : ModuleArtifacts) : Array System.FilePath
   -- Producer (e.g., Lake) should limit parts to the proper import level.
   if let some mFile := arts.olean? then
     fnames := fnames.push mFile
-    if let some sFile := arts.oleanServer? then
-      fnames := fnames.push sFile
-      if let some pFile := arts.oleanPrivate? then
-        fnames := fnames.push pFile
+    if let some iFile := arts.oleanIR? then
+      fnames := fnames.push iFile
+      if let some sFile := arts.oleanServer? then
+        fnames := fnames.push sFile
+        if let some pFile := arts.oleanPrivate? then
+          fnames := fnames.push pFile
   return fnames
 
 private def findOLeanParts (mod : Name) : IO (Array System.FilePath) := do

src/Lean/Setup.lean

@@ -42,6 +42,7 @@ structure ModuleHeader where
 structure ModuleArtifacts where
   lean? : Option System.FilePath := none
   olean? : Option System.FilePath := none
+  oleanIR? : Option System.FilePath := none
   oleanServer? : Option System.FilePath := none
   oleanPrivate? : Option System.FilePath := none
   ilean? : Option System.FilePath := none