chore: remove new_frontend from tests

tests/compiler/append.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def main (xs : List String) : IO Unit :=
 let ys1 := List.replicate 1000000 1;

tests/compiler/array_test.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def foo (a : Array Nat) : Array Nat :=
 let a := a.push 0

tests/compiler/binomial.lean

@@ -1,5 +1,5 @@
 import Std.Data.BinomialHeap
-new_frontend
+
 open Std
 
 abbrev Heap := BinomialHeap Nat (fun a b => a < b)

tests/compiler/bytearray_bug.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def main (xs : List String) : IO Unit :=
   let arr := (let e := ByteArray.empty; e.push (UInt8.ofNat 10));
   let v := arr.data.get! 0;

tests/compiler/closure_bug1.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1
 let x2 := x + 2

tests/compiler/closure_bug2.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1
 let x2 := x + 2

tests/compiler/closure_bug3.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1
 let x2 := x + 2

tests/compiler/closure_bug4.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1
 let x2 := x + 2

tests/compiler/closure_bug5.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1;
 let x2 := x + 2;

tests/compiler/closure_bug6.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1;
 let x2 := x + 2;

tests/compiler/closure_bug7.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1;
 let x2 := x + 2;

tests/compiler/closure_bug8.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1;
 let x2 := x + 2;

tests/compiler/expr.lean

@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 def main : IO UInt32 := do

tests/compiler/float.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def tst1 : IO Unit := do
 IO.println (1 : Float);
 IO.println ((1 : Float) + 2);

tests/compiler/float_cases_bug.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 inductive Term : Type
 | const : Nat -> Term
 | app   : List Term -> Term

tests/compiler/init.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Foo
 

tests/compiler/lazylist.lean

@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-new_frontend
+
 universes u v w
 
 inductive LazyList (α : Type u)

tests/compiler/map_big.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f2 (n : Nat) (xs : List Nat) : List (List Nat) :=
 let ys := List.replicate n 0;
 xs.map (fun x => x :: ys)

tests/compiler/partial.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 set_option pp.implicit true
 set_option pp.binder_types false
 -- set_option trace.compiler.boxed true

tests/compiler/phashmap.lean

@@ -1,6 +1,6 @@
 import Std.Data.PersistentHashMap
 import Lean.Data.Format
-new_frontend
+
 open Lean Std Std.PersistentHashMap
 
 abbrev Map := PersistentHashMap Nat Nat

tests/elabissues/invalid_field_notation_error_msg.lean

@@ -15,7 +15,7 @@ def Foo.f3 (f : Foo) : Nat := f.n
 def Foo.f4 (f : Foo) : Nat := f.n
 def Foo.f5 (f : Foo) : Nat := f.n
 
-new_frontend
+
 
 #check (λ f g h =>
   let x : Foo := ⟨f.n + 1⟩;

tests/lean/IRbug.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Repro
 

tests/lean/PPRoundtrip.lean

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

tests/lean/Process.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 open IO.Process
 
 def usingIO {α} (x : IO α) : IO α := x

tests/lean/Reformat.lean

@@ -1,6 +1,6 @@
 /-! Parse and reformat file -/
 import Lean.PrettyPrinter
-new_frontend
+
 open Lean
 open Lean.Elab
 open Lean.Elab.Term

tests/lean/StxQuot.lean

@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 namespace Lean
 open Lean.Elab
 

tests/lean/abst.lean

@@ -1,5 +1,5 @@
 import Lean.Expr
-new_frontend
+
 open Lean
 
 def tst : IO Unit :=

tests/lean/appParserIssue.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) (g : Nat → Nat) := g x
 
 #check f 1 fun x => x   -- should work

tests/lean/attrCmd.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def M := StateM Nat
 

tests/lean/auxDeclIssue.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 theorem ex1 : False :=
 by {

tests/lean/binsearch.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 partial def mkAssocArray : Nat → Array (Nat × Bool) → Array (Nat × Bool)
 | 0,   as => as
 | i+1, as  => mkAssocArray i (as.push (i, i % 2 == 0))

tests/lean/bytearray.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def tst : IO Unit :=
 do
 let bs := [1, 2, 3].toByteArray;

tests/lean/classBadOutParam.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 class C1 (x : outParam Nat) (y : { n : Nat // n > x }) (α : Type) := -- should fail
 (val : α)
 

tests/lean/collectDepsIssue.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 variables {α : Type} in
 def f (a : α) : List α :=

tests/lean/ctor_layout.lean

@@ -1,5 +1,5 @@
 import Lean.Compiler.IR
-new_frontend
+
 open Lean
 open Lean.IR
 

tests/lean/dbgMacros.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) :=
 if x = 0 then panic! "unexpected zero"

tests/lean/doNotation1.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1 (x : Nat) : IO Nat := do
 y := 1  -- error 'y' cannot be reassigned

tests/lean/doSeqRightIssue.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 universes u
 variables {α : Type u}

tests/lean/emptyc.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure A :=
 (x : Nat := 0)

tests/lean/evalWithMVar.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def c {α} : Sum α Nat :=
 Sum.inr 10

tests/lean/eval_except.lean

@@ -1,5 +1,5 @@
 prelude
 import Init.System.IO
-new_frontend
+
 #eval (throw $ IO.userError "this is my error" : IO Unit)
 #eval (throw $ IO.Error.noFileOrDirectory "file.ext" 31 "and details" : IO Unit)

tests/lean/exitAfterParseError.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def foo 
 

tests/lean/extract.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 #eval "abc"
 
 /- some "a" -/

tests/lean/file_not_found.lean

@@ -1,6 +1,6 @@
 prelude
 import Init.System.IO
-new_frontend
+
 open IO.FS
 def usingIO {α} (x : IO α) : IO α := x
 #eval (discard $ IO.FS.Handle.mk "non-existent-file.txt" Mode.read : IO Unit)

tests/lean/holeErrors.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1 := id
 

tests/lean/holes.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) : Nat :=
 id (_ x)

tests/lean/hygienicIntro.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 set_option hygienicIntro false in
 theorem ex1 {a p q r : Prop} : p → (p → q) → (q → r) → r := by

tests/lean/inductive1.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 -- Test1
 inductive T1 : Nat -- Error, resultant type is not a sort

tests/lean/infoFromFailure.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def A.foo {α : Type} [HasAdd α] (a : α) : α × α :=
 (a, a + a)

tests/lean/inst.lean

@@ -1,5 +1,5 @@
 import Lean.Expr
-new_frontend
+
 open Lean
 
 def tst : IO Unit :=

tests/lean/json.lean

@@ -1,6 +1,6 @@
 import Lean.Data.Json.Parser
 import Lean.Data.Json.Printer
-new_frontend
+
 def test (s : String) : String :=
 match Lean.Json.parse s with
 | Except.ok res    => toString res

tests/lean/letrec1.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1.g := 10
 

tests/lean/ll_infer_type_bug.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 partial def f : List Nat → Bool
 | []      => false
 | (a::as) => a > 0 && f as

tests/lean/lvl1.lean

@@ -1,5 +1,5 @@
 import Lean.Level
-new_frontend
+
 namespace Lean
 namespace Level
 

tests/lean/macroStack.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1 :=
 if h:x then 1 else 0

tests/lean/macroscopes.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 open Lean
 def check (b : Bool) : IO Unit :=
 «unless» b $ throw $ IO.userError "check failed"

tests/lean/match1.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 #print "---- h1"
 

tests/lean/match2.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 #print "---- Op"
 

tests/lean/match3.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) : Nat :=
 match x with

tests/lean/match4.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1 (x : Nat × Nat) : Nat :=
 match x with

tests/lean/matchErrorLocation.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def head {α} (xs : List α) (h : xs = [] → False) : α :=
 match he:xs with

tests/lean/mutualWithNamespaceMacro.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 mutual
 

tests/lean/mutualdef1.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 mutual
 

tests/lean/mvar1.lean

@@ -1,5 +1,5 @@
 import Lean.MetavarContext
-new_frontend
+
 open Lean
 
 def check (b : Bool) : IO Unit :=

tests/lean/mvar2.lean

@@ -1,5 +1,5 @@
 import Lean.MetavarContext
-new_frontend
+
 open Lean
 
 def check (b : Bool) : IO Unit :=

tests/lean/mvar3.lean

@@ -1,5 +1,5 @@
 import Lean.MetavarContext
-new_frontend
+
 open Lean
 
 def mkLambdaTest (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)

tests/lean/mvar_fvar.lean

@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 #eval (mkFVar `a).hasFVar

tests/lean/namedHoles.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) (y : Bool) :=
 x + if y then 1 else 0

tests/lean/namelit.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 #check `foo
 #check `foo.bla

tests/lean/openExport.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def A.x := 10
 

tests/lean/parserPrio.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 -- New notation that overlaps with existing notation
 syntax [myPair, 100] "(" term "," term ")" : term

tests/lean/phashmap_inst_coherence.lean

@@ -1,5 +1,5 @@
 import Std.Data.PersistentHashMap
-new_frontend
+
 open Std
 def m : PersistentHashMap Nat Nat :=
 let m : PersistentHashMap Nat Nat := {};

tests/lean/ppExpr.lean

@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 
 /-! Pretty printing tests for `Expr`s that cannot be generated by parsing+elaborating. -/
 

tests/lean/precissues.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 #check id fun x => x -- should work
 

tests/lean/private.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 -- Issue 1
 def foo := 10

tests/lean/protected.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Foo
 

tests/lean/ref1.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def inc (r : IO.Ref Nat) : IO Unit := do
 let v ← r.get;
 r.set (v+1);

tests/lean/repr_issue.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
 tryCatch
   (do modify $ fun (a : Array Nat) => a.set! 0 33;

tests/lean/resolveGlobalName.lean

@@ -1,6 +1,6 @@
 import Lean
 
-new_frontend
+
 
 def Boo.x := 1
 def Foo.x := 2

tests/lean/rewrite.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 axiom appendNil {α} (as : List α) : as ++ [] = as
 axiom appendAssoc {α} (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs)

tests/lean/run/108.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 macro m n:ident : command => `(def $n := 1)
 

tests/lean/run/111.lean

@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 #check mkNullNode  -- Lean.Syntax
 #check mkNullNode #[]  -- Lean.Syntax

tests/lean/run/121.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 abbrev DelabM := Id
 abbrev Delab := DelabM Nat

tests/lean/run/125.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 class HasElems (α : Type) : Type := (elems : Array α)
 def elems (α : Type) [HasElems α] : Array α := HasElems.elems

tests/lean/run/175.lean

@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 
 namespace Foo
 open Lean.Elab.Term

tests/lean/run/1954.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def all (p : Nat → Prop) : Prop := ∀x, p x
 example {p : Nat → Prop} (h : all p) : p 0 := h 0

tests/lean/run/1968.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive type
 | bv  : Nat → type

tests/lean/run/28.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure bv (w : Nat) := (u:Unit)
 

tests/lean/run/29.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def foo : Nat -> Nat -> Nat -> List Nat
 | _, _, 0   => [1]

tests/lean/run/34.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 partial def foo : ∀ (n : Nat), StateM Unit Unit
 | n =>

tests/lean/run/CoeNew.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 universes u v w
 

tests/lean/run/CommandExtOverlap.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 syntax [mycheck] "#check" (sepBy term ",") : command
 

tests/lean/run/DefEqAssignBug.lean

@@ -1,6 +1,6 @@
 import Lean.Meta
 
-new_frontend
+
 
 open Lean
 open Lean.Meta

tests/lean/run/IO_test.lean

@@ -2,7 +2,7 @@ prelude
 import Init.System.IO
 import Init.Data.List.Control
 import Init.Data.ToString
-new_frontend
+
 
 open IO.FS
 

tests/lean/run/LiftMethodIssue.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def tst : IO (Option Nat) := do
 let x? : Option Nat ← pure none;

tests/lean/run/Reid1.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure ConstantFunction (α β : Type) :=
 (f : α → β)

tests/lean/run/Reparen.lean

@@ -1,6 +1,6 @@
 /-! Reprint file after removing all parentheses and then passing it through the parenthesizer -/
 import Lean.Parser
-new_frontend
+
 open Lean
 open Lean.Format
 

tests/lean/run/anonymous_ctor_error_msg.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure Foo := (n : Nat)
 

tests/lean/run/array1.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 #check @Array.mk
 
 def v : Array Nat := @Array.mk Nat 10 (fun ⟨i, _⟩ => i)

tests/lean/run/autoparam.lean

@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x y : Nat) (h : x = y := by assumption) : Nat :=
 x + x