Merge branch 'experimental/master'

14 files changed, 143 insertions, 38 deletions

diff --git a/debian/README.source b/debian/README.source
index ab1f26cd..37984e0b 100644
--- a/debian/README.source
+++ b/debian/README.source
@@ -16,10 +16,10 @@ Only coqdoc-generated documentation of the standard library is shipped
 in main. The full documentation is shipped in non-free (as coq-doc
 package).
 
-The script debian/purify_tarball removes non-DFSG content from an
-upstream tarball. It should be run first when packaging a new upstream
-version. The suffix "+dfsg" is used to being appended to upstream
-version (the script will do it for you).
+The git-import-orig tool automatically filters out problematic files,
+thanks to the configuration in debian/gbp.conf. It is suggested to
+append the "dfsg" suffix to the upstream version to make repackaging
+explicit.
 
 
 Patch system
@@ -53,4 +53,4 @@ to ../coq.cache, and debian/rules will detect its presence and rsync
 from there instead of really compiling Coq...
 
 
- -- Stéphane Glondu <glondu@debian.org>, Mon, 31 May 2010 15:30:50 +0200
+ -- Stéphane Glondu <glondu@debian.org>, Mon, 20 Aug 2012 18:20:18 +0200
diff --git a/debian/changelog b/debian/changelog
index 5caa0f72..91ce92b7 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,63 @@
+coq (8.4pl2dfsg-1) UNRELEASED; urgency=low
+
+  * New upstream release
+
+ -- Stéphane Glondu <glondu@debian.org>  Wed, 08 May 2013 17:47:25 +0200
+
+coq (8.4pl1dfsg-1) experimental; urgency=low
+
+  * New upstream release
+    - 0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch
+      has been merged upstream
+    - add ocaml-findlib to Build-Depends
+
+ -- Stéphane Glondu <glondu@debian.org>  Sat, 29 Dec 2012 15:56:53 +0100
+
+coq (8.4dfsg-2) experimental; urgency=low
+
+  * Upstream bugfix: Fix use of $(HASNATDYNLINK) in coq_makefile output
+
+ -- Stéphane Glondu <glondu@debian.org>  Sat, 22 Sep 2012 12:43:13 +0200
+
+coq (8.4dfsg-1) experimental; urgency=low
+
+  * New upstream release
+
+ -- Stéphane Glondu <glondu@debian.org>  Mon, 20 Aug 2012 18:33:45 +0200
+
+coq (8.4~gamma0+really8.4beta2+dfsg-1) experimental; urgency=low
+
+  * New upstream beta release
+
+ -- Stéphane Glondu <glondu@debian.org>  Tue, 05 Jun 2012 07:38:25 +0200
+
+coq (8.4~beta+dfsg-4) experimental; urgency=low
+
+  * Recompile with camlp5 6.05 (no changes)
+
+ -- Stéphane Glondu <glondu@debian.org>  Fri, 06 Apr 2012 10:04:06 +0200
+
+coq (8.4~beta+dfsg-3) experimental; urgency=low
+
+  * Replace proofgeneral-coq by proofgeneral in dependencies
+  * Disable a test that uses too much memory, causing random FTBFS
+
+ -- Stéphane Glondu <glondu@debian.org>  Sun, 15 Jan 2012 12:37:23 +0100
+
+coq (8.4~beta+dfsg-2) experimental; urgency=low
+
+  * Fix a typo that caused decl_mode_plugin.cmxs not being installed,
+    making coqtop.opt useless
+  * Fix an ordering issue that was causing a test to fail in bytecode
+
+ -- Stéphane Glondu <glondu@debian.org>  Sat, 14 Jan 2012 11:11:48 +0100
+
+coq (8.4~beta+dfsg-1) experimental; urgency=low
+
+  * New upstream beta release
+
+ -- Stéphane Glondu <glondu@debian.org>  Thu, 12 Jan 2012 18:53:08 +0100
+
 coq (8.3.pl4+dfsg-2) unstable; urgency=low
 
   * Recompile with camlp5 6.06 (no changes)
diff --git a/debian/clean b/debian/clean
deleted file mode 100644
index 7c32f559..00000000
--- a/debian/clean
+++ /dev/null
@@ -1 +0,0 @@
-install
diff --git a/debian/control b/debian/control
index 2e104f03..d314e2c3 100644
--- a/debian/control
+++ b/debian/control
@@ -6,12 +6,13 @@ Uploaders:
  Ralf Treinen <treinen@debian.org>,
  Samuel Mimram <smimram@debian.org>,
  Stéphane Glondu <glondu@debian.org>
-Standards-Version: 3.9.3
+Standards-Version: 3.9.2
 Build-Depends:
  debhelper (>= 7.2.11~),
  dh-ocaml (>= 0.9.5~),
  ocaml-nox (>= 3.11.1-3~),
  ocaml-best-compilers,
+ ocaml-findlib,
  camlp5 (>= 5.12-2~),
  liblablgtk2-ocaml-dev (>= 2.14),
  texlive-latex-extra,
diff --git a/debian/copyright b/debian/copyright
index 4a84b1db..6ff2511f 100644
--- a/debian/copyright
+++ b/debian/copyright
@@ -1,23 +1,25 @@
-Format: http://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
-
-License: LGPL-2.1
- The Coq Proof Assistant is distributed under the terms of the GNU
- Lesser General Public Licence, version 2.1, see
- /usr/share/common-licenses/LGPL-2.1.
+Packaged-By: Fernando Sanchez <fer@debian.org>
+Packaged-Date: Fri, 03 Dec 1999 22:06:04 +0100
+Original-Source-Location: http://coq.inria.fr/
 
 Files: *
-Copyright: 1999-2010, The Coq development team,
-                      INRIA, CNRS, University Paris Sud,
-                      University Paris 7, Ecole Polytechnique.
+Copyright: © 1999-2010 The Coq development team,
+                       INRIA, CNRS, University Paris Sud,
+                       University Paris 7, Ecole Polytechnique.
 License: LGPL-2.1
- This product includes also software developed by
-   Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
-   Pierre Courtieu and Julien Forest, CNAM (plugins/funind)
-   Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
-   Pierre Corbineau, Radbout University, Nijmegen (declarative mode)
-   John Harrison, University of Cambridge (csdp wrapper)
- .
- The file /usr/share/doc/coq/CREDITS.gz contains a list of contributors.
+
+  This product includes also software developed by
+    Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega)
+    Pierre Courtieu and Julien Forest, CNAM (plugins/funind)
+    Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml)
+    Pierre Corbineau, Radbout University, Nijmegen (declarative mode)
+    John Harrison, University of Cambridge (csdp wrapper)
+
+  The file /usr/share/doc/coq/CREDITS.gz contains a list of contributors.
+
+  The Coq Proof Assistant is distributed under the terms of the GNU
+  Lesser General Public Licence, version 2.1, see
+  /usr/share/common-licenses/LGPL-2.1.
 
 Files: debian/*
 Copyright: © 1999-2000 Fernando Sanchez <fer@debian.org>
diff --git a/debian/coqide.dirs b/debian/coqide.dirs
index bf32ae9c..c1da623a 100644
--- a/debian/coqide.dirs
+++ b/debian/coqide.dirs
@@ -1,5 +1 @@
-usr/lib/coq/ide
-usr/share/doc/coqide
-usr/share/applications
-usr/share/man/man1
 usr/share/pixmaps
diff --git a/debian/coqide.docs b/debian/coqide.docs
deleted file mode 100644
index 6fcc323e..00000000
--- a/debian/coqide.docs
+++ /dev/null
@@ -1 +0,0 @@
-ide/FAQ
diff --git a/debian/coqide.install b/debian/coqide.install
index fc5b80fe..4336ff03 100644
--- a/debian/coqide.install
+++ b/debian/coqide.install
@@ -1,6 +1,6 @@
 usr/bin/coqide*
-usr/lib/coq/ide/coq.png
-usr/lib/coq/ide/.coqide-gtk2rc
-usr/lib/coq/ide/FAQ
+usr/share/coq/coq.png
+etc/xdg/coq/coqide-gtk2rc
+usr/share/doc/coq/FAQ-CoqIde usr/share/doc/coqide
 usr/share/man/man1/coqide*
 debian/coqide.desktop    usr/share/applications
diff --git a/debian/gbp.conf b/debian/gbp.conf
index cec628c7..126a7b7a 100644
--- a/debian/gbp.conf
+++ b/debian/gbp.conf
@@ -1,2 +1,18 @@
 [DEFAULT]
 pristine-tar = True
+filter-pristine-tar = True
+filter = [
+    "doc/common/styles/html/coqremote/cover.html",
+    "doc/common/styles/html/coqremote/hevea.css",
+    "doc/common/styles/html/coqremote/styles.hva",
+    "doc/common/styles/html/simple/cover.html",
+    "doc/common/styles/html/simple/hevea.css",
+    "doc/common/styles/html/simple/styles.hva",
+    "doc/common/macros.tex",
+    "doc/common/title.tex",
+    "doc/RecTutorial",
+    "doc/faq",
+    "doc/refman",
+    "doc/rt",
+    "doc/tools",
+    "doc/tutorial" ]
diff --git a/debian/libcoq-ocaml.install.in b/debian/libcoq-ocaml.install.in
index 746a3577..07fca0ac 100644
--- a/debian/libcoq-ocaml.install.in
+++ b/debian/libcoq-ocaml.install.in
@@ -13,7 +13,6 @@ usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cma
 usr/lib/coq/plugins/funind/recdef_plugin.cma
 usr/lib/coq/plugins/nsatz/nsatz_plugin.cma
 usr/lib/coq/plugins/xml/xml_plugin.cma
-usr/lib/coq/plugins/dp/dp_plugin.cma
 usr/lib/coq/plugins/romega/romega_plugin.cma
 usr/lib/coq/plugins/firstorder/ground_plugin.cma
 usr/lib/coq/plugins/subtac/subtac_plugin.cma
@@ -22,6 +21,7 @@ usr/lib/coq/plugins/rtauto/rtauto_plugin.cma
 usr/lib/coq/plugins/setoid_ring/newring_plugin.cma
 usr/lib/coq/plugins/micromega/micromega_plugin.cma
 usr/lib/coq/plugins/quote/quote_plugin.cma
+usr/lib/coq/plugins/decl_mode/decl_mode_plugin.cma
 DYN: usr/lib/coq/plugins/ring/ring_plugin.cmxs
 DYN: usr/lib/coq/plugins/fourier/fourier_plugin.cmxs
 DYN: usr/lib/coq/plugins/extraction/extraction_plugin.cmxs
@@ -36,7 +36,6 @@ DYN: usr/lib/coq/plugins/syntax/ascii_syntax_plugin.cmxs
 DYN: usr/lib/coq/plugins/funind/recdef_plugin.cmxs
 DYN: usr/lib/coq/plugins/nsatz/nsatz_plugin.cmxs
 DYN: usr/lib/coq/plugins/xml/xml_plugin.cmxs
-DYN: usr/lib/coq/plugins/dp/dp_plugin.cmxs
 DYN: usr/lib/coq/plugins/romega/romega_plugin.cmxs
 DYN: usr/lib/coq/plugins/firstorder/ground_plugin.cmxs
 DYN: usr/lib/coq/plugins/subtac/subtac_plugin.cmxs
@@ -45,3 +44,4 @@ DYN: usr/lib/coq/plugins/rtauto/rtauto_plugin.cmxs
 DYN: usr/lib/coq/plugins/setoid_ring/newring_plugin.cmxs
 DYN: usr/lib/coq/plugins/micromega/micromega_plugin.cmxs
 DYN: usr/lib/coq/plugins/quote/quote_plugin.cmxs
+DYN: usr/lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs
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
new file mode 100644
index 00000000..722ab00c
--- /dev/null
+++ b/debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
@@ -0,0 +1,30 @@
+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 d316e4a..d783b2a 100644
+--- a/test-suite/success/Nsatz.v
++++ b/test-suite/success/Nsatz.v
+@@ -461,6 +461,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 ->
+@@ -472,6 +473,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/series b/debian/patches/series
new file mode 100644
index 00000000..53d51a16
--- /dev/null
+++ b/debian/patches/series
@@ -0,0 +1 @@
+0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch
diff --git a/debian/rules b/debian/rules
index 3e9a8830..4a033c89 100755
--- a/debian/rules
+++ b/debian/rules
@@ -22,10 +22,11 @@ ADDPREF := COQINSTALLPREFIX=$(COQPREF) OLDROOT=
 
 PACKAGES := $(shell dh_listpackages)
 
-COQ_VERSION := 8.3pl4
+COQ_VERSION := 8.4pl2
 COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI)
 
 CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \
+  --configdir /etc/xdg/coq \
   --emacslib /usr/share/emacs/site-lisp/coq \
   --browser "/usr/bin/x-www-browser %s &" \
   --with-doc no --coqrunbyteflags "-dllib -lcoqrun"
diff --git a/debian/watch b/debian/watch
index 37d70519..5d9c70de 100644
--- a/debian/watch
+++ b/debian/watch
@@ -1,4 +1,4 @@
 version=3
-
-opts=uversionmangle=s/pl/.pl/,dversionmangle=s/\+dfsg\d*$// \
-        http://coq.inria.fr/download distrib/[^/]+/files/coq-(.*)\.tar\.gz
+opts=dversionmangle=s/\+?(debian|dfsg|ds|deb)\d*$// \
+http://coq.inria.fr/download .*/coq-(\d.*)\.(?:tgz|tbz2|txz|tar\.(?:gz|bz2|xz))
+# Bart Martens <bartm@debian.org>  Sun, 30 Dec 2012 20:22:30 +0000