chore: move tests to new frontend

tests/lean/run/structInst3.lean

@@ -1,3 +1,4 @@
+new_frontend
 universes u
 
 namespace Ex1
@@ -13,7 +14,6 @@ structure C (α : Type u) extends B α :=
 
 end Ex1
 
-new_frontend
 open Ex1
 
 def c1 : C Nat := { x := 1 }

tests/lean/run/structInst4.lean

@@ -1,3 +1,4 @@
+new_frontend
 universes u
 
 def a : Array ((Nat × Nat) × Bool) := #[]
@@ -7,8 +8,6 @@ structure Foo :=
 (x : Array ((Nat × Nat) × Bool) := #[])
 (y : Nat := 0)
 
-new_frontend
-
 #check (b).modifyOp (idx := 1) (fun s => 2)
 
 #check { b with [1] := 2 }

tests/lean/run/struct_inst_typed.lean

@@ -1,3 +1,4 @@
+new_frontend
 #check { fst := 10, snd := 20 : Nat × Nat }
 
 structure S :=

tests/lean/run/struct_instance_in_eqn.lean

@@ -1,7 +1,7 @@
+new_frontend
+
 structure S :=
 (x : Nat) (y : Bool) (z : Nat) (w : Nat)
 
-set_option trace.compiler.stage1 true
-
 def g : S → S
 | s@{ x := x, ..} => { s with x := x + 1 }

tests/lean/run/structure.lean

@@ -1,4 +1,5 @@
 import Lean
+new_frontend
 open Lean
 
 structure S1 :=

tests/lean/run/synth1.lean

@@ -1,4 +1,5 @@
 import Lean.Meta
+new_frontend
 open Lean
 open Lean.Meta
 
@@ -26,14 +27,14 @@ instance coerceNatToInt : HasCoerce Nat Int :=
 def print {α} [HasToString α] (a : α) : MetaM Unit :=
 trace! `Meta.synthInstance (toString a)
 
-set_option trace.Meta.synthInstance true
-set_option trace.Meta.synthInstance.tryResolve false
 
 def tst1 : MetaM Unit :=
 do inst ← mkAppM `HasCoerce #[mkConst `Nat, mkSort levelZero];
    r ← synthInstance inst;
    print r
 
+set_option trace.Meta.synthInstance true in
+set_option trace.Meta.synthInstance.tryResolve false in
 #eval tst1
 
 def tst2 : MetaM Unit :=
@@ -46,6 +47,8 @@ do inst ← mkAppM `HasBind #[mkConst `IO];
    print r;
    pure ()
 
+set_option trace.Meta.synthInstance true in
+set_option trace.Meta.synthInstance.tryResolve false in
 #eval tst2
 
 def tst3 : MetaM Unit :=
@@ -54,4 +57,6 @@ do inst ← mkAppM `HasBeq #[mkConst `Nat];
    print r;
    pure ()
 
+set_option trace.Meta.synthInstance true in
+set_option trace.Meta.synthInstance.tryResolve false in
 #eval tst3

tests/lean/run/tactic.lean

@@ -1,4 +1,6 @@
 import Lean.Meta
+new_frontend
+
 open Lean
 open Lean.Meta
 
@@ -7,8 +9,6 @@ axiom simple : forall {p q : Prop}, p → q → p
 def print (msg : MessageData) : MetaM Unit :=
 trace! `Meta.Tactic msg
 
-set_option trace.Meta.Tactic true
-
 def tst1 : MetaM Unit :=
 do cinfo ← getConstInfo `simple;
    mvar  ← mkFreshExprSyntheticOpaqueMVar cinfo.type;
@@ -18,4 +18,6 @@ do cinfo ← getConstInfo `simple;
    result ← instantiateMVars mvar;
    print result
 
+set_option trace.Meta.Tactic true
+
 #eval tst1

tests/lean/run/task_test.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 def g (x : Nat) : Nat :=
 dbgTrace ("g: " ++ toString x) $ fun _ =>
   x + 1

tests/lean/run/task_test2.lean

@@ -1,3 +1,5 @@
+new_frontend
+
 def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat :=
 n.repeat (fun r =>
   dbgTrace (">> [" ++ toString i ++ "] " ++ toString r) $ fun _ =>

tests/lean/run/termElab.lean

@@ -1,11 +1,10 @@
 import Lean
+new_frontend
 
 open Lean
 open Lean.Elab
 open Lean.Elab.Term
 
-set_option trace.Elab.debug true
-
 def tst1 : TermElabM Unit := do
 opt ← getOptions;
 stx ← `(forall (a b : Nat), Nat);

tests/lean/run/termParserAttr.lean

@@ -1,4 +1,5 @@
 import Lean
+new_frontend
 open Lean
 open Lean.Elab
 
@@ -61,8 +62,6 @@ adaptExpander $ fun stx => match_syntax stx with
 #eval run "#check (| id 1 |)"
 #eval run "#check (| id 1, id 2 |)"
 
-new_frontend
-
 declare_syntax_cat foo
 
 syntax "⟨|" term "|⟩" : foo

tests/lean/run/termparsertest1.lean

@@ -1,4 +1,5 @@
 import Lean.Parser.Term
+new_frontend
 open Lean
 open Lean.Parser