diff options
Diffstat (limited to 'debian')
| -rw-r--r-- | debian/changelog | 14 | ||||
| -rw-r--r-- | debian/control | 21 | ||||
| -rw-r--r-- | debian/copyright | 76 | ||||
| -rw-r--r-- | debian/coq.install.in | 8 | ||||
| -rw-r--r-- | debian/coq.links.in | 3 | ||||
| -rw-r--r-- | debian/gbp.conf | 3 | ||||
| -rw-r--r-- | debian/libcoq-ocaml-dev.install.in | 16 | ||||
| -rw-r--r-- | debian/libcoq-ocaml.install.in | 47 | ||||
| -rw-r--r-- | debian/patches/0001-Disable-micromega-tests.patch | 25 | ||||
| -rw-r--r-- | debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch | 74 | ||||
| -rw-r--r-- | debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch | 155 | ||||
| -rw-r--r-- | debian/patches/series | 3 | ||||
| -rwxr-xr-x | debian/rules | 19 | ||||
| -rw-r--r-- | debian/source/local-options | 2 |
14 files changed, 142 insertions, 324 deletions
diff --git a/debian/changelog b/debian/changelog index 22a134cd..d87646b5 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,17 @@ +coq (8.3.pl1+dfsg-1) experimental; urgency=low + + * 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 + * Update copyright file + * Fix installation of emacs files + * Install plugins in new binary package libcoq-ocaml + * Bump Standards-Version to 3.9.1 (no changes) + + -- Stéphane Glondu <glondu@debian.org> Fri, 24 Dec 2010 12:51:59 +0100 + coq (8.2.pl2+dfsg-2) unstable; urgency=low * Add Fix-build-with-camlp5-6.02.1.patch diff --git a/debian/control b/debian/control index 8687770b..d093e79e 100644 --- a/debian/control +++ b/debian/control @@ -6,10 +6,10 @@ Uploaders: Ralf Treinen <treinen@debian.org>, Samuel Mimram <smimram@debian.org>, Stéphane Glondu <glondu@debian.org> -Standards-Version: 3.9.0 +Standards-Version: 3.9.1 Build-Depends: debhelper (>= 7.2.11~), - dh-ocaml (>= 0.9~), + dh-ocaml (>= 0.9.5~), ocaml-nox (>= 3.11.1-3~), ocaml-best-compilers, camlp5 (>= 5.12-2~), @@ -80,6 +80,23 @@ Description: proof assistant for higher-order logic (theories) This package provides existing theories that new proofs can be based upon, including theories of arithmetic and Boolean values. +Package: libcoq-ocaml +Section: ocaml +Architecture: any +Depends: + ${ocaml:Depends}, + ${shlibs:Depends}, + ${misc:Depends} +Provides: ${ocaml:Provides} +Breaks: coq (<< 8.3~), libcoq-ocaml-dev (<< 8.3~), coq-libs +Replaces: coq (<< 8.3~), libcoq-ocaml-dev (<< 8.3~), coq-libs +Description: runtime libraries for Coq + Coq is a proof assistant for higher-order logic, which allows the + development of computer programs consistent with their formal + specification. It is developed using Objective Caml and Camlp5. + . + This package provides runtime libraries for Coq. + Package: libcoq-ocaml-dev Section: ocaml Architecture: any diff --git a/debian/copyright b/debian/copyright index 38373808..6ff2511f 100644 --- a/debian/copyright +++ b/debian/copyright @@ -1,47 +1,29 @@ -This package was debianized by Fernando Sanchez <fer@debian.org> - -It was downloaded from - -ftp://ftp.inria.fr/INRIA/LogiCal/coq/current - -The Coq proof assistant V7 and V8 includes software developed by the -Coq development team inside the LogiCal project, at INRIA, CNRS and -University Paris Sud. - -Copyright 1999-2005 The Coq development team, -INRIA-CNRS, University Paris Sud, All rights reserved. - -This product includes also software developed by - Yves Bertot, Lemme, INRIA Sophia-Antipolis (contrib/interface, - parsing/search.ml) - Pierre Crégut, France Telecom R & D (contrib/omega and contrib/romega) - Pierre Courtieu, Lemme (contrib/funind) - Loïc Pottier, Lemme, INRIA Sophia-Antipolis (contrib/fourier) - Claudio Sacerdoti Coen, HELM, University of Bologna (contrib/xml) - -Coq includes a tactic Jp based on JProver, a theorem prover for -first-order intuitionistic logic. Jprover was originally implemented -by Stephan Schmitt and then integrated into MetaPRL by Aleksey -Nogin. After this, Huang extracted the necessary ML-codes from MetaPRL -and then integrated it into Coq. - -The Coq development Team (march 2004) - Bruno Barras (INRIA) - Pierre Corbineau (Université Paris Sud) - Jean-Christophe Filliâtre (CNRS) - Hugo Herbelin (INRIA) - Pierre Letouzey (Université Paris Sud) - Claude Marché (Université Paris Sud-INRIA) - Christine Paulin (Université Paris Sud) - Clément Renard (INRIA) - -The complete list of developpers and contributors can be found in -/usr/share/doc/doc/CREDITS.gz - -Copyright: 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. - -However there are two exceptions: files in the directories contrib/jprover and -ide/utils are distributed under the terms of the GNU General Public Licence, -see /usr/share/common-licenses/GPL-2. +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. +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. + + 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> + © 2001-2002 Judicael Courant <Judicael.Courant@lri.fr> + © 2004-2009 Samuel Mimram <smimram@debian.org> + © 2008-2010 Stéphane Glondu <glondu@debian.org> +License: LGPL-2.1 diff --git a/debian/coq.install.in b/debian/coq.install.in index ba265336..2c0f9c86 100644 --- a/debian/coq.install.in +++ b/debian/coq.install.in @@ -2,14 +2,11 @@ usr/bin/coqc* usr/bin/coqdep* usr/bin/coqdoc* usr/bin/coq_makefile* -usr/bin/coq-interface* -usr/bin/coq-parser* usr/bin/coq-tex* usr/bin/coqtop* usr/bin/coqwc* usr/bin/gallina* -usr/lib/coq/contrib/micromega/csdpcert -usr/lib/coq/contrib/interface/vernacrc +usr/lib/coq/plugins/micromega/csdpcert usr/lib/coq/tools/coqdoc/coqdoc.css usr/lib/coq/tools/coqdoc/coqdoc.sty usr/lib/coq/states/initial.coq @@ -18,13 +15,10 @@ usr/share/man/man1/coqc* usr/share/man/man1/coqdep* usr/share/man/man1/coqdoc* usr/share/man/man1/coq_makefile* -usr/share/man/man1/coq-interface* -usr/share/man/man1/coq-parser* usr/share/man/man1/coq-tex* usr/share/man/man1/coqtop* usr/share/man/man1/coqwc* usr/share/man/man1/gallina* -usr/lib/coq/dllcoqrun.so @OCamlDllDir@ usr/share/emacs/site-lisp/coqdoc.sty usr/share/texmf/tex/latex/misc/ debian/coq.xpm usr/share/pixmaps debian/coqvars.mk usr/share/coq diff --git a/debian/coq.links.in b/debian/coq.links.in index 250c3210..33c64ad9 100644 --- a/debian/coq.links.in +++ b/debian/coq.links.in @@ -1,2 +1 @@ -OPT: /usr/share/man/man1/coq-interface.1 /usr/share/man/man1/coq-interface.opt.1 -OPT: /usr/share/man/man1/coq-parser.1 /usr/share/man/man1/coq-parser.opt.1 +OPT: /usr/share/man/man1/coqchk.1 /usr/share/man/man1/coqchk.opt.1
\ No newline at end of file diff --git a/debian/gbp.conf b/debian/gbp.conf index 6c7ed3be..dfa07a01 100644 --- a/debian/gbp.conf +++ b/debian/gbp.conf @@ -1,3 +1,4 @@ [DEFAULT] pristine-tar = True -cleaner = debuild clean && dh_quilt_unpatch && dh_clean +upstream-branch = experimental/upstream +debian-branch = experimental/master diff --git a/debian/libcoq-ocaml-dev.install.in b/debian/libcoq-ocaml-dev.install.in index b246d33f..cfaf7ca6 100644 --- a/debian/libcoq-ocaml-dev.install.in +++ b/debian/libcoq-ocaml-dev.install.in @@ -1,3 +1,17 @@ usr/bin/coqmktop* usr/share/man/man1/coqmktop* -# *.cm* files will be added here +usr/lib/coq/proofs/proofs.cma +usr/lib/coq/ide/ide.cma +usr/lib/coq/interp/interp.cma +usr/lib/coq/tactics/tactics.cma +usr/lib/coq/tactics/hightactics.cma +usr/lib/coq/lib/lib.cma +usr/lib/coq/toplevel/toplevel.cma +usr/lib/coq/parsing/highparsing.cma +usr/lib/coq/parsing/grammar.cma +usr/lib/coq/parsing/parsing.cma +usr/lib/coq/pretyping/pretyping.cma +usr/lib/coq/library/library.cma +usr/lib/coq/kernel/kernel.cma +usr/lib/coq/config/coq_config.cmo +# other *.cm* files will be added here by debian/rules diff --git a/debian/libcoq-ocaml.install.in b/debian/libcoq-ocaml.install.in new file mode 100644 index 00000000..746a3577 --- /dev/null +++ b/debian/libcoq-ocaml.install.in @@ -0,0 +1,47 @@ +usr/lib/coq/dllcoqrun.so @OCamlDllDir@ +usr/lib/coq/plugins/ring/ring_plugin.cma +usr/lib/coq/plugins/fourier/fourier_plugin.cma +usr/lib/coq/plugins/extraction/extraction_plugin.cma +usr/lib/coq/plugins/omega/omega_plugin.cma +usr/lib/coq/plugins/cc/cc_plugin.cma +usr/lib/coq/plugins/syntax/string_syntax_plugin.cma +usr/lib/coq/plugins/syntax/nat_syntax_plugin.cma +usr/lib/coq/plugins/syntax/numbers_syntax_plugin.cma +usr/lib/coq/plugins/syntax/z_syntax_plugin.cma +usr/lib/coq/plugins/syntax/r_syntax_plugin.cma +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 +usr/lib/coq/plugins/field/field_plugin.cma +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 +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 +DYN: usr/lib/coq/plugins/omega/omega_plugin.cmxs +DYN: usr/lib/coq/plugins/cc/cc_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/string_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/nat_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/numbers_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/z_syntax_plugin.cmxs +DYN: usr/lib/coq/plugins/syntax/r_syntax_plugin.cmxs +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 +DYN: usr/lib/coq/plugins/field/field_plugin.cmxs +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 diff --git a/debian/patches/0001-Disable-micromega-tests.patch b/debian/patches/0001-Disable-micromega-tests.patch deleted file mode 100644 index 5979dc6d..00000000 --- a/debian/patches/0001-Disable-micromega-tests.patch +++ /dev/null @@ -1,25 +0,0 @@ -From: Stephane Glondu <steph@glondu.net> -Date: Mon, 22 Feb 2010 10:39:03 +0100 -Subject: Disable micromega tests - -Workaround for bug #570920. ---- - test-suite/check | 4 ++-- - 1 files changed, 2 insertions(+), 2 deletions(-) - -diff --git a/test-suite/check b/test-suite/check -index bed86c4..e7889cf 100755 ---- a/test-suite/check -+++ b/test-suite/check -@@ -248,8 +248,8 @@ echo "Parser tests" - test_parser parser - echo "Interactive tests" - test_interactive interactive --echo "Micromega tests" --test_success micromega -+#echo "Micromega tests" -+#test_success micromega - - # We give a chance to disable the complexity tests which may cause - # random build failures on build farms --- diff --git a/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch b/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch deleted file mode 100644 index fd1aaf13..00000000 --- a/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch +++ /dev/null @@ -1,74 +0,0 @@ -From: Stephane Glondu <steph@glondu.net> -Date: Fri, 2 Jul 2010 15:00:43 +0200 -Subject: Remove dependency to Unix from module Profile - -Applied-Upstream: https://gforge.inria.fr/scm/viewvc.php?view=rev&root=coq&revision=13234 -Signed-off-by: Stephane Glondu <steph@glondu.net> ---- - Makefile.build | 4 ++-- - lib/profile.ml | 8 +++++--- - lib/profile.mli | 4 +--- - 3 files changed, 8 insertions(+), 8 deletions(-) - -diff --git a/Makefile.build b/Makefile.build -index 148bb62..c4358ce 100644 ---- a/Makefile.build -+++ b/Makefile.build -@@ -782,10 +782,10 @@ dev/printers.cma: $(PRINTERSCMO) - parsing/grammar.cma: $(GRAMMARCMO) - $(SHOW)'Testing $@' - @touch test.ml4 -- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) unix.cma $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar -+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar - @rm -f test-grammar test.* - $(SHOW)'OCAMLC -a $@' -- $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $(GRAMMARCMO) -linkall -a -o $@ -+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ - - # toplevel/mltop.ml4 (ifdef Byte) - -diff --git a/lib/profile.ml b/lib/profile.ml -index dd7e977..40bfba3 100644 ---- a/lib/profile.ml -+++ b/lib/profile.ml -@@ -17,8 +17,7 @@ let float_of_time t = float_of_int t /. 100. - let time_of_float f = int_of_float (f *. 100.) - - let get_time () = -- let {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in -- time_of_float (ut +. st) -+ time_of_float (Sys.time ()) - - (* Since ocaml 3.01, gc statistics are in float *) - let get_alloc () = -@@ -157,7 +156,10 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = - (* Unix measure of time is approximative and shoitt delays are often - unperceivable; therefore, total times are measured in one (big) - step to avoid rounding errors and to get the best possible -- approximation *) -+ approximation. -+ Note: Sys.time is the same as: -+ Unix.(let x = times () in x.tms_utime +. x.tms_stime) -+ *) - - (* - ---------- start profile for f1 -diff --git a/lib/profile.mli b/lib/profile.mli -index 0937e9e..1e28834 100644 ---- a/lib/profile.mli -+++ b/lib/profile.mli -@@ -10,12 +10,10 @@ - - (*s This program is a small time and allocation profiler for Objective Caml *) - --(*i It requires the UNIX library *) - - (* Adapted from Christophe Raffalli *) - --(* To use it, link it with the program you want to profile (do not forget --"-cclib -lunix -custom unix.cma" among the link options). -+(* To use it, link it with the program you want to profile. - - To trace a function "f" you first need to get a key for it by using : - --- diff --git a/debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch b/debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch deleted file mode 100644 index 908296ac..00000000 --- a/debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch +++ /dev/null @@ -1,155 +0,0 @@ -From: Stephane Glondu <steph@glondu.net> -Date: Wed, 17 Nov 2010 21:26:49 +0000 -Subject: Fix build with camlp5 6.02.1 - -This is a squash of upstream commits 13647 and 13706 in v8.2 branch. ---- - lib/compat.ml4 | 10 ++++++++++ - parsing/pcoq.ml4 | 11 ++++++++--- - parsing/pcoq.mli | 2 ++ - parsing/q_util.ml4 | 6 +++--- - toplevel/metasyntax.ml | 26 +++++++++++++------------- - 5 files changed, 36 insertions(+), 19 deletions(-) - -diff --git a/lib/compat.ml4 b/lib/compat.ml4 -index 40cffad..de049b2 100644 ---- a/lib/compat.ml4 -+++ b/lib/compat.ml4 -@@ -69,3 +69,13 @@ let join_loc = M.join_loc - type token = M.token - type lexer = M.lexer - let using = M.using -+ -+(** Compatibility with Camlp5 6.x *) -+ -+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 d2d81cd..3ab89cd 100644 ---- a/parsing/pcoq.ml4 -+++ b/parsing/pcoq.ml4 -@@ -159,6 +159,11 @@ module Gram = - errorlabstrm "Pcoq.delete_rule" (str "GDELETE_RULE forbidden.") - 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 -@@ -746,9 +751,9 @@ let rec symbol_of_production assoc from forpat typ = - | ETConstrList (typ',[]) -> - Gramext.Slist1 (symbol_of_production assoc from forpat (ETConstr typ')) - | ETConstrList (typ',tkl) -> -- Gramext.Slist1sep -- (symbol_of_production assoc from forpat (ETConstr typ'), -- Gramext.srules -+ Compat.slist1sep -+ (symbol_of_production assoc from forpat (ETConstr typ')) -+ (Gramext.srules - [List.map (fun x -> Gramext.Stoken x) tkl, - List.fold_right (fun _ v -> Gramext.action (fun _ -> v)) tkl - (Gramext.action (fun loc -> ()))]) -diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli -index 0a4b349..077f178 100644 ---- a/parsing/pcoq.mli -+++ b/parsing/pcoq.mli -@@ -24,6 +24,8 @@ val lexer : Compat.lexer - - module Gram : Grammar.S with type te = Compat.token - -+val entry_print : 'a Gram.Entry.e -> unit -+ - (* The superclass of all grammar entries *) - type grammar_object - -diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4 -index da4329b..0d2a890 100644 ---- a/parsing/q_util.ml4 -+++ b/parsing/q_util.ml4 -@@ -82,7 +82,7 @@ let modifiers e = - <:expr< Gramext.srules - [([], Gramext.action(fun _loc -> [])); - ([Gramext.Stoken ("", "("); -- Gramext.Slist1sep ($e$, Gramext.Stoken ("", ",")); -+ Compat.slist1sep $e$ (Gramext.Stoken ("", ",")); - Gramext.Stoken ("", ")")], - Gramext.action (fun _ l _ _loc -> l))] - >> -@@ -96,14 +96,14 @@ let rec interp_entry_name loc s sep = - String.sub s (l-9) 9 = "_list_sep" then - let t, g = interp_entry_name loc (String.sub s 3 (l-12)) "" in - let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in -- List1ArgType t, <:expr< Gramext.Slist1sep $g$ $sep$ >> -+ List1ArgType t, <:expr< Compat.slist1sep $g$ $sep$ >> - else if l > 5 & String.sub s (l-5) 5 = "_list" then - let t, g = interp_entry_name loc (String.sub s 0 (l-5)) "" in - List0ArgType t, <:expr< Gramext.Slist0 $g$ >> - else if l > 9 & String.sub s (l-9) 9 = "_list_sep" then - let t, g = interp_entry_name loc (String.sub s 0 (l-9)) "" in - let sep = <:expr< Gramext.Stoken("",$str:sep$) >> in -- List0ArgType t, <:expr< Gramext.Slist0sep $g$ $sep$ >> -+ List0ArgType t, <:expr< Compat.slist0sep $g$ $sep$ >> - else if l > 4 & String.sub s (l-4) 4 = "_opt" then - let t, g = interp_entry_name loc (String.sub s 0 (l-4)) "" in - OptArgType t, <:expr< Gramext.Sopt $g$ >> -diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml -index 821a73f..ba10708 100644 ---- a/toplevel/metasyntax.ml -+++ b/toplevel/metasyntax.ml -@@ -100,33 +100,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 7ce5e4c8..00000000 --- a/debian/patches/series +++ /dev/null @@ -1,3 +0,0 @@ -0001-Disable-micromega-tests.patch -0002-Remove-dependency-to-Unix-from-module-Profile.patch -0003-Fix-build-with-camlp5-6.02.1.patch diff --git a/debian/rules b/debian/rules index 5a7363fa..3471198a 100755 --- a/debian/rules +++ b/debian/rules @@ -8,7 +8,6 @@ BUILDCACHE := $(wildcard ../coq.cache) # This has to be exported to make some magic below work. -export COQTEST_SKIPCOMPLEXITY = true export CAML_LD_LIBRARY_PATH = $(shell pwd)/kernel/byterun # Show full commands when building Coq @@ -19,15 +18,15 @@ include /usr/share/ocaml/ocamlvars.mk HTMLDOC := doc/stdlib/html/index.html COQPREF := $(CURDIR)/debian/tmp -ADDPREF := COQINSTALLPREFIX=$(COQPREF) +ADDPREF := COQINSTALLPREFIX=$(COQPREF) OLDROOT= PACKAGES := $(shell dh_listpackages) -COQ_VERSION := $(shell head -n1 debian/changelog | awk -F'[+() ]' '{print $$3}') +COQ_VERSION := $(shell dpkg-parsechangelog | sed -n -e 's/~/+/g' -e 's/^Version: \(.*\)-[0-9]\+/\1/p') COQ_ABI := $(COQ_VERSION)+$(OCAML_ABI) CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \ - --emacslib /usr/share/emacs/site-lisp/coq --reals all --fsets all \ + --emacslib /usr/share/emacs/site-lisp/coq \ --browser "/usr/bin/x-www-browser %s &" \ --with-doc no --coqrunbyteflags "-dllib -lcoqrun" @@ -38,6 +37,12 @@ export OCAMLINIT_SED += \ %: +dh --with ocaml $@ +# There is already a file named "build" in upstream sources, so the +# above rule is never called. We make it explicitly a phony rule here. +.PHONY: build +build: + +dh --with ocaml $@ + .PHONY: override_dh_auto_configure override_dh_auto_configure: ./configure $(CONFIGUREOPTS) @@ -50,7 +55,7 @@ ifeq ($(BUILDCACHE),) # the default one without -silent (-silent maybe cause buildd to # timeout because of lack of output) - $(MAKE) STRIP=true VALIDOPTS="-o -m" check + $(MAKE) world STRIP=true $(MAKE) DOC_TARGETS=$(HTMLDOC) $(HTMLDOC) else rsync -a --exclude=debian --exclude=.git $(BUILDCACHE)/ . @@ -58,13 +63,13 @@ endif .PHONY: override_dh_auto_test override_dh_auto_test: -# TODO: run make check here instead of in override_dh_auto_build (?) + $(MAKE) check COMPLEXITY= BESTCHICKEN=/bin/true .PHONY: override_dh_auto_install override_dh_auto_install: $(MAKE) $(ADDPREF) install find debian/tmp -regextype posix-awk \ - -regex '.*\.(cm[aoxi]|cmxa|[ao])$$' \ + -regex '.*\.(cm[xi]|cmxa|[ao])$$' \ >> debian/libcoq-ocaml-dev.install find debian/tmp -name '*.vo' -printf '%P\n' \ >> debian/coq-theories.install diff --git a/debian/source/local-options b/debian/source/local-options new file mode 100644 index 00000000..c4cf4805 --- /dev/null +++ b/debian/source/local-options @@ -0,0 +1,2 @@ +abort-on-upstream-changes +unapply-patches |