From 9fcf3d46758e11b433963afa1da60ceb4d21d671 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 18 Aug 2015 12:39:14 -0700
Subject: [PATCH] fix(tests/lean/extra): discrepancy between tests output when
 compiling Lean with IGNORE_SORRY

---
 tests/lean/extra/755.expected.out              | 3 ---
 tests/lean/extra/755.hlean                     | 8 ++++----
 tests/lean/extra/print_info.12.19.expected.out | 1 -
 tests/lean/extra/print_info.12.20.expected.out | 1 -
 tests/lean/extra/print_info.12.30.expected.out | 1 -
 tests/lean/extra/print_info.17.0.expected.out  | 1 -
 tests/lean/extra/print_info.17.2.expected.out  | 1 -
 tests/lean/extra/print_info.21.0.expected.out  | 1 -
 tests/lean/extra/print_info.21.1.expected.out  | 1 -
 tests/lean/extra/print_info.21.3.expected.out  | 1 -
 tests/lean/extra/print_info.lean               | 4 ++--
 11 files changed, 6 insertions(+), 17 deletions(-)

diff --git a/tests/lean/extra/755.expected.out b/tests/lean/extra/755.expected.out
index 4def83188..253f7dea6 100644
--- a/tests/lean/extra/755.expected.out
+++ b/tests/lean/extra/755.expected.out
@@ -1,6 +1,3 @@
-755.hlean:56:10: warning: using 'sorry'
-755.hlean:57:10: warning: using 'sorry'
-755.hlean:58:10: warning: using 'sorry'
 LEAN_INFORMATION
 position 55:52
 A : Type,
diff --git a/tests/lean/extra/755.hlean b/tests/lean/extra/755.hlean
index d508bcf29..193156c89 100644
--- a/tests/lean/extra/755.hlean
+++ b/tests/lean/extra/755.hlean
@@ -1,7 +1,7 @@
 import types.eq types.pi hit.colimit
 
 open eq is_trunc unit quotient seq_colim equiv
-
+axiom mysorry : ∀ {A : Type}, A
 namespace one_step_tr
 section
   parameters {A : Type}
@@ -53,7 +53,7 @@ definition one_step_tr_up (A B : Type)
 begin
   fapply equiv.MK,
   { intro f, fconstructor, intro a, exact f (tr a), intros, exact ap f !tr_eq},
-  { exact sorry},
-  { exact sorry},
-  { exact sorry},
+  { exact mysorry},
+  { exact mysorry},
+  { exact mysorry},
 end
diff --git a/tests/lean/extra/print_info.12.19.expected.out b/tests/lean/extra/print_info.12.19.expected.out
index 92b0c3876..885bc42df 100644
--- a/tests/lean/extra/print_info.12.19.expected.out
+++ b/tests/lean/extra/print_info.12.19.expected.out
@@ -3,4 +3,3 @@ definition int.mul : ℤ → ℤ → ℤ
 
 definition nat.mul : ℕ → ℕ → ℕ
 END_LEAN_INFORMATION
-print_info.lean:13:8: warning: using 'sorry'
diff --git a/tests/lean/extra/print_info.12.20.expected.out b/tests/lean/extra/print_info.12.20.expected.out
index 92b0c3876..885bc42df 100644
--- a/tests/lean/extra/print_info.12.20.expected.out
+++ b/tests/lean/extra/print_info.12.20.expected.out
@@ -3,4 +3,3 @@ definition int.mul : ℤ → ℤ → ℤ
 
 definition nat.mul : ℕ → ℕ → ℕ
 END_LEAN_INFORMATION
-print_info.lean:13:8: warning: using 'sorry'
diff --git a/tests/lean/extra/print_info.12.30.expected.out b/tests/lean/extra/print_info.12.30.expected.out
index be2c4959f..e69de29bb 100644
--- a/tests/lean/extra/print_info.12.30.expected.out
+++ b/tests/lean/extra/print_info.12.30.expected.out
@@ -1 +0,0 @@
-print_info.lean:13:8: warning: using 'sorry'
diff --git a/tests/lean/extra/print_info.17.0.expected.out b/tests/lean/extra/print_info.17.0.expected.out
index 4d88a72d1..aec1f64ce 100644
--- a/tests/lean/extra/print_info.17.0.expected.out
+++ b/tests/lean/extra/print_info.17.0.expected.out
@@ -1,4 +1,3 @@
-print_info.lean:13:8: warning: using 'sorry'
 LEAN_INFORMATION
 definition rfl : ∀ {A : Type} {a : A}, a = a
 END_LEAN_INFORMATION
diff --git a/tests/lean/extra/print_info.17.2.expected.out b/tests/lean/extra/print_info.17.2.expected.out
index 4d88a72d1..aec1f64ce 100644
--- a/tests/lean/extra/print_info.17.2.expected.out
+++ b/tests/lean/extra/print_info.17.2.expected.out
@@ -1,4 +1,3 @@
-print_info.lean:13:8: warning: using 'sorry'
 LEAN_INFORMATION
 definition rfl : ∀ {A : Type} {a : A}, a = a
 END_LEAN_INFORMATION
diff --git a/tests/lean/extra/print_info.21.0.expected.out b/tests/lean/extra/print_info.21.0.expected.out
index 381410b0e..298e8de4c 100644
--- a/tests/lean/extra/print_info.21.0.expected.out
+++ b/tests/lean/extra/print_info.21.0.expected.out
@@ -1,4 +1,3 @@
-print_info.lean:13:8: warning: using 'sorry'
 LEAN_INFORMATION
 parameter a₁ : ℕ
 END_LEAN_INFORMATION
diff --git a/tests/lean/extra/print_info.21.1.expected.out b/tests/lean/extra/print_info.21.1.expected.out
index 381410b0e..298e8de4c 100644
--- a/tests/lean/extra/print_info.21.1.expected.out
+++ b/tests/lean/extra/print_info.21.1.expected.out
@@ -1,4 +1,3 @@
-print_info.lean:13:8: warning: using 'sorry'
 LEAN_INFORMATION
 parameter a₁ : ℕ
 END_LEAN_INFORMATION
diff --git a/tests/lean/extra/print_info.21.3.expected.out b/tests/lean/extra/print_info.21.3.expected.out
index 7f2a803ee..384e15f05 100644
--- a/tests/lean/extra/print_info.21.3.expected.out
+++ b/tests/lean/extra/print_info.21.3.expected.out
@@ -1,4 +1,3 @@
-print_info.lean:13:8: warning: using 'sorry'
 LEAN_INFORMATION
 _ `+`:65 _:65 :=
   | nat.add #1 #0
diff --git a/tests/lean/extra/print_info.lean b/tests/lean/extra/print_info.lean
index ea87922b7..310791c78 100644
--- a/tests/lean/extra/print_info.lean
+++ b/tests/lean/extra/print_info.lean
@@ -3,14 +3,14 @@ open nat int
 
 variables a b : nat
 variables i j : int
-
+axiom mysorry : ∀ {A : Type}, A
 definition foo := add a i
 definition f₁ := a + i
 
 example (n : nat) : n + n = 2 * n :=
 begin
   unfold [nat.add,mul],
-  apply sorry
+  apply mysorry
 end
 
 example (n : nat) : n + n = n + n :=