From 390d4b28f24e6e1a3366799312324c4d9ec00643 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Nov 2022 08:33:55 -0800 Subject: [PATCH] chore: disable most LCNF passes to be able to use `update-stage0` We cannot effectively test without an `update-stage0` since the LCNF representation is different and incompatible with the one in the .olean files. One of the passes is not terminating (probably `simp`) when compiling stage2. --- src/Lean/Compiler/LCNF/Passes.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index 33aefdc4b8..3bfee21ea7 100644 --- a/src/Lean/Compiler/LCNF/Passes.lean +++ b/src/Lean/Compiler/LCNF/Passes.lean @@ -45,6 +45,7 @@ def builtinPassManager : PassManager := { init, pullInstances, cse, +/- simp, floatLetIn, findJoinPoints, @@ -55,7 +56,9 @@ def builtinPassManager : PassManager := { specialize, simp (occurrence := 2), cse (occurrence := 1), +-/ saveBase, -- End of base phase +/- toMono, simp (occurrence := 3) (phase := .mono), reduceJpArity (phase := .mono), @@ -69,6 +72,7 @@ def builtinPassManager : PassManager := { extendJoinPointContext (phase := .mono) (occurrence := 1), simp (occurrence := 5) (phase := .mono), cse (occurrence := 2) (phase := .mono), +-/ saveMono -- End of mono phase ] }