diff options
| -rw-r--r-- | debian/patches/5127-fails-on-mips.patch | 30 | ||||
| -rw-r--r-- | debian/patches/Remove-test-4429.patch | 46 | ||||
| -rw-r--r-- | debian/patches/remove-heavy-tests.patch | 43 | ||||
| -rw-r--r-- | debian/patches/remove-time-sensitive-tests.patch (renamed from debian/patches/Remove-3441.v-and-4811.v-due-to-timeout-on-small-pla.patch) | 43 | ||||
| -rw-r--r-- | debian/patches/series | 6 | ||||
| -rw-r--r-- | debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch | 29 |
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 -> |