feat: add extractClosed pass to LCNF pass list (#8462)

zwarich · web-flow · commit d5060e9e66ae · 2025-05-24T05:20:10.000Z
This PR enables the LCNF extractClosed pass by default.
diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean
@@ -80,7 +80,8 @@ def builtinPassManager : PassManager := {
     simp (occurrence := 5) (phase := .mono),
     structProjCases,
     cse (occurrence := 2) (phase := .mono),
-    saveMono  -- End of mono phase
+    saveMono,  -- End of mono phase
+    extractClosed
   ]
 }
 

Original file line number	Diff line number	Diff line change
`@@ -80,7 +80,8 @@ def builtinPassManager : PassManager := {`
`80`	`80`	`simp (occurrence := 5) (phase := .mono),`
`81`	`81`	`structProjCases,`
`82`	`82`	`cse (occurrence := 2) (phase := .mono),`
`83`		`- saveMono -- End of mono phase`
	`83`	`+ saveMono, -- End of mono phase`
	`84`	`+ extractClosed`
`84`	`85`	`]`
`85`	`86`	`}`
`86`	`87`