From f9f576e1414f75ad762302ac3a485a82e0eb2179 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:58:19 +0100 Subject: New upstream release, update changelog --- debian/changelog | 8 +- ...g-coqlib-argument-to-coqdep-in-test-suite.patch | 23 --- .../0002-Fix-mixed-implicit-and-normal-rules.patch | 85 ----------- .../patches/0003-Support-for-camlp5-6.02.1.patch | 156 --------------------- debian/patches/series | 3 - 5 files changed, 6 insertions(+), 269 deletions(-) delete mode 100644 debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch delete mode 100644 debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch delete mode 100644 debian/patches/0003-Support-for-camlp5-6.02.1.patch delete mode 100644 debian/patches/series diff --git a/debian/changelog b/debian/changelog index 593104db..47377d58 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,6 +1,10 @@ -coq (8.3+dfsg-2) UNRELEASED; urgency=low +coq (8.3.pl1+dfsg-1) UNRELEASED; urgency=low - * NOT RELEASED YET + * New upstream release + - remove all patches (applied upstream) + * debian/rules: + - run test-suite in override_dh_auto_test, skip coqchk run + - make "build" explicitly a phony target -- Stéphane Glondu Tue, 19 Oct 2010 12:10:18 +0200 diff --git a/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch b/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch deleted file mode 100644 index c3092bac..00000000 --- a/debian/patches/0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch +++ /dev/null @@ -1,23 +0,0 @@ -From: Stephane Glondu -Date: Fri, 15 Oct 2010 17:24:18 +0200 -Subject: [PATCH] Fix missing -coqlib argument to coqdep in test-suite - -Signed-off-by: Stephane Glondu ---- - test-suite/Makefile | 2 +- - 1 files changed, 1 insertions(+), 1 deletions(-) - -diff --git a/test-suite/Makefile b/test-suite/Makefile -index 62d443d..98bab43 100644 ---- a/test-suite/Makefile -+++ b/test-suite/Makefile -@@ -40,7 +40,7 @@ endif - - command := $(coqtop) -top Top -load-vernac-source - coqc := $(coqtop) -compile --coqdep := $(BIN)coqdep -+coqdep := $(BIN)coqdep -coqlib $(LIB) - - SHOW := $(if $(VERBOSE),@true,@echo) - HIDE := $(if $(VERBOSE),,@) --- diff --git a/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch b/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch deleted file mode 100644 index 79c1a22b..00000000 --- a/debian/patches/0002-Fix-mixed-implicit-and-normal-rules.patch +++ /dev/null @@ -1,85 +0,0 @@ -From: Stephane Glondu -Date: Tue, 19 Oct 2010 12:00:55 +0200 -Subject: [PATCH] Fix mixed implicit and normal rules - -This fixes build with GNU Make 3.82. See threads: - - https://sympa-roc.inria.fr/wws/arc/coqdev/2010-10/msg00025.html - http://thread.gmane.org/gmane.comp.gnu.make.bugs/4912 - -Signed-off-by: Stephane Glondu ---- - Makefile | 10 ++++++++++ - Makefile.common | 15 +++++++++------ - 2 files changed, 19 insertions(+), 6 deletions(-) - -diff --git a/Makefile b/Makefile -index 975ece0..908dbd6 100644 ---- a/Makefile -+++ b/Makefile -@@ -160,9 +160,19 @@ else - stage1 $(STAGE1_TARGETS) : always - $(call stage-template,1) - -+ifneq (,$(STAGE1_IMPLICITS)) -+$(STAGE1_IMPLICITS) : always -+ $(call stage-template,1) -+endif -+ - stage2 $(STAGE2_TARGETS) : stage1 - $(call stage-template,2) - -+ifneq (,$(STAGE2_IMPLICITS)) -+$(STAGE2_IMPLICITS) : stage1 -+ $(call stage-template,2) -+endif -+ - # Nota: - # - world is one of the targets in $(STAGE2_TARGETS), hence launching - # "make" or "make world" leads to recursion into stage1 then stage2 -diff --git a/Makefile.common b/Makefile.common -index cc38980..46bf217 100644 ---- a/Makefile.common -+++ b/Makefile.common -@@ -365,7 +365,7 @@ DATE=$(shell LANG=C date +"%B %Y") - - SOURCEDOCDIR=dev/source-doc - --CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot -+CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.o %.cmi %.cma %.cmxa %.a %.cmxs %.dep.ps %.dot - - ### Targets forwarded by Makefile to a specific stage: - -@@ -374,10 +374,12 @@ CAML_OBJECT_PATTERNS:=%.cmo %.cmx %.cmi %.cma %.cmxa %.cmxs %.dep.ps %.dot - STAGE1_TARGETS:= $(STAGE1) $(COQDEPBOOT) \ - $(GENFILES) \ - source-doc revision toplevel/mltop.byteml toplevel/mltop.optml \ -- $(STAGE1_ML4:.ml4=.ml4-preprocessed) %.o -+ $(STAGE1_ML4:.ml4=.ml4-preprocessed) -+ -+STAGE1_IMPLICITS:= - - ifdef CM_STAGE1 -- STAGE1_TARGETS+=$(CAML_OBJECT_PATTERNS) -+ STAGE1_IMPLICITS+=$(CAML_OBJECT_PATTERNS) - endif - - ## Enumeration of targets that require being done at stage2 -@@ -402,12 +404,13 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ - printers debug initplugins plugins \ - world install coqide coqide-files coq coqlib \ - coqlight states check init theories theories-light \ -- $(DOC_TARGETS) $(VO_TARGETS) validate \ -- %.vo %.glob states/% install-% %.ml4-preprocessed \ -+ $(DOC_TARGETS) $(VO_TARGETS) validate -+ -+STAGE2_IMPLICITS:= %.vo %.glob states/% install-% %.ml4-preprocessed \ - $(DOC_TARGET_PATTERNS) - - ifndef CM_STAGE1 -- STAGE2_TARGETS+=$(CAML_OBJECT_PATTERNS) -+ STAGE2_IMPLICITS+=$(CAML_OBJECT_PATTERNS) - endif - - --- diff --git a/debian/patches/0003-Support-for-camlp5-6.02.1.patch b/debian/patches/0003-Support-for-camlp5-6.02.1.patch deleted file mode 100644 index 4dfaa7b9..00000000 --- a/debian/patches/0003-Support-for-camlp5-6.02.1.patch +++ /dev/null @@ -1,156 +0,0 @@ -From: glondu -Date: Tue, 16 Nov 2010 20:25:56 +0000 -Subject: [PATCH] Support for camlp5 6.02.1 - -Signed-off-by: Stephane Glondu ---- - lib/compat.ml4 | 12 ++++++++++++ - parsing/pcoq.ml4 | 23 ++++++++++++++--------- - parsing/pcoq.mli | 2 ++ - toplevel/metasyntax.ml | 26 +++++++++++++------------- - 4 files changed, 41 insertions(+), 22 deletions(-) - -diff --git a/lib/compat.ml4 b/lib/compat.ml4 -index 9b6bb19..a77c2bc 100644 ---- a/lib/compat.ml4 -+++ b/lib/compat.ml4 -@@ -65,3 +65,15 @@ let unloc = M.unloc - let join_loc = M.join_loc - type token = M.token - type lexer = M.lexer -+ -+IFDEF CAMLP5_6_00 THEN -+ -+let slist0sep x y = Gramext.Slist0sep (x, y, false) -+let slist1sep x y = Gramext.Slist1sep (x, y, false) -+ -+ELSE -+ -+let slist0sep x y = Gramext.Slist0sep (x, y) -+let slist1sep x y = Gramext.Slist1sep (x, y) -+ -+END -diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 -index 90a9220..de1b3ed 100644 ---- a/parsing/pcoq.ml4 -+++ b/parsing/pcoq.ml4 -@@ -145,6 +145,11 @@ module Gram = - G.delete_rule e pil - end - -+IFDEF CAMLP5_6_02_1 THEN -+let entry_print x = Gram.Entry.print !Pp_control.std_ft x -+ELSE -+let entry_print = Gram.Entry.print -+END - - let camlp4_verbosity silent f x = - let a = !Gramext.warning_verbose in -@@ -631,16 +636,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = - | ETConstrList (typ',[]) -> - Gramext.Slist1 (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) - | ETConstrList (typ',tkl) -> -- Gramext.Slist1sep -- (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ'), -- make_sep_rules tkl) -+ Compat.slist1sep -+ (symbol_of_constr_prod_entry_key assoc from forpat (ETConstr typ')) -+ (make_sep_rules tkl) - | ETBinderList (false,[]) -> - Gramext.Slist1 - (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) - | ETBinderList (false,tkl) -> -- Gramext.Slist1sep -- (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false), -- make_sep_rules tkl) -+ Compat.slist1sep -+ (symbol_of_constr_prod_entry_key assoc from forpat (ETBinder false)) -+ (make_sep_rules tkl) - | _ -> - match interp_constr_prod_entry_key assoc from forpat typ with - | (eobj,None,_) -> Gramext.Snterm (Gram.Entry.obj eobj) -@@ -654,16 +659,16 @@ let rec symbol_of_constr_prod_entry_key assoc from forpat typ = - let rec symbol_of_prod_entry_key = function - | Alist1 s -> Gramext.Slist1 (symbol_of_prod_entry_key s) - | Alist1sep (s,sep) -> -- Gramext.Slist1sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep)) -+ Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep)) - | Alist0 s -> Gramext.Slist0 (symbol_of_prod_entry_key s) - | Alist0sep (s,sep) -> -- Gramext.Slist0sep (symbol_of_prod_entry_key s, Gramext.Stoken ("",sep)) -+ Compat.slist0sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", sep)) - | Aopt s -> Gramext.Sopt (symbol_of_prod_entry_key s) - | Amodifiers s -> - Gramext.srules - [([], Gramext.action(fun _loc -> [])); - ([Gramext.Stoken ("", "("); -- Gramext.Slist1sep ((symbol_of_prod_entry_key s), Gramext.Stoken ("", ",")); -+ Compat.slist1sep (symbol_of_prod_entry_key s) (Gramext.Stoken ("", ",")); - Gramext.Stoken ("", ")")], - Gramext.action (fun _ l _ _loc -> l))] - | Aself -> Gramext.Sself -diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli -index e4566e7..7dbd78e 100644 ---- a/parsing/pcoq.mli -+++ b/parsing/pcoq.mli -@@ -23,6 +23,8 @@ open Libnames - - module Gram : Grammar.S with type te = Compat.token - -+val entry_print : 'a Gram.Entry.e -> unit -+ - (**********************************************************************) - (* The parser of Coq is built from three kinds of rule declarations: - - dynamic rules declared at the evaluation of Coq files (using -diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml -index 6ee00f4..ddb1b11 100644 ---- a/toplevel/metasyntax.ml -+++ b/toplevel/metasyntax.ml -@@ -106,33 +106,33 @@ let add_tactic_notation (n,prods,e) = - let print_grammar = function - | "constr" | "operconstr" | "binder_constr" -> - msgnl (str "Entry constr is"); -- Gram.Entry.print Pcoq.Constr.constr; -+ entry_print Pcoq.Constr.constr; - msgnl (str "and lconstr is"); -- Gram.Entry.print Pcoq.Constr.lconstr; -+ entry_print Pcoq.Constr.lconstr; - msgnl (str "where binder_constr is"); -- Gram.Entry.print Pcoq.Constr.binder_constr; -+ entry_print Pcoq.Constr.binder_constr; - msgnl (str "and operconstr is"); -- Gram.Entry.print Pcoq.Constr.operconstr; -+ entry_print Pcoq.Constr.operconstr; - | "pattern" -> -- Gram.Entry.print Pcoq.Constr.pattern -+ entry_print Pcoq.Constr.pattern - | "tactic" -> - msgnl (str "Entry tactic_expr is"); -- Gram.Entry.print Pcoq.Tactic.tactic_expr; -+ entry_print Pcoq.Tactic.tactic_expr; - msgnl (str "Entry binder_tactic is"); -- Gram.Entry.print Pcoq.Tactic.binder_tactic; -+ entry_print Pcoq.Tactic.binder_tactic; - msgnl (str "Entry simple_tactic is"); -- Gram.Entry.print Pcoq.Tactic.simple_tactic; -+ entry_print Pcoq.Tactic.simple_tactic; - | "vernac" -> - msgnl (str "Entry vernac is"); -- Gram.Entry.print Pcoq.Vernac_.vernac; -+ entry_print Pcoq.Vernac_.vernac; - msgnl (str "Entry command is"); -- Gram.Entry.print Pcoq.Vernac_.command; -+ entry_print Pcoq.Vernac_.command; - msgnl (str "Entry syntax is"); -- Gram.Entry.print Pcoq.Vernac_.syntax; -+ entry_print Pcoq.Vernac_.syntax; - msgnl (str "Entry gallina is"); -- Gram.Entry.print Pcoq.Vernac_.gallina; -+ entry_print Pcoq.Vernac_.gallina; - msgnl (str "Entry gallina_ext is"); -- Gram.Entry.print Pcoq.Vernac_.gallina_ext; -+ entry_print Pcoq.Vernac_.gallina_ext; - | _ -> error "Unknown or unprintable grammar entry." - - (**********************************************************************) --- diff --git a/debian/patches/series b/debian/patches/series deleted file mode 100644 index de7a4950..00000000 --- a/debian/patches/series +++ /dev/null @@ -1,3 +0,0 @@ -0001-Fix-missing-coqlib-argument-to-coqdep-in-test-suite.patch -0002-Fix-mixed-implicit-and-normal-rules.patch -0003-Support-for-camlp5-6.02.1.patch -- cgit v1.2.3