diff options
Diffstat (limited to 'debian')
-rw-r--r-- | debian/README.source | 10 | ||||
-rw-r--r-- | debian/changelog | 60 | ||||
-rw-r--r-- | debian/clean | 1 | ||||
-rw-r--r-- | debian/control | 3 | ||||
-rw-r--r-- | debian/copyright | 36 | ||||
-rw-r--r-- | debian/coqide.dirs | 4 | ||||
-rw-r--r-- | debian/coqide.docs | 1 | ||||
-rw-r--r-- | debian/coqide.install | 6 | ||||
-rw-r--r-- | debian/gbp.conf | 16 | ||||
-rw-r--r-- | debian/libcoq-ocaml.install.in | 4 | ||||
-rw-r--r-- | debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch | 30 | ||||
-rw-r--r-- | debian/patches/series | 1 | ||||
-rwxr-xr-x | debian/rules | 3 | ||||
-rw-r--r-- | debian/watch | 6 |
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 |