From fa101444b454fbefc4f8913eb76049ebd6bd0199 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 25 Oct 2020 09:11:13 -0700
Subject: [PATCH] chore: fix tests

---
 tests/compiler/StackOverflow.lean             |   1 +
 tests/compiler/StackOverflowTask.lean         |   1 +
 tests/compiler/qsortBadLt.lean                |   1 +
 tests/lean/class_def_must_fail.lean           |   1 +
 .../class_def_must_fail.lean.expected.out     |   4 +-
 .../lean/ll_infer_type_bug.lean.expected.out  |   6 +-
 tests/lean/run/emptycOverloadIssues.lean      |   1 +
 tests/lean/run/listDecEq.lean                 |   1 +
 tests/lean/run/meta2.lean                     |  31 +---
 tests/lean/run/parseCore.lean                 |   3 +-
 tests/lean/run/reduce2.lean                   |  10 +-
 tests/lean/run/reduce3.lean                   |   4 +-
 tests/lean/server/diags.lean                  |   2 +-
 tests/lean/server/edits.lean                  |   2 +-
 tests/lean/server/init_exit.lean              |   2 +-
 tests/lean/trust0/basic.lean                  | 160 ------------------
 16 files changed, 22 insertions(+), 208 deletions(-)
 delete mode 100644 tests/lean/trust0/basic.lean

diff --git a/tests/compiler/StackOverflow.lean b/tests/compiler/StackOverflow.lean
index e495adbe68..b741b11497 100644
--- a/tests/compiler/StackOverflow.lean
+++ b/tests/compiler/StackOverflow.lean
@@ -1,3 +1,4 @@
+#lang lean4
 partial def foo : Nat → Nat | n => foo n + 1
 @[neverExtract]
 def main : IO Unit := IO.println $ foo 0
diff --git a/tests/compiler/StackOverflowTask.lean b/tests/compiler/StackOverflowTask.lean
index cbbc961cba..1f4d314c91 100644
--- a/tests/compiler/StackOverflowTask.lean
+++ b/tests/compiler/StackOverflowTask.lean
@@ -1,3 +1,4 @@
+#lang lean4
 partial def foo : Nat → Nat | n => foo n + 1
 @[neverExtract]
 def main : IO Unit := IO.println $ Task.get $ Task.spawn fun _ => foo 0
diff --git a/tests/compiler/qsortBadLt.lean b/tests/compiler/qsortBadLt.lean
index f9a8d857a3..6d28b70714 100644
--- a/tests/compiler/qsortBadLt.lean
+++ b/tests/compiler/qsortBadLt.lean
@@ -1,3 +1,4 @@
+#lang lean4
 def badLt (a b : Nat) : Bool :=
 a != b
 
diff --git a/tests/lean/class_def_must_fail.lean b/tests/lean/class_def_must_fail.lean
index 7ec170cd62..a160b390e6 100644
--- a/tests/lean/class_def_must_fail.lean
+++ b/tests/lean/class_def_must_fail.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /- The following definition should fail. -/
 @[class] def Foo (n : Nat) : Prop := n > 2
 
diff --git a/tests/lean/class_def_must_fail.lean.expected.out b/tests/lean/class_def_must_fail.lean.expected.out
index 9f9cfcb007..0948503a8d 100644
--- a/tests/lean/class_def_must_fail.lean.expected.out
+++ b/tests/lean/class_def_must_fail.lean.expected.out
@@ -1,2 +1,2 @@
-class_def_must_fail.lean:2:13: error: invalid 'class', declaration 'Foo' must be inductive datatype or structure
-class_def_must_fail.lean:7:0: error: invalid 'class', declaration 'Bla' must be inductive datatype or structure
+class_def_must_fail.lean:3:0: error: invalid 'class', declaration 'Foo' must be inductive datatype or structure
+class_def_must_fail.lean:8:18: error: invalid 'class', declaration 'Bla' must be inductive datatype or structure
diff --git a/tests/lean/ll_infer_type_bug.lean.expected.out b/tests/lean/ll_infer_type_bug.lean.expected.out
index 6062de0ea0..3b9d50fca4 100644
--- a/tests/lean/ll_infer_type_bug.lean.expected.out
+++ b/tests/lean/ll_infer_type_bug.lean.expected.out
@@ -1,6 +1,6 @@
 unsafe def f._cstage2 : _obj → UInt8 :=
 fun (x : _obj) =>
   List.casesOn
-    fun (hd tl : _obj) =>
-      let _x_1 : UInt8 := Nat.decLt 0 hd;
-      Bool.casesOn false (f tl)
+    fun (head tail : _obj) =>
+      let _x_1 : UInt8 := Nat.decLt 0 head;
+      Bool.casesOn false (f tail)
diff --git a/tests/lean/run/emptycOverloadIssues.lean b/tests/lean/run/emptycOverloadIssues.lean
index c13733ba37..9dd4b9a638 100644
--- a/tests/lean/run/emptycOverloadIssues.lean
+++ b/tests/lean/run/emptycOverloadIssues.lean
@@ -1,3 +1,4 @@
+#lang lean4
 structure A :=
 (x : Nat := 10)
 
diff --git a/tests/lean/run/listDecEq.lean b/tests/lean/run/listDecEq.lean
index 225e16d579..060978784e 100644
--- a/tests/lean/run/listDecEq.lean
+++ b/tests/lean/run/listDecEq.lean
@@ -1,3 +1,4 @@
+#lang lean4
 -- List decidable equality using `withPtrEqDecEq`
 def listDecEqAux {α} [s : DecidableEq α] : ∀ (as bs : List α), Decidable (as = bs)
 | [],    []    => isTrue rfl
diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean
index 077e2ffab6..1058ca685d 100644
--- a/tests/lean/run/meta2.lean
+++ b/tests/lean/run/meta2.lean
@@ -1,5 +1,5 @@
+#lang lean4
 import Lean.Meta
-new_frontend
 open Lean
 open Lean.Meta
 
@@ -153,20 +153,6 @@ do print "----- tst7 -----";
 
 #eval tst7
 
-def tst8 : MetaM Unit :=
-do print "----- tst8 -----";
-   let add := mkAppN (mkConst `HasAdd.add [levelOne]) #[nat, mkConst `Nat.HasAdd];
-   let t   := mkAppN add #[mkNatLit 2, mkNatLit 3];
-   let t ← withTransparency TransparencyMode.reducible $ whnf t;
-   print t;
-   let t ← whnf t;
-   print t;
-   let t ← reduce t;
-   print t;
-   pure ()
-
-#eval tst8
-
 def tst9 : MetaM Unit :=
 do print "----- tst9 -----";
    let env ← getEnv;
@@ -370,21 +356,6 @@ do print "----- tst23 -----";
 
 #eval tst23
 
-def tst24 : MetaM Unit :=
-do print "----- tst24 -----";
-   let m1 ← mkFreshExprMVar (← mkArrow nat (← mkArrow type type));
-   let m2 ← mkFreshExprMVar type;
-   let zero ← mkAppM `HasZero.zero #[nat];
-   let idNat ← mkAppM `Id #[nat];
-   let lhs := mkAppB m1 zero m2;
-   print zero;
-   print idNat;
-   print lhs;
-   checkM $ fullApproxDefEq $ isDefEq lhs idNat;
-   pure ()
-
-#eval tst24
-
 def tst25 : MetaM Unit :=
 do print "----- tst25 -----";
    withLocalDeclD `α type $ fun α =>
diff --git a/tests/lean/run/parseCore.lean b/tests/lean/run/parseCore.lean
index 58b57c19d4..be79608f88 100644
--- a/tests/lean/run/parseCore.lean
+++ b/tests/lean/run/parseCore.lean
@@ -1,5 +1,6 @@
+#lang lean4
 import Lean.Parser
-new_frontend
+
 def test : IO Unit :=
 if System.Platform.isWindows then
   pure () -- TODO investigate why the following doesn't work on Windows
diff --git a/tests/lean/run/reduce2.lean b/tests/lean/run/reduce2.lean
index 488eec8629..e864beae7f 100644
--- a/tests/lean/run/reduce2.lean
+++ b/tests/lean/run/reduce2.lean
@@ -1,15 +1,9 @@
+#lang lean4
+
 def fact : Nat → Nat
 | 0     => 1
 | (n+1) => (n+1)*fact n
 
-
 def v1 := fact 10
 theorem v1Eq : v1 = fact 10 :=
 Eq.refl (fact 10)
-
-new_frontend
-set_option trace.Elab.definition true
-
-abbrev v2 := fact 10
-theorem v2Eq : v2 = fact 10 :=
-Eq.refl (fact 10)
diff --git a/tests/lean/run/reduce3.lean b/tests/lean/run/reduce3.lean
index 161d2fc09a..2acf980457 100644
--- a/tests/lean/run/reduce3.lean
+++ b/tests/lean/run/reduce3.lean
@@ -1,11 +1,13 @@
+#lang lean4
+
 def fact : Nat → Nat
 | 0     => 1
 | (n+1) => (n+1)*fact n
 
 #check fact 6
+
 #eval fact 10
 
-new_frontend
 -- set_option pp.all true
 theorem tst1 : 100000000000 + 200000000000 = 300000000000 :=
 rfl
diff --git a/tests/lean/server/diags.lean b/tests/lean/server/diags.lean
index 2fd39d5309..4b96c6191c 100644
--- a/tests/lean/server/diags.lean
+++ b/tests/lean/server/diags.lean
@@ -1,3 +1,3 @@
+#lang lean4
 import Lean.Server
-
 #eval Lean.Server.Test.runWithInputFile "./diags_client.log" none -- The builtin search path seems to be fine
diff --git a/tests/lean/server/edits.lean b/tests/lean/server/edits.lean
index 7dbf4c1ed6..cf907f4912 100644
--- a/tests/lean/server/edits.lean
+++ b/tests/lean/server/edits.lean
@@ -1,3 +1,3 @@
+#lang lean4
 import Lean.Server
-
 #eval Lean.Server.Test.runWithInputFile "./edits_client.log" none -- The builtin search path seems to be fine
diff --git a/tests/lean/server/init_exit.lean b/tests/lean/server/init_exit.lean
index 481551275e..93a946155d 100644
--- a/tests/lean/server/init_exit.lean
+++ b/tests/lean/server/init_exit.lean
@@ -1,3 +1,3 @@
+#lang lean4
 import Lean.Server
-
 #eval Lean.Server.Test.runWithInputFile "./init_exit_client.log" none
diff --git a/tests/lean/trust0/basic.lean b/tests/lean/trust0/basic.lean
deleted file mode 100644
index bc20fec135..0000000000
--- a/tests/lean/trust0/basic.lean
+++ /dev/null
@@ -1,160 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Floris van Doorn, Leonardo de Moura
--/
-prelude
-import Init.Core
-
-notation `ℕ` := Nat
-
-namespace Nat
-
-inductive lessThanOrEqual (a : ℕ) : ℕ → Prop
-| refl {} : lessThanOrEqual a
-| step : ∀ {b}, lessThanOrEqual b → lessThanOrEqual (succ b)
-
-@[elabAsEliminator]
-theorem lessThanOrEqual.ndrec  {a : Nat} {C : Nat → Prop} (m₁ : C a) (m₂ : ∀ (b : Nat), lessThanOrEqual a b → C b → C (succ b)) {b : ℕ} (h : lessThanOrEqual a b) : C b :=
-@lessThanOrEqual.rec a (fun b _ => C b) m₁ m₂ b h
-
-@[elabAsEliminator]
-theorem lessThanOrEqual.ndrecOn {a : Nat} {C : Nat → Prop} {b : ℕ} (h : lessThanOrEqual a b) (m₁ : C a) (m₂ : ∀ (b : Nat), lessThanOrEqual a b → C b → C (succ b)) : C b :=
-@lessThanOrEqual.rec a (fun b _ => C b) m₁ m₂ b h
-
-instance : HasLessEq ℕ :=
-⟨Nat.lessThanOrEqual⟩
-
-@[reducible] protected def le (n m : ℕ) := Nat.lessThanOrEqual n m
-@[reducible] protected def lt (n m : ℕ) := Nat.lessThanOrEqual (succ n) m
-
-set_option codegen false
-
-
-instance : HasLess ℕ :=
-⟨Nat.lt⟩
-
-def pred : ℕ → ℕ
-| 0     => 0
-| a+1   => a
-
-protected def sub : ℕ → ℕ → ℕ
-| a, 0     => a
-| a, b+1   => pred (sub a b)
-
-protected def mul : Nat → Nat → Nat
-| a, 0     => 0
-| a, b+1   => (mul a b) + a
-
-instance : HasSub ℕ :=
-⟨Nat.sub⟩
-
-instance : HasMul ℕ :=
-⟨Nat.mul⟩
-
-def hasDecEq : ∀ (a b : Nat), Decidable (a = b)
-| zero,     zero     => isTrue rfl
-| succ x,   zero     => isFalse (fun h => Nat.noConfusion h)
-| zero,     succ y   => isFalse (fun h => Nat.noConfusion h)
-| succ x,   succ y   =>
-    match hasDecEq x y with
-    | isTrue xeqy => isTrue (xeqy ▸ Eq.refl (succ x))
-    | isFalse xney => isFalse (fun h => Nat.noConfusion h (fun xeqy => absurd xeqy xney))
-
-instance : DecidableEq ℕ :=
-hasDecEq
-
-def repeat.{u} {α : Type u} (f : ℕ → α → α) : ℕ → α → α
-| 0,         a => a
-| succ n,    a => f n (repeat n a)
-
-theorem natZeroEqZero : Nat.zero = 0 :=
-rfl
-
-/- properties of inequality -/
-
-protected def leRefl : ∀ (a : ℕ), a ≤ a :=
-lessThanOrEqual.refl
-
-theorem leSucc (n : ℕ) : n ≤ succ n :=
-lessThanOrEqual.step (Nat.leRefl n)
-
-theorem succLeSucc {n m : ℕ} : n ≤ m → succ n ≤ succ m :=
-fun h => lessThanOrEqual.ndrec (Nat.leRefl (succ n)) (fun a b => lessThanOrEqual.step) h
-
-theorem zeroLe : ∀ (n : ℕ), 0 ≤ n
-| 0     => Nat.leRefl 0
-| n+1   => lessThanOrEqual.step (zeroLe n)
-
-theorem zeroLtSucc (n : ℕ) : 0 < succ n :=
-succLeSucc (zeroLe n)
-
-def succPos := zeroLtSucc
-
-theorem notSuccLeZero (n : ℕ) (h : succ n ≤ 0) : False :=
-nomatch h
-
-theorem notLtZero (a : ℕ) : ¬ a < 0 := notSuccLeZero a
-
-theorem predLePred {n m : ℕ} : n ≤ m → pred n ≤ pred m :=
-fun h => lessThanOrEqual.ndrecOn h
-  (Nat.leRefl (pred n))
-  (fun n => Nat.rec (fun a b => b) (fun a b c => lessThanOrEqual.step) n)
-
-theorem leOfSuccLeSucc {n m : ℕ} : succ n ≤ succ m → n ≤ m :=
-predLePred
-
-instance decidableLe : ∀ (a b : ℕ), Decidable (a ≤ b)
-| 0,     b     => isTrue (zeroLe b)
-| a+1,   0     => isFalse (notSuccLeZero a)
-| a+1,   b+1   =>
-  match decidableLe a b with
-  | isTrue h  => isTrue (succLeSucc h)
-  | isFalse h => isFalse (fun a => h (leOfSuccLeSucc a))
-
-instance decidableLt : ∀ (a b : ℕ), Decidable (a < b) :=
-fun a b => Nat.decidableLe (succ a) b
-
-protected theorem eqOrLtOfLe {a b : ℕ} (h : a ≤ b) : a = b ∨ a < b :=
-lessThanOrEqual.casesOn h (Or.inl rfl) (fun n h => Or.inr (succLeSucc h))
-
-theorem ltSuccOfLe {a b : ℕ} : a ≤ b → a < succ b :=
-succLeSucc
-
-theorem succSubSuccEqSub (a b : ℕ) : succ a - succ b = a - b :=
-Nat.recOn b
-  (show succ a - succ zero = a - zero from (Eq.refl (succ a - succ zero)))
-  (fun b => congrArg pred)
-
-theorem notSuccLeSelf : ∀ (n : ℕ), ¬succ n ≤ n :=
-fun n => Nat.rec (notSuccLeZero 0) (fun a b c => b (leOfSuccLeSucc c)) n
-
-protected theorem ltIrrefl (n : ℕ) : ¬n < n :=
-notSuccLeSelf n
-
-protected theorem leTrans {n m k : ℕ} (h1 : n ≤ m) : m ≤ k → n ≤ k :=
-lessThanOrEqual.ndrec h1 (fun p h2 => lessThanOrEqual.step)
-
-theorem predLe : ∀ (n : ℕ), pred n ≤ n
-| 0        => lessThanOrEqual.refl 0
-| succ a   => lessThanOrEqual.step (lessThanOrEqual.refl a)
-
-theorem predLt : ∀ {n : ℕ}, n ≠ 0 → pred n < n
-| 0,        h => absurd rfl h
-| succ a,   h => ltSuccOfLe (lessThanOrEqual.refl _)
-
-theorem subLe (a b : ℕ) : a - b ≤ a :=
-Nat.recOn b (Nat.leRefl (a - 0)) (fun b₁ => Nat.leTrans (predLe (a - b₁)))
-
-theorem subLt : ∀ {a b : ℕ}, 0 < a → 0 < b → a - b < a
-| 0,     b,     h1, h2 => absurd h1 (Nat.ltIrrefl 0)
-| a+1,   0,     h1, h2 => absurd h2 (Nat.ltIrrefl 0)
-| a+1,   b+1,   h1, h2 =>
-  Eq.symm (succSubSuccEqSub a b) ▸
-    show a - b < succ a from
-    ltSuccOfLe (subLe a b)
-
-protected theorem ltOfLtOfLe {n m k : ℕ} : n < m → m ≤ k → n < k :=
-Nat.leTrans
-
-end Nat