diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-01-28 11:47:57 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-28 11:47:57 +0100 |
| commit | 7c9b0a702976078b813e6493c1284af62a3f093c (patch) | |
| tree | 5d8be36e1541f17bd76dcc54f1189db561582e8f | |
| parent | ad20f9ab9a6f4d9e080b27571fa411aa68a53907 (diff) | |
fix FTBFS on slow architectures by disabling 4429debian/8.5-2
| -rw-r--r-- | debian/changelog | 6 | ||||
| -rw-r--r-- | debian/patches/0003-Remove-test-4429.patch | 46 | ||||
| -rw-r--r-- | debian/patches/series | 1 |
3 files changed, 53 insertions, 0 deletions
diff --git a/debian/changelog b/debian/changelog index 0d0bd9da..27fbb510 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +coq (8.5-2) unstable; urgency=medium + + * patch: disable test 4429 (timeout too strict for slow architectures) + + -- Enrico Tassi <gareuselesinge@debian.org> Thu, 28 Jan 2016 11:47:07 +0100 + coq (8.5-1) unstable; urgency=medium * New upstream release diff --git a/debian/patches/0003-Remove-test-4429.patch b/debian/patches/0003-Remove-test-4429.patch new file mode 100644 index 00000000..9baee306 --- /dev/null +++ b/debian/patches/0003-Remove-test-4429.patch @@ -0,0 +1,46 @@ +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/series b/debian/patches/series index 75215115..2fabc9f2 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,2 +1,3 @@ 0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch 0002-Remove-test-4366-too-picky-on-the-timeout.patch +0003-Remove-test-4429.patch |