From d3ba3713b521ffe82e95d50d2948dba088b5a78b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:09:19 +0100 Subject: New upstream beta release --- debian/changelog | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index 4ff1a521..c3da9fbf 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +coq (8.4~beta+dfsg-1) UNRELEASED; urgency=low + + * New upstream beta release + + -- Stéphane Glondu Thu, 12 Jan 2012 16:09:13 +0100 + coq (8.3.pl3+dfsg-1) unstable; urgency=low * New upstream release -- cgit v1.2.3 From f231ae59d9189649cb69262376b2f2dab4b543a2 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:30:22 +0100 Subject: Add distclean target to test-suite/Makefile --- ...Add-distclean-back-to-test-suite-Makefile.patch | 23 ++++++++++++++++++++++ debian/patches/series | 1 + 2 files changed, 24 insertions(+) create mode 100644 debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch create mode 100644 debian/patches/series (limited to 'debian') diff --git a/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch b/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch new file mode 100644 index 00000000..80cd27ae --- /dev/null +++ b/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch @@ -0,0 +1,23 @@ +From: Stephane Glondu +Date: Thu, 12 Jan 2012 16:30:10 +0100 +Subject: Add distclean back to test-suite/Makefile + +--- + test-suite/Makefile | 3 +++ + 1 files changed, 3 insertions(+), 0 deletions(-) + +diff --git a/test-suite/Makefile b/test-suite/Makefile +index cd5886f..f3013c0 100644 +--- a/test-suite/Makefile ++++ b/test-suite/Makefile +@@ -97,6 +97,9 @@ clean: + -name '*.stamp' -o -name '*.vo' -o -name '*.log' \ + \) -print0 | xargs -0 rm -f + ++distclean: clean ++ $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f ++ + ####################################################################### + # Per-subsystem targets + ####################################################################### +-- diff --git a/debian/patches/series b/debian/patches/series new file mode 100644 index 00000000..1d411110 --- /dev/null +++ b/debian/patches/series @@ -0,0 +1 @@ +0001-Add-distclean-back-to-test-suite-Makefile.patch -- cgit v1.2.3 From 4ac272f0121ba8f3ab48a18c8225b44b03bba4f7 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 17:37:10 +0100 Subject: Miscellaneous updates --- debian/clean | 1 - debian/coqide.dirs | 4 ---- debian/coqide.docs | 1 - debian/coqide.install | 6 +++--- debian/libcoq-ocaml.install.in | 2 ++ debian/rules | 3 ++- 6 files changed, 7 insertions(+), 10 deletions(-) delete mode 100644 debian/clean delete mode 100644 debian/coqide.docs (limited to 'debian') 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/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/libcoq-ocaml.install.in b/debian/libcoq-ocaml.install.in index 746a3577..9459116f 100644 --- a/debian/libcoq-ocaml.install.in +++ b/debian/libcoq-ocaml.install.in @@ -22,6 +22,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 @@ -45,3 +46,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.cma diff --git a/debian/rules b/debian/rules index a364ad70..379cb28f 100755 --- a/debian/rules +++ b/debian/rules @@ -22,10 +22,11 @@ ADDPREF := COQINSTALLPREFIX=$(COQPREF) OLDROOT= PACKAGES := $(shell dh_listpackages) -COQ_VERSION := 8.3pl3 +COQ_VERSION := 8.4beta 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" -- cgit v1.2.3 From 740160e590c78840860ee145a0260952507992dc Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 18:53:24 +0100 Subject: Prepare upload to experimental --- debian/changelog | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index c3da9fbf..23e20ced 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,8 +1,8 @@ -coq (8.4~beta+dfsg-1) UNRELEASED; urgency=low +coq (8.4~beta+dfsg-1) experimental; urgency=low * New upstream beta release - -- Stéphane Glondu Thu, 12 Jan 2012 16:09:13 +0100 + -- Stéphane Glondu Thu, 12 Jan 2012 18:53:08 +0100 coq (8.3.pl3+dfsg-1) unstable; urgency=low -- cgit v1.2.3 From 64007d9eae3bfe88341db8995698aa86a50faa37 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 13 Jan 2012 16:07:02 +0100 Subject: Fix typo (shame...) --- debian/libcoq-ocaml.install.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'debian') diff --git a/debian/libcoq-ocaml.install.in b/debian/libcoq-ocaml.install.in index 9459116f..c6507720 100644 --- a/debian/libcoq-ocaml.install.in +++ b/debian/libcoq-ocaml.install.in @@ -46,4 +46,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.cma +DYN: usr/lib/coq/plugins/decl_mode/decl_mode_plugin.cmxs -- cgit v1.2.3 From 5872768853f8c78187a3daaa89f09e674c90fa07 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 14 Jan 2012 11:13:29 +0100 Subject: Call dh_install with --fail-missing --- debian/rules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'debian') diff --git a/debian/rules b/debian/rules index 379cb28f..4ed4e3a3 100755 --- a/debian/rules +++ b/debian/rules @@ -83,7 +83,7 @@ override_dh_auto_install: .PHONY: override_dh_install override_dh_install: - dh_install --list-missing + dh_install --fail-missing cp debian/coq.xpm debian/coqide/usr/share/pixmaps/coqide.xpm .PHONY: override_dh_gencontrol -- cgit v1.2.3 From 4331c26d60d7109f49d082113d40b896ea6a1fae Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 14 Jan 2012 02:51:40 +0100 Subject: Fix an ordering issue that was causing a test to fail in bytecode --- ...ga.ml-fix-order-of-recursive-calls-to-rco.patch | 31 ++++++++++++++++++++++ debian/patches/series | 1 + 2 files changed, 32 insertions(+) create mode 100644 debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch (limited to 'debian') diff --git a/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch b/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch new file mode 100644 index 00000000..3307023d --- /dev/null +++ b/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch @@ -0,0 +1,31 @@ +From: Stephane Glondu +Date: Sat, 14 Jan 2012 01:24:30 +0100 +Subject: coq_micromega.ml: fix order of recursive calls to rconstant + +Some tests were failing on architectures without native code because +the evaluation order of arguments in a function call is not the same +on bytecode, leading to different behaviours for the psatzl tactic. +--- + plugins/micromega/coq_micromega.ml | 8 ++++++-- + 1 files changed, 6 insertions(+), 2 deletions(-) + +diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml +index 1ad49bb..543ab1b 100644 +--- a/plugins/micromega/coq_micromega.ml ++++ b/plugins/micromega/coq_micromega.ml +@@ -991,8 +991,12 @@ struct + else raise ParseError + | App(op,args) -> + begin +- try +- (assoc_const op rconst_assoc) (rconstant args.(0)) (rconstant args.(1)) ++ try ++ (* the evaluation order is important in the following *) ++ let f = assoc_const op rconst_assoc in ++ let a = rconstant args.(0) in ++ let b = rconstant args.(1) in ++ f a b + with + ParseError -> + match op with +-- diff --git a/debian/patches/series b/debian/patches/series index 1d411110..41965593 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1 +1,2 @@ 0001-Add-distclean-back-to-test-suite-Makefile.patch +0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch -- cgit v1.2.3 From 144b0828b16f2ddde3c34aaccb59a70d8f977fae Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 14 Jan 2012 02:52:18 +0100 Subject: Update changelog and prepare upload to experimental --- debian/changelog | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index 23e20ced..a881bf77 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,11 @@ +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 Sat, 14 Jan 2012 11:11:48 +0100 + coq (8.4~beta+dfsg-1) experimental; urgency=low * New upstream beta release -- cgit v1.2.3 From 899e0b980396967970b15d062985dca7e29c59d3 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 14 Jan 2012 15:11:23 +0100 Subject: proofgeneral-coq has been dropped in favour of proofgeneral --- debian/control | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'debian') diff --git a/debian/control b/debian/control index 98b15dc2..f2a5e66b 100644 --- a/debian/control +++ b/debian/control @@ -29,10 +29,10 @@ Depends: ${shlibs:Depends}, ${misc:Depends} Provides: coq-${F:CoqABI} -Recommends: coqide | proofgeneral-coq +Recommends: coqide | proofgeneral Suggests: ocaml-nox, - proofgeneral-coq, + proofgeneral, ledit | readline-editor, libcoq-ocaml-dev, why (>= 2.19), @@ -48,7 +48,7 @@ Description: proof assistant for higher-order logic (toplevel and compiler) . A graphical interface for Coq is provided in the coqide package. Coq can also be used with ProofGeneral, which allows proofs to be - edited using emacs and xemacs. This requires the proofgeneral-coq + edited using emacs and xemacs. This requires the proofgeneral package to be installed. Package: coqide -- cgit v1.2.3 From 5eb084011ecf23993159a2e1e057ecdb7d7aa06f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 15 Jan 2012 12:36:33 +0100 Subject: Disable a test that uses too much memory --- ...st-suite-success-Nsatz.v-comment-out-Ceva.patch | 30 ++++++++++++++++++++++ debian/patches/series | 1 + 2 files changed, 31 insertions(+) create mode 100644 debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch (limited to 'debian') diff --git a/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch new file mode 100644 index 00000000..6969f7dd --- /dev/null +++ b/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch @@ -0,0 +1,30 @@ +From: Stephane Glondu +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 files changed, 2 insertions(+), 0 deletions(-) + +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 index 41965593..b0df385f 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,2 +1,3 @@ 0001-Add-distclean-back-to-test-suite-Makefile.patch 0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch +0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch -- cgit v1.2.3 From d136352525babcff56d1a7c9ac018c6c6c7443a4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 15 Jan 2012 12:37:44 +0100 Subject: Update changelog and prepare upload to experimental --- debian/changelog | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index a881bf77..23e77f2a 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,10 @@ +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 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, -- cgit v1.2.3 From ff61c7f8b0cbe6f0173720e08a63142a3146cc53 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Apr 2012 10:04:14 +0200 Subject: Recompile with camlp5 6.05 (no changes) --- debian/changelog | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index 23e77f2a..5f365100 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +coq (8.4~beta+dfsg-4) experimental; urgency=low + + * Recompile with camlp5 6.05 (no changes) + + -- Stéphane Glondu Fri, 06 Apr 2012 10:04:06 +0200 + coq (8.4~beta+dfsg-3) experimental; urgency=low * Replace proofgeneral-coq by proofgeneral in dependencies -- cgit v1.2.3 From 3a10a27a477f3df2f3f51a1011fef318ff4f5f58 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:26:25 +0200 Subject: New upstream beta release --- debian/changelog | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index 5f365100..698bd42f 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +coq (8.4~gamma0+really8.4beta2+dfsg-1) UNRELEASED; urgency=low + + * New upstream beta release + + -- Stéphane Glondu Mon, 04 Jun 2012 12:26:18 +0200 + coq (8.4~beta+dfsg-4) experimental; urgency=low * Recompile with camlp5 6.05 (no changes) -- cgit v1.2.3 From 4c3793181d62c1e4c883cea7547ee04ea423fbe4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 12:28:06 +0200 Subject: Refresh patches --- ...Add-distclean-back-to-test-suite-Makefile.patch | 23 ---------------- ...st-suite-success-Nsatz.v-comment-out-Ceva.patch | 30 +++++++++++++++++++++ ...ga.ml-fix-order-of-recursive-calls-to-rco.patch | 31 ---------------------- ...st-suite-success-Nsatz.v-comment-out-Ceva.patch | 30 --------------------- debian/patches/series | 4 +-- 5 files changed, 31 insertions(+), 87 deletions(-) delete mode 100644 debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch create mode 100644 debian/patches/0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch delete mode 100644 debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch delete mode 100644 debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch (limited to 'debian') diff --git a/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch b/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch deleted file mode 100644 index 80cd27ae..00000000 --- a/debian/patches/0001-Add-distclean-back-to-test-suite-Makefile.patch +++ /dev/null @@ -1,23 +0,0 @@ -From: Stephane Glondu -Date: Thu, 12 Jan 2012 16:30:10 +0100 -Subject: Add distclean back to test-suite/Makefile - ---- - test-suite/Makefile | 3 +++ - 1 files changed, 3 insertions(+), 0 deletions(-) - -diff --git a/test-suite/Makefile b/test-suite/Makefile -index cd5886f..f3013c0 100644 ---- a/test-suite/Makefile -+++ b/test-suite/Makefile -@@ -97,6 +97,9 @@ clean: - -name '*.stamp' -o -name '*.vo' -o -name '*.log' \ - \) -print0 | xargs -0 rm -f - -+distclean: clean -+ $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f -+ - ####################################################################### - # Per-subsystem targets - ####################################################################### --- 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 +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/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch b/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch deleted file mode 100644 index 3307023d..00000000 --- a/debian/patches/0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch +++ /dev/null @@ -1,31 +0,0 @@ -From: Stephane Glondu -Date: Sat, 14 Jan 2012 01:24:30 +0100 -Subject: coq_micromega.ml: fix order of recursive calls to rconstant - -Some tests were failing on architectures without native code because -the evaluation order of arguments in a function call is not the same -on bytecode, leading to different behaviours for the psatzl tactic. ---- - plugins/micromega/coq_micromega.ml | 8 ++++++-- - 1 files changed, 6 insertions(+), 2 deletions(-) - -diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml -index 1ad49bb..543ab1b 100644 ---- a/plugins/micromega/coq_micromega.ml -+++ b/plugins/micromega/coq_micromega.ml -@@ -991,8 +991,12 @@ struct - else raise ParseError - | App(op,args) -> - begin -- try -- (assoc_const op rconst_assoc) (rconstant args.(0)) (rconstant args.(1)) -+ try -+ (* the evaluation order is important in the following *) -+ let f = assoc_const op rconst_assoc in -+ let a = rconstant args.(0) in -+ let b = rconstant args.(1) in -+ f a b - with - ParseError -> - match op with --- diff --git a/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch deleted file mode 100644 index 6969f7dd..00000000 --- a/debian/patches/0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch +++ /dev/null @@ -1,30 +0,0 @@ -From: Stephane Glondu -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 files changed, 2 insertions(+), 0 deletions(-) - -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 index b0df385f..53d51a16 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,3 +1 @@ -0001-Add-distclean-back-to-test-suite-Makefile.patch -0002-coq_micromega.ml-fix-order-of-recursive-calls-to-rco.patch -0003-test-suite-success-Nsatz.v-comment-out-Ceva.patch +0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch -- cgit v1.2.3 From c467035933a683a7b7ac214fc511604735f15e7f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 14:18:02 +0200 Subject: Update ABI --- debian/rules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'debian') diff --git a/debian/rules b/debian/rules index 4ed4e3a3..d885ece6 100755 --- a/debian/rules +++ b/debian/rules @@ -22,7 +22,7 @@ ADDPREF := COQINSTALLPREFIX=$(COQPREF) OLDROOT= PACKAGES := $(shell dh_listpackages) -COQ_VERSION := 8.4beta +COQ_VERSION := 8.4beta2 COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI) CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \ -- cgit v1.2.3 From 9ba360bc40800295fd8f706a4d561805c2e4c8db Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 4 Jun 2012 15:03:22 +0200 Subject: Dp plugin has been dropped --- debian/libcoq-ocaml.install.in | 2 -- 1 file changed, 2 deletions(-) (limited to 'debian') diff --git a/debian/libcoq-ocaml.install.in b/debian/libcoq-ocaml.install.in index c6507720..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 @@ -37,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 -- cgit v1.2.3 From 509d6d4b58f50b86ca482d49fb6b2fee7fc3dfe9 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Tue, 5 Jun 2012 07:38:34 +0200 Subject: Prepare upload to experimental --- debian/changelog | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index 698bd42f..a67dc785 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,8 +1,8 @@ -coq (8.4~gamma0+really8.4beta2+dfsg-1) UNRELEASED; urgency=low +coq (8.4~gamma0+really8.4beta2+dfsg-1) experimental; urgency=low * New upstream beta release - -- Stéphane Glondu Mon, 04 Jun 2012 12:26:18 +0200 + -- Stéphane Glondu Tue, 05 Jun 2012 07:38:25 +0200 coq (8.4~beta+dfsg-4) experimental; urgency=low -- cgit v1.2.3 From 72deb90ec0aca34501f0476c013e2cee7ccd1f2a Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:18:30 +0200 Subject: Use filter-pristine-tar and change versioning scheme --- debian/README.source | 10 +++++----- debian/gbp.conf | 16 ++++++++++++++++ debian/watch | 4 ++-- 3 files changed, 23 insertions(+), 7 deletions(-) (limited to 'debian') 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 , Mon, 31 May 2010 15:30:50 +0200 + -- Stéphane Glondu , Mon, 20 Aug 2012 18:20:18 +0200 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/watch b/debian/watch index 37d70519..07bcf5fe 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/dfsg$// \ + http://coq.inria.fr/download .*/coq-(.*)\.tar\.gz -- cgit v1.2.3 From ab08ae9f0f944d9f801c44e4ffd3e6b7fcf4b024 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:25:30 +0200 Subject: Use experimental branches --- debian/gbp.conf | 2 ++ 1 file changed, 2 insertions(+) (limited to 'debian') diff --git a/debian/gbp.conf b/debian/gbp.conf index 126a7b7a..68cfceb8 100644 --- a/debian/gbp.conf +++ b/debian/gbp.conf @@ -16,3 +16,5 @@ filter = [ "doc/rt", "doc/tools", "doc/tutorial" ] +upstream-branch=experimental/upstream +debian-branch=experimental/master -- cgit v1.2.3 From 65f39a78452feed5f4138ffd4846356b9bc57439 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:27:39 +0200 Subject: New upstream release --- debian/changelog | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index a67dc785..6dc59d00 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +coq (8.4dfsg-1) UNRELEASED; urgency=low + + * New upstream release + + -- Stéphane Glondu Mon, 20 Aug 2012 18:27:33 +0200 + coq (8.4~gamma0+really8.4beta2+dfsg-1) experimental; urgency=low * New upstream beta release -- cgit v1.2.3 From 72959f444c4247c47f63b2499230cb79c208ce51 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:33:26 +0200 Subject: Update ABI --- debian/rules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'debian') diff --git a/debian/rules b/debian/rules index d885ece6..ad53d1f0 100755 --- a/debian/rules +++ b/debian/rules @@ -22,7 +22,7 @@ ADDPREF := COQINSTALLPREFIX=$(COQPREF) OLDROOT= PACKAGES := $(shell dh_listpackages) -COQ_VERSION := 8.4beta2 +COQ_VERSION := 8.4 COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI) CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \ -- cgit v1.2.3 From e0356f0d6ec9310a3863f1983f7264847be3c274 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Mon, 20 Aug 2012 18:33:50 +0200 Subject: Prepare upload to experimental --- debian/changelog | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index 6dc59d00..32009920 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,8 +1,8 @@ -coq (8.4dfsg-1) UNRELEASED; urgency=low +coq (8.4dfsg-1) experimental; urgency=low * New upstream release - -- Stéphane Glondu Mon, 20 Aug 2012 18:27:33 +0200 + -- Stéphane Glondu Mon, 20 Aug 2012 18:33:45 +0200 coq (8.4~gamma0+really8.4beta2+dfsg-1) experimental; urgency=low -- cgit v1.2.3 From dcdaa8517bfaedcf4ce97380d39011d976fc1b64 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 22 Sep 2012 12:31:59 +0200 Subject: Upstream bugfix: Fix use of $(HASNATDYNLINK) in coq_makefile output --- ...e-of-HASNATDYNLINK-in-coq_makefile-output.patch | 46 ++++++++++++++++++++++ debian/patches/series | 1 + 2 files changed, 47 insertions(+) create mode 100644 debian/patches/0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch (limited to 'debian') diff --git a/debian/patches/0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch b/debian/patches/0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch new file mode 100644 index 00000000..8e9b9ee6 --- /dev/null +++ b/debian/patches/0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch @@ -0,0 +1,46 @@ +From: Stephane Glondu +Date: Sat, 22 Sep 2012 12:24:42 +0200 +Subject: Fix use of $(HASNATDYNLINK) in coq_makefile output + +Generated makefiles were broken because + $(if ifeq '$(HASNATDYNLINK)' 'true',X) +always returns X. +--- + tools/coq_makefile.ml | 10 +++++++--- + 1 file changed, 7 insertions(+), 3 deletions(-) + +diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml +index eedbf42..bc38136 100644 +--- a/tools/coq_makefile.ml ++++ b/tools/coq_makefile.ml +@@ -222,7 +222,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in + print "\n"; + end; + print "install:"; +- if (not_empty cmxsfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)"; ++ if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; + print "\n"; + if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc; + if (not_empty cmofiles) then +@@ -543,14 +543,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other + print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n"; + classify_files_by_root "CMXSFILES" (l1@l2) inc; + end; +- print "\n"; ++ print "ifeq '$(HASNATDYNLINK)' 'true'\n"; ++ print "HASNATDYNLINK_OR_EMPTY := yes\n"; ++ print "else\n"; ++ print "HASNATDYNLINK_OR_EMPTY :=\n"; ++ print "endif\n\n"; + section "Definition of the toplevel targets."; + print "all: "; + if !some_vfile then print "$(VOFILES) "; + if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) "; + if !some_mllibfile then print "$(CMAFILES) "; + if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile +- then print "$(if ifeq '$(HASNATDYNLINK)' 'true',$(CMXSFILES)) "; ++ then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) "; + print_list "\\\n " other_targets; print "\n\n"; + if !some_mlifile then + begin +-- diff --git a/debian/patches/series b/debian/patches/series index 53d51a16..f1d97c91 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1 +1,2 @@ 0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch +0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch -- cgit v1.2.3 From eabf57d06ca1eafa762d7f31262e5515401eff55 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 22 Sep 2012 12:43:41 +0200 Subject: Update changelog and prepare upload to experimental --- debian/changelog | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index 32009920..8ef512b8 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +coq (8.4dfsg-2) experimental; urgency=low + + * Upstream bugfix: Fix use of $(HASNATDYNLINK) in coq_makefile output + + -- Stéphane Glondu Sat, 22 Sep 2012 12:43:13 +0200 + coq (8.4dfsg-1) experimental; urgency=low * New upstream release -- cgit v1.2.3 From eddfbb4299e1707e7b0e2347a089fde045ed0e24 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:58:57 +0100 Subject: New upstream release --- debian/changelog | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index 8ef512b8..f1a6b5c0 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +coq (8.4pl1dfsg-1) UNRELEASED; urgency=low + + * New upstream release + + -- Stéphane Glondu Sat, 29 Dec 2012 10:58:46 +0100 + coq (8.4dfsg-2) experimental; urgency=low * Upstream bugfix: Fix use of $(HASNATDYNLINK) in coq_makefile output -- cgit v1.2.3 From 310693f95754bff6577f0ab933e00190f9b4083b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:59:02 +0100 Subject: Refresh patches --- ...e-of-HASNATDYNLINK-in-coq_makefile-output.patch | 46 ---------------------- debian/patches/series | 1 - 2 files changed, 47 deletions(-) delete mode 100644 debian/patches/0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch (limited to 'debian') diff --git a/debian/patches/0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch b/debian/patches/0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch deleted file mode 100644 index 8e9b9ee6..00000000 --- a/debian/patches/0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch +++ /dev/null @@ -1,46 +0,0 @@ -From: Stephane Glondu -Date: Sat, 22 Sep 2012 12:24:42 +0200 -Subject: Fix use of $(HASNATDYNLINK) in coq_makefile output - -Generated makefiles were broken because - $(if ifeq '$(HASNATDYNLINK)' 'true',X) -always returns X. ---- - tools/coq_makefile.ml | 10 +++++++--- - 1 file changed, 7 insertions(+), 3 deletions(-) - -diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml -index eedbf42..bc38136 100644 ---- a/tools/coq_makefile.ml -+++ b/tools/coq_makefile.ml -@@ -222,7 +222,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in - print "\n"; - end; - print "install:"; -- if (not_empty cmxsfiles) then print "$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)"; -+ if (not_empty cmxsfiles) then print "$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)"; - print "\n"; - if not_empty vfiles then install_include_by_root "VOFILES" vfiles inc; - if (not_empty cmofiles) then -@@ -543,14 +543,18 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other - print "CMXSFILES=$(CMXFILES:.cmx=.cmxs) $(CMXAFILES:.cmxa=.cmxs)\n"; - classify_files_by_root "CMXSFILES" (l1@l2) inc; - end; -- print "\n"; -+ print "ifeq '$(HASNATDYNLINK)' 'true'\n"; -+ print "HASNATDYNLINK_OR_EMPTY := yes\n"; -+ print "else\n"; -+ print "HASNATDYNLINK_OR_EMPTY :=\n"; -+ print "endif\n\n"; - section "Definition of the toplevel targets."; - print "all: "; - if !some_vfile then print "$(VOFILES) "; - if !some_mlfile || !some_ml4file || !some_mlpackfile then print "$(CMOFILES) "; - if !some_mllibfile then print "$(CMAFILES) "; - if !some_mlfile || !some_ml4file || !some_mllibfile || !some_mlpackfile -- then print "$(if ifeq '$(HASNATDYNLINK)' 'true',$(CMXSFILES)) "; -+ then print "$(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) "; - print_list "\\\n " other_targets; print "\n\n"; - if !some_mlifile then - begin --- diff --git a/debian/patches/series b/debian/patches/series index f1d97c91..53d51a16 100644 --- a/debian/patches/series +++ b/debian/patches/series @@ -1,2 +1 @@ 0001-test-suite-success-Nsatz.v-comment-out-Ceva.patch -0002-Fix-use-of-HASNATDYNLINK-in-coq_makefile-output.patch -- cgit v1.2.3 From 82f618cde74011104f2d369c2aa28d47deb08fb3 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 11:30:23 +0100 Subject: Update ABI --- debian/rules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'debian') diff --git a/debian/rules b/debian/rules index ad53d1f0..29dfdc5c 100755 --- a/debian/rules +++ b/debian/rules @@ -22,7 +22,7 @@ ADDPREF := COQINSTALLPREFIX=$(COQPREF) OLDROOT= PACKAGES := $(shell dh_listpackages) -COQ_VERSION := 8.4 +COQ_VERSION := 8.4pl1 COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI) CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \ -- cgit v1.2.3 From e16a62685a044b4754d9075512d2852d0dd7c1d2 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 15:55:53 +0100 Subject: Add ocaml-findlib to Build-Depends... ...so that detection of lablgtk2 works --- debian/control | 1 + 1 file changed, 1 insertion(+) (limited to 'debian') diff --git a/debian/control b/debian/control index f2a5e66b..d314e2c3 100644 --- a/debian/control +++ b/debian/control @@ -12,6 +12,7 @@ Build-Depends: 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, -- cgit v1.2.3 From 1c212c7027effb41a8831acdc0c4277ab8c80d26 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 11:02:57 +0100 Subject: Update changelog and prepare upload to experimental --- debian/changelog | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index f1a6b5c0..890aff07 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,8 +1,11 @@ -coq (8.4pl1dfsg-1) UNRELEASED; urgency=low +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 Sat, 29 Dec 2012 10:58:46 +0100 + -- Stéphane Glondu Sat, 29 Dec 2012 15:56:53 +0100 coq (8.4dfsg-2) experimental; urgency=low -- cgit v1.2.3 From 0c6687c12b628881d5660d57707f0e7ca9e521b7 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:45:24 +0200 Subject: New debian/watch file by Bart Martens --- debian/watch | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'debian') diff --git a/debian/watch b/debian/watch index 07bcf5fe..5d9c70de 100644 --- a/debian/watch +++ b/debian/watch @@ -1,4 +1,4 @@ version=3 - -opts=dversionmangle=s/dfsg$// \ - http://coq.inria.fr/download .*/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 Sun, 30 Dec 2012 20:22:30 +0000 -- cgit v1.2.3 From 5f7828e08f3583244ce7f1aa06af76caae69eb27 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:31 +0200 Subject: New upstream release --- debian/changelog | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index 890aff07..7e91a3d3 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,9 @@ +coq (8.4pl2dfsg-1) UNRELEASED; urgency=low + + * New upstream release + + -- Stéphane Glondu Wed, 08 May 2013 17:47:25 +0200 + coq (8.4pl1dfsg-1) experimental; urgency=low * New upstream release -- cgit v1.2.3 From 0b14713e3efd7f8f1cc8a06555d0ec8fbe496130 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:49:57 +0200 Subject: Update ABI --- debian/rules | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'debian') diff --git a/debian/rules b/debian/rules index 29dfdc5c..4a033c89 100755 --- a/debian/rules +++ b/debian/rules @@ -22,7 +22,7 @@ ADDPREF := COQINSTALLPREFIX=$(COQPREF) OLDROOT= PACKAGES := $(shell dh_listpackages) -COQ_VERSION := 8.4pl1 +COQ_VERSION := 8.4pl2 COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI) CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \ -- cgit v1.2.3