chore: stop running compiler twice during tests (#6321)

The reason given for this in the comment seemingly no longer holds. Co-authored-by: Cameron Zwarich <cameron@lean-fro.org>
leanprover · Dec 13, 2024 · aa00725 · aa00725
1 parent 7530fd6
commit aa00725
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 15 deletions.
diff --git a/tests/lean/run/CompilerCSE.lean b/tests/lean/run/CompilerCSE.lean
@@ -6,9 +6,6 @@ import Lean.Elab.Command
 open Lean
 open Lean.Compiler.LCNF
 
--- Run compilation twice to avoid the output caused by the inliner
-run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo]
-
 @[cpass]
 def cseFixTest : PassInstaller := Testing.assertIsAtFixPoint |>.install `cse `cseFix
 

diff --git a/tests/lean/run/CompilerFindJoinPoints.lean b/tests/lean/run/CompilerFindJoinPoints.lean
@@ -6,9 +6,6 @@ import Lean.Elab.Command
 open Lean
 open Lean.Compiler.LCNF
 
--- Run compilation twice to avoid the output caused by the inliner
-run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo, ``Lean.MetavarContext.MkBinding.collectForwardDeps]
-
 @[cpass]
 def findJoinPointFixTest : PassInstaller := Testing.assertIsAtFixPoint |>.install `findJoinPoints `findJoinPointsFix
 

diff --git a/tests/lean/run/CompilerFloatLetIn.lean b/tests/lean/run/CompilerFloatLetIn.lean
@@ -6,9 +6,6 @@ import Lean.Elab.Command
 open Lean
 open Lean.Compiler.LCNF
 
--- Run compilation twice to avoid the output caused by the inliner
-run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo]
-
 -- #eval fails if we uncomment this pass after I added a `floatLetIn` pass at the mono phase
 -- @[cpass]
 -- def floatLetInFixTest : PassInstaller := Testing.assertIsAtFixPoint |>.install `floatLetIn `floatLetInFix

diff --git a/tests/lean/run/CompilerPullInstances.lean b/tests/lean/run/CompilerPullInstances.lean
@@ -6,9 +6,6 @@ import Lean.Elab.Command
 open Lean
 open Lean.Compiler.LCNF
 
--- Run compilation twice to avoid the output caused by the inliner
-run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo]
-
 @[cpass]
 def pullInstancesFixTest : PassInstaller := Testing.assertIsAtFixPoint |>.install `pullInstances `pullInstancesFix
 

diff --git a/tests/lean/run/CompilerSimp.lean b/tests/lean/run/CompilerSimp.lean
@@ -6,9 +6,6 @@ import Lean.Elab.Command
 open Lean
 open Lean.Compiler.LCNF
 
--- Run compilation twice to avoid the output caused by the inliner
-run_meta Compiler.compile #[``Lean.Meta.synthInstance, ``Lean.Elab.Term.Do.elabDo]
-
 @[cpass]
 def simpFixTest : PassInstaller := Testing.assertIsAtFixPoint |>.install `simp `simpFix