This is an automated email from the git hooks/post-receive script.
gareuselesinge pushed a commit to branch master
in repository coq.
commit ad20f9ab9a6f4d9e080b27571fa411aa68a53907
Author: Enrico Tassi <gareuselesi...@debian.org>
Date: Tue Jan 26 17:18:24 2016 +0100
8.5
---
debian/changelog | 7 +++++
...st-suite-success-Nsatz.v-comment-out-Ceva.patch | 7 +++--
...Remove-test-4366-too-picky-on-the-timeout.patch | 30 ++++++++++++++++++++++
debian/patches/series | 1 +
debian/rules | 2 +-
5 files changed, 42 insertions(+), 5 deletions(-)
diff --git a/debian/changelog b/debian/changelog
index 9e661d4..0d0bd9d 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,10 @@
+coq (8.5-1) unstable; urgency=medium
+
+ * New upstream release
+ * patch: disable test 4366 (timeout too strict for slow architectures)
+
+ -- Enrico Tassi <gareuselesi...@debian.org> Tue, 26 Jan 2016 16:59:05 +0100
+
coq (8.5~beta3+dfsg-2) experimental; urgency=medium
* Option -no-native-compiler now called -native-compiler no
diff --git
a/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
index 198188e..2cf6af5 100644
--- a/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
+++ b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
@@ -8,10 +8,10 @@ This lemma uses too much memory for many buildds...
1 file changed, 2 insertions(+)
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
-index d316e4a..d783b2a 100644
+index e38affd..040169e 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
-@@ -461,6 +461,7 @@ idtac "chords".
+@@ -462,6 +462,7 @@ idtac "chords".
(*Finished transaction in 4. secs (3.959398u,0.s)*)
Qed.
@@ -19,7 +19,7 @@ index d316e4a..d783b2a 100644
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 ->
-@@ -472,6 +473,7 @@ idtac "Ceva".
+@@ -473,6 +474,7 @@ idtac "Ceva".
Time nsatz.
(*Finished transaction in 105. secs (104.121171u,0.474928s)*)
Qed.
@@ -27,4 +27,3 @@ index d316e4a..d783b2a 100644
Lemma bissectrices: forall A B C M:point,
equaltangente C A M M A B ->
---
diff --git
a/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch
b/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch
new file mode 100644
index 0000000..e71306c
--- /dev/null
+++ b/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch
@@ -0,0 +1,30 @@
+From: Enrico Tassi <gareuselesi...@debian.org>
+Date: Tue, 26 Jan 2016 16:58:25 +0100
+Subject: Remove test 4366 (too picky on the timeout)
+
+---
+ test-suite/bugs/closed/4366.v | 15 ---------------
+ 1 file changed, 15 deletions(-)
+ delete mode 100644 test-suite/bugs/closed/4366.v
+
+diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v
+deleted file mode 100644
+index 6a5e9a4..0000000
+--- a/test-suite/bugs/closed/4366.v
++++ /dev/null
+@@ -1,15 +0,0 @@
+-Fixpoint stupid (n : nat) : unit :=
+-match n with
+-| 0 => tt
+-| S n =>
+- let () := stupid n in
+- let () := stupid n in
+- tt
+-end.
+-
+-Goal True.
+-Proof.
+-pose (v := stupid 24).
+-Timeout 2 vm_compute in v.
+-exact I.
+-Qed.
diff --git a/debian/patches/series b/debian/patches/series
index 53d51a1..7521511 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -1 +1,2 @@
0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
+0002-Remove-test-4366-too-picky-on-the-timeout.patch
diff --git a/debian/rules b/debian/rules
index 7944985..4cf2f8f 100755
--- a/debian/rules
+++ b/debian/rules
@@ -22,7 +22,7 @@ ADDPREF := COQINSTALLPREFIX=$(COQPREF) OLDROOT=
PACKAGES := $(shell dh_listpackages)
-COQ_VERSION := 8.5beta3
+COQ_VERSION := 8.5
COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI)
ARCH := $(shell dpkg-architecture -q DEB_TARGET_ARCH)
--
Alioth's /usr/local/bin/git-commit-notice on
/srv/git.debian.org/git/pkg-ocaml-maint/packages/coq.git
_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
