Consolidate patches to disable tests that are too big or too slow

Consolidate the several patches that disable tests that time out on
MIPS or use too much RAM/time on the buildds.

6 files changed, 85 insertions, 112 deletions

diff --git a/debian/patches/5127-fails-on-mips.patch b/debian/patches/5127-fails-on-mips.patch
deleted file mode 100644
index 949c33a7..00000000
--- a/debian/patches/5127-fails-on-mips.patch
+++ /dev/null
@@ -1,30 +0,0 @@
-From: Enrico Tassi <gareuselesinge@debian.org>
-Date: Thu, 29 Dec 2016 08:56:45 +0100
-Subject: 5127 fails on mips
-
----
- test-suite/bugs/closed/5127.v | 15 ---------------
- 1 file changed, 15 deletions(-)
- delete mode 100644 test-suite/bugs/closed/5127.v
-
-diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v
-deleted file mode 100644
-index 831e8fb..0000000
---- a/test-suite/bugs/closed/5127.v
-+++ /dev/null
-@@ -1,15 +0,0 @@
--Fixpoint arrow (n: nat) :=
--  match n with
--  | S n => bool -> arrow n
--  | O => bool
--  end.
--
--Fixpoint apply (n : nat) : arrow n -> bool :=
--  match n return arrow n -> bool with
--  | S n => fun f => apply _ (f true)
--  | O => fun x => x
--  end.
--
--Axiom f : arrow 10000.
--Definition v : bool := Eval compute in apply _ f.
--Definition w : bool := Eval vm_compute in v.
diff --git a/debian/patches/Remove-test-4429.patch b/debian/patches/Remove-test-4429.patch
deleted file mode 100644
index 9baee306..00000000
--- a/debian/patches/Remove-test-4429.patch
+++ /dev/null
@@ -1,46 +0,0 @@
-From: Enrico Tassi <gareuselesinge@debian.org>
-Date: Thu, 28 Jan 2016 10:11:08 +0100
-Subject: Remove test 4429
-
----
- test-suite/bugs/closed/4429.v | 31 -------------------------------
- 1 file changed, 31 deletions(-)
- delete mode 100644 test-suite/bugs/closed/4429.v
-
-diff --git a/test-suite/bugs/closed/4429.v b/test-suite/bugs/closed/4429.v
-deleted file mode 100644
-index bf0e570..0000000
---- a/test-suite/bugs/closed/4429.v
-+++ /dev/null
-@@ -1,31 +0,0 @@
--Require Import Arith.Compare_dec.
--Require Import Unicode.Utf8.
--
--Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
--  match n with
--    | O    => x
--    | S n' => f (my_nat_iter n' f x)
--  end.
--
--Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
--  match mn with
--    | (0, 0)       => 0
--    | (0, S n')    => S n'
--    | (S m', 0)    => S m'
--    | (S m', S n') =>
--      match le_gt_dec (S m') (S n') with
--        | left  _ => f (S m', S n' - S m')
--        | right _ => f (S m' - S n', S n')
--      end
--  end.
--
--Axiom max_correct_l : ∀ m n : nat, m <= max m n.
--Axiom max_correct_r : ∀ m n : nat, n <= max m n.
--
--Hint Resolve max_correct_l max_correct_r : arith.
--
--Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
--Proof.
--  intros.
--  Timeout 3 eauto with arith.
--Qed.
diff --git a/debian/patches/remove-heavy-tests.patch b/debian/patches/remove-heavy-tests.patch
new file mode 100644
index 00000000..2cc8e17c
--- /dev/null
+++ b/debian/patches/remove-heavy-tests.patch
@@ -0,0 +1,43 @@
+From: Benjamin Barenblat <bbaren@debian.org>
+Subject: Remove heavyweight tests
+Forwarded: not-needed
+
+Remove tests that use too much RAM or time to run on a buildd. (The MIPS
+buildd is frequently the culprit, as MIPS lacks an OCaml native
+compiler.)
+--- a/test-suite/bugs/closed/5127.v
++++ /dev/null
+@@ -1,15 +0,0 @@
+-Fixpoint arrow (n: nat) :=
+-  match n with
+-  | S n => bool -> arrow n
+-  | O => bool
+-  end.
+-
+-Fixpoint apply (n : nat) : arrow n -> bool :=
+-  match n return arrow n -> bool with
+-  | S n => fun f => apply _ (f true)
+-  | O => fun x => x
+-  end.
+-
+-Axiom f : arrow 10000.
+-Definition v : bool := Eval compute in apply _ f.
+-Definition w : bool := Eval vm_compute in v.
+--- a/test-suite/success/Nsatz.v
++++ b/test-suite/success/Nsatz.v
+@@ -462,6 +462,7 @@ idtac "chords".
+ (*Finished transaction in 4. secs (3.959398u,0.s)*)
+ Qed.
+ 
++(*
+ Lemma Ceva: forall A B C D E F M:point,
+   collinear M A D -> collinear M B E -> collinear M C F ->
+   collinear B C D -> collinear E A C -> collinear F A B ->
+@@ -473,6 +474,7 @@ idtac "Ceva".
+ Time nsatz.
+ (*Finished transaction in 105. secs (104.121171u,0.474928s)*)
+ Qed.
++*)
+ 
+ Lemma bissectrices: forall A B C M:point,
+   equaltangente C A M M A B ->
diff --git a/debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch b/debian/patches/remove-time-sensitive-tests.patch
index 45acd396..8a5d640b 100644
--- a/debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch
+++ b/debian/patches/remove-time-sensitive-tests.patch
@@ -1,6 +1,9 @@
-From: Enrico Tassi <gareuselesinge@debian.org>
-Date: Wed, 28 Dec 2016 18:18:34 +0100
-Subject: Remove 3441.v and 4811.v due to timeout on small platforms
+From: Benjamin Barenblat <bbaren@debian.org>
+Subject: Remove time-sensitive tests
+Forwarded: not-needed
+
+Remove tests that have tight timing bounds. These tests consistently run
+too slowly to pass on platforms without OCaml native compilers (MIPS).
 --- a/test-suite/bugs/closed/3441.v
 +++ /dev/null
 @@ -1,23 +0,0 @@
@@ -27,6 +30,40 @@ Subject: Remove 3441.v and 4811.v due to timeout on small platforms
 -     let x := constr:(let n := 17 in do_n n = do_n n) in
 -     let y := (eval lazy in x) in
 -     assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *)
+--- a/test-suite/bugs/closed/4429.v
++++ /dev/null
+@@ -1,31 +0,0 @@
+-Require Import Arith.Compare_dec.
+-Require Import Unicode.Utf8.
+-
+-Fixpoint my_nat_iter (n : nat) {A} (f : A → A) (x : A) : A :=
+-  match n with
+-    | O    => x
+-    | S n' => f (my_nat_iter n' f x)
+-  end.
+-
+-Definition gcd_IT_F (f : nat * nat → nat) (mn : nat * nat) : nat :=
+-  match mn with
+-    | (0, 0)       => 0
+-    | (0, S n')    => S n'
+-    | (S m', 0)    => S m'
+-    | (S m', S n') =>
+-      match le_gt_dec (S m') (S n') with
+-        | left  _ => f (S m', S n' - S m')
+-        | right _ => f (S m' - S n', S n')
+-      end
+-  end.
+-
+-Axiom max_correct_l : ∀ m n : nat, m <= max m n.
+-Axiom max_correct_r : ∀ m n : nat, n <= max m n.
+-
+-Hint Resolve max_correct_l max_correct_r : arith.
+-
+-Theorem foo : ∀ p p' p'' : nat, p'' < S (max p (max p' p'')).
+-Proof.
+-  intros.
+-  Timeout 3 eauto with arith.
+-Qed.
 --- a/test-suite/bugs/closed/4811.v
 +++ /dev/null
 @@ -1,1685 +0,0 @@
diff --git a/debian/patches/series b/debian/patches/series
index 4f1f3fcf..eb7aeee1 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1,7 +1,5 @@
-test-suite-success-Nsatz.v-comment-out-Ceva.patch
-Remove-test-4429.patch
-Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch
-5127-fails-on-mips.patch
+remove-heavy-tests.patch
+remove-time-sensitive-tests.patch
 remove-tests-that-need-coqlib.patch
 avoid-usr-bin-env.patch
 python-scripts-libraries.patch
diff --git a/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch
deleted file mode 100644
index 2cf6af5c..00000000
--- a/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch
+++ /dev/null
@@ -1,29 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Sun, 15 Jan 2012 12:34:19 +0100
-Subject: test-suite/success/Nsatz.v: comment out Ceva
-
-This lemma uses too much memory for many buildds...
----
- test-suite/success/Nsatz.v | 2 ++
- 1 file changed, 2 insertions(+)
-
-diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
-index e38affd..040169e 100644
---- a/test-suite/success/Nsatz.v
-+++ b/test-suite/success/Nsatz.v
-@@ -462,6 +462,7 @@ idtac "chords".
- (*Finished transaction in 4. secs (3.959398u,0.s)*)
- Qed.
- 
-+(*
- Lemma Ceva: forall A B C D E F M:point,
-   collinear M A D -> collinear M B E -> collinear M C F ->
-   collinear B C D -> collinear E A C -> collinear F A B ->
-@@ -473,6 +474,7 @@ idtac "Ceva".
- Time nsatz.
- (*Finished transaction in 105. secs (104.121171u,0.474928s)*)
- Qed.
-+*)
- 
- Lemma bissectrices: forall A B C M:point,
-   equaltangente C A M M A B ->