[Pkg-ocaml-maint-commits] [coq] 01/01: fix FTBFS on slow architectures by disabling 4429

[Enrico Tassi]

This is an automated email from the git hooks/post-receive script.

gareuselesinge pushed a commit to branch master
in repository coq.

commit 7c9b0a702976078b813e6493c1284af62a3f093c
Author: Enrico Tassi <gareuselesinge at debian.org>
Date:   Thu Jan 28 11:47:57 2016 +0100

    fix FTBFS on slow architectures by disabling 4429
---
 debian/changelog                           |  6 ++++
 debian/patches/0003-Remove-test-4429.patch | 46 ++++++++++++++++++++++++++++++
 debian/patches/series                      |  1 +
 3 files changed, 53 insertions(+)

diff --git a/debian/changelog b/debian/changelog
index 0d0bd9d..27fbb51 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 at 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 0000000..9baee30
--- /dev/null
+++ b/debian/patches/0003-Remove-test-4429.patch
@@ -0,0 +1,46 @@
+From: Enrico Tassi <gareuselesinge at 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 7521511..2fabc9f 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

-- 
Alioth's /usr/local/bin/git-commit-notice on /srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git