chore: finish Lake changes

Author: Kha

src/lake/Lake/Build/Module.lean

@@ -483,6 +483,11 @@ def Module.ileanFacetConfig : ModuleFacetConfig ileanFacet :=
       addTrace art.trace
       return art.path
 
+/-- The `ModuleFacetConfig` for the builtin `irFacet`. -/
+def Module.irFacetConfig : ModuleFacetConfig irFacet :=
+  mkFacetJobConfig <| fetchOLeanCore "ir" (·.ir)
+    "No `.ir` generated. Ensure the module system is enabled."
+
 /-- The `ModuleFacetConfig` for the builtin `cFacet`. -/
 def Module.cFacetConfig : ModuleFacetConfig cFacet :=
   mkFacetJobConfig fun mod => do
@@ -630,6 +635,7 @@ def Module.initFacetConfigs : DNameMap ModuleFacetConfig :=
   |>.insert oleanServerFacet oleanServerFacetConfig
   |>.insert oleanPrivateFacet oleanPrivateFacetConfig
   |>.insert ileanFacet ileanFacetConfig
+  |>.insert irFacet irFacetConfig
   |>.insert cFacet cFacetConfig
   |>.insert bcFacet bcFacetConfig
   |>.insert coFacet coFacetConfig