From 783b26ca58daa06d66776ddf1b50a20268e0c4b0 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Mon, 15 Oct 2007 19:55:12 +0000 Subject: New upstream release. --- debian/changelog | 8 +- debian/control | 2 +- debian/patches/00list | 1 - debian/patches/browser.dpatch | 10 +- debian/patches/camlp5.dpatch | 563 ------------------------------------ debian/patches/coqdoc_stdlib.dpatch | 12 +- debian/patches/makefile.dpatch | 12 +- 7 files changed, 24 insertions(+), 584 deletions(-) delete mode 100755 debian/patches/camlp5.dpatch diff --git a/debian/changelog b/debian/changelog index 527e5c78..3bb3c0a4 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,8 +1,12 @@ -coq (8.1.pl1+dfsg-4) UNRELEASED; urgency=low +coq (8.1.pl2+dfsg-1) experimental; urgency=low + * New upstream release. + * Removed camlp5.dpatch, integrated upstream. + * Updated browser.dpatch, coqdoc_stdlib.dpatch and makefile.dpatch. * Corrected emacs-mode startup file, closes: #446170. + * Removed Sven Luther from uploaders. - -- Samuel Mimram Wed, 10 Oct 2007 22:36:07 +0000 + -- Samuel Mimram Mon, 15 Oct 2007 18:55:09 +0000 coq (8.1.pl1+dfsg-3) unstable; urgency=low diff --git a/debian/control b/debian/control index 3824703e..338fb38a 100644 --- a/debian/control +++ b/debian/control @@ -2,7 +2,7 @@ Source: coq Section: math Priority: optional Maintainer: Debian OCaml Maintainers -Uploaders: Ralf Treinen , Sven Luther , Remi Vanicat , Stefano Zacchiroli , Samuel Mimram +Uploaders: Ralf Treinen , Remi Vanicat , Stefano Zacchiroli , Samuel Mimram Standards-Version: 3.7.2 Build-Depends: debhelper (>= 4.0.0), dpkg-dev (>= 1.13.19), dpatch, ocaml-nox (>= 3.10), ocaml-best-compilers, camlp5, liblablgtk2-ocaml-dev (>= 2.4.0), texlive-latex-extra, hevea XS-Vcs-Svn: svn://svn.debian.org/svn/pkg-ocaml-maint/trunk/packages/coq diff --git a/debian/patches/00list b/debian/patches/00list index 333bbd2f..bbb91a76 100644 --- a/debian/patches/00list +++ b/debian/patches/00list @@ -1,4 +1,3 @@ -camlp5 coqdoc_stdlib browser makefile diff --git a/debian/patches/browser.dpatch b/debian/patches/browser.dpatch index ba55f3de..9a15372c 100755 --- a/debian/patches/browser.dpatch +++ b/debian/patches/browser.dpatch @@ -5,15 +5,15 @@ ## DP: Use the default Debian browser for help. @DPATCH@ -diff -urNad coq-8.0pl3+8.1alpha~/lib/options.ml coq-8.0pl3+8.1alpha/lib/options.ml ---- coq-8.0pl3+8.1alpha~/lib/options.ml 2005-12-26 20:07:21.000000000 +0000 -+++ coq-8.0pl3+8.1alpha/lib/options.ml 2006-04-29 16:06:20.000000000 +0000 -@@ -117,7 +117,4 @@ +diff -urNad coq-8.1.pl2+dfsg~/lib/options.ml coq-8.1.pl2+dfsg/lib/options.ml +--- coq-8.1.pl2+dfsg~/lib/options.ml 2007-10-15 11:00:52.000000000 +0000 ++++ coq-8.1.pl2+dfsg/lib/options.ml 2007-10-15 11:01:51.000000000 +0000 +@@ -118,7 +118,4 @@ "\" must contain exactly one placeholder \"%s\".") else pre,post with - Not_found -> - if Sys.os_type = "Win32" - then "C:\\PROGRA~1\\INTERN~1\\IEXPLORE ", "" -- else "netscape -remote \"OpenURL(", ")\"" +- else "firefox -remote \"OpenURL(", ")\"" + Not_found -> "/usr/bin/x-www-browser ", "" diff --git a/debian/patches/camlp5.dpatch b/debian/patches/camlp5.dpatch deleted file mode 100755 index 2c5b8643..00000000 --- a/debian/patches/camlp5.dpatch +++ /dev/null @@ -1,563 +0,0 @@ -#! /bin/sh /usr/share/dpatch/dpatch-run -## camlp5.dpatch by Samuel Mimram -## -## All lines beginning with `## DP:' are a description of the patch. -## DP: Use camlp5 instead of the new camlp4 for coq. - -@DPATCH@ -diff -urNad coq-8.1.pl1+dfsg~/Makefile coq-8.1.pl1+dfsg/Makefile ---- coq-8.1.pl1+dfsg~/Makefile 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/Makefile 2007-08-24 10:56:52.000000000 +0000 -@@ -1504,11 +1504,11 @@ - - # BEFOREDEPEND+= parsing/pcoq.ml parsing/extend.ml - --# File using pa_ifdef and only necessary for parsing ml files -+# File using pa_macro and only necessary for parsing ml files - - parsing/q_coqast.cmo: parsing/q_coqast.ml4 - $(SHOW)'OCAMLC4 $<' -- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo $(CAMLP4COMPAT) -impl" -c -impl $< -+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo $(CAMLP4COMPAT) -impl" -c -impl $< - - # toplevel/mltop.ml4 (ifdef Byte) - -@@ -1522,11 +1522,11 @@ - - toplevel/mltop.byteml: toplevel/mltop.ml4 - $(SHOW)'CAMLP4O $<' -- $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@ -+ $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo -DByte -impl $< > $@ || rm -f $@ - - toplevel/mltop.optml: toplevel/mltop.ml4 - $(SHOW)'CAMLP4O $<' -- $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo -impl $< > $@ || rm -f $@ -+ $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo -impl $< > $@ || rm -f $@ - - ML4FILES += toplevel/mltop.ml4 - -@@ -1571,11 +1571,11 @@ - - lib/compat.cmo: lib/compat.ml4 - $(SHOW)'OCAMLC4 $<' -- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $< -+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo -impl" -c -impl $< - - lib/compat.cmx: lib/compat.ml4 - $(SHOW)'OCAMLOPT $<' -- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo -impl" -c -impl $< -+ $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo -impl" -c -impl $< - - # files compiled with camlp4 because of streams syntax - -@@ -1654,7 +1654,7 @@ - $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl" -c -impl $< - - %.ml: %.ml4 -- $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ -+ $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ - - #.v.vo: - # $(BOOTCOQTOP) -compile $* -diff -urNad coq-8.1.pl1+dfsg~/Makefile.dep coq-8.1.pl1+dfsg/Makefile.dep ---- coq-8.1.pl1+dfsg~/Makefile.dep 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/Makefile.dep 2007-08-24 10:56:52.000000000 +0000 -@@ -12,4 +12,4 @@ - include .depend.camlp4 - - .ml4.ml: -- $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_ifdef.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ -+ $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pa_macro.cmo pr_o.cmo `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ || rm -f $@ -diff -urNad coq-8.1.pl1+dfsg~/config/Makefile.template coq-8.1.pl1+dfsg/config/Makefile.template ---- coq-8.1.pl1+dfsg~/config/Makefile.template 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/config/Makefile.template 2007-08-24 10:56:52.000000000 +0000 -@@ -62,7 +62,7 @@ - CAMLMKTOP="CAMLMKTOPEXEC" - - # Caml flags --CAMLFLAGS=CAMLANNOTATEFLAG -+CAMLFLAGS=-rectypes CAMLANNOTATEFLAG - - # Compilation debug flag - CAMLDEBUG=COQDEBUGFLAG -@@ -80,8 +80,8 @@ - BEST=BESTCOMPILER - - # For Camlp4 use --P4=$(COQTOP)/bin/$(ARCH)/call_camlp4 -I $(COQTOP)/src/parsing --P4DEP=$(COQTOP)/bin/$(ARCH)/camlp4dep -+P4=$(COQTOP)/bin/$(ARCH)/call_camlp5 -I $(COQTOP)/src/parsing -+P4DEP=$(COQTOP)/bin/$(ARCH)/camlp5dep - - # Your architecture - # Can be obtain by UNIX command arch -diff -urNad coq-8.1.pl1+dfsg~/configure coq-8.1.pl1+dfsg/configure ---- coq-8.1.pl1+dfsg~/configure 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/configure 2007-08-24 10:56:52.000000000 +0000 -@@ -78,7 +78,7 @@ - ocamllexexec=ocamllex - ocamlyaccexec=ocamlyacc - ocamlmktopexec=ocamlmktop --camlp4oexec=camlp4o -+camlp4oexec=camlp5o - - - coq_debug_flag= -@@ -153,7 +153,7 @@ - arch=$2 - shift;; - -opt|--opt) bytecamlc=ocamlc.opt -- camlp4oexec=camlp4o # can't add .opt since dyn load'll be required -+ camlp4oexec=camlp5o # can't add .opt since dyn load'll be required - nativecamlc=ocamlopt.opt;; - -fsets|--fsets) fsets_opt=yes - case "$2" in -@@ -297,7 +297,7 @@ - ocamllexexec=$CAMLBIN/ocamllex - ocamlyaccexec=$CAMLBIN/ocamlyacc - camlmktopexec=$CAMLBIN/ocamlmktop -- camlp4oexec=$CAMLBIN/camlp4o -+ camlp4oexec=$CAMLBIN/camlp5o - esac - - if test ! -f "$CAMLC" ; then -@@ -362,10 +362,10 @@ - - #case $OS in - # Win32) -- CAMLP4LIB=+camlp4 -+ CAMLP4LIB=+camlp5 - # ;; - # *) --# CAMLP4LIB=${CAMLLIB}/camlp4 -+# CAMLP4LIB=${CAMLLIB}/camlp5 - #esac - - # OS dependent libraries -@@ -615,7 +615,7 @@ - ESCLIBDIR="`VAR=LIBDIR escape_var`" - ESCCAMLDIR="`VAR=CAMLBIN escape_var`" - ESCCAMLLIB="`VAR=CAMLLIB escape_var`" --ESCCAMLP4LIB="$ESCCAMLLIB"/camlp4 -+ESCCAMLP4LIB="$ESCCAMLLIB"/camlp5 - - mlconfig_file="$COQSRC/config/coq_config.ml" - rm -f $mlconfig_file -@@ -739,8 +739,8 @@ - - if test "$coq_debug_flag" = "-g" ; then - rm -f $OCAMLDEBUGCOQ -- if [ "$CAMLP4LIB" = "+camlp4" ] ; then -- CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp4 -+ if [ "$CAMLP4LIB" = "+camlp5" ] ; then -+ CAMLP4LIBFORCAMLDEBUG=$CAMLLIB/camlp5 - else - CAMLP4LIBFORCAMLDEBUG=$CAMLP4LIB - fi -diff -urNad coq-8.1.pl1+dfsg~/dev/ocamldebug-coq.template coq-8.1.pl1+dfsg/dev/ocamldebug-coq.template ---- coq-8.1.pl1+dfsg~/dev/ocamldebug-coq.template 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/dev/ocamldebug-coq.template 2007-08-24 10:56:52.000000000 +0000 -@@ -7,7 +7,7 @@ - export COQTH=$COQLIB/theories - CAMLBIN=CAMLBINDIRECTORY - OCAMLDEBUG=$CAMLBIN/ocamldebug --export CAMLP4LIB=`$CAMLBIN/camlp4 -where` -+export CAMLP4LIB=`$CAMLBIN/camlp5 -where` - - exec $OCAMLDEBUG \ - -I $CAMLP4LIB \ -diff -urNad coq-8.1.pl1+dfsg~/lib/compat.ml4 coq-8.1.pl1+dfsg/lib/compat.ml4 ---- coq-8.1.pl1+dfsg~/lib/compat.ml4 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/lib/compat.ml4 2007-08-24 10:56:52.000000000 +0000 -@@ -11,6 +11,7 @@ - (* IFDEF not available in 3.06; use ifdef instead *) - - (* type loc is different in 3.08 *) -+(* - ifdef OCAML_308 then - module M = struct - type loc = Token.flocation -@@ -32,8 +33,9 @@ - let make_loc x = x - let unloc x = x - end -+*) - --type loc = M.loc --let dummy_loc = M.dummy_loc --let unloc = M.unloc --let make_loc = M.make_loc -+type loc = Stdpp.location -+let dummy_loc = Stdpp.dummy_loc -+let make_loc = Stdpp.make_loc -+let unloc loc = Stdpp.first_pos loc, Stdpp.last_pos loc -diff -urNad coq-8.1.pl1+dfsg~/lib/util.ml coq-8.1.pl1+dfsg/lib/util.ml ---- coq-8.1.pl1+dfsg~/lib/util.ml 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/lib/util.ml 2007-08-24 10:56:52.000000000 +0000 -@@ -34,7 +34,7 @@ - let invalid_arg_loc (loc,s) = Stdpp.raise_with_loc loc (Invalid_argument s) - let join_loc loc1 loc2 = - if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc -- else (fst loc1, snd loc2) -+ else Stdpp.encl_loc loc1 loc2 - - (* Like Exc_located, but specifies the outermost file read, the filename - associated to the location of the error, and the error itself. *) -diff -urNad coq-8.1.pl1+dfsg~/parsing/argextend.ml4 coq-8.1.pl1+dfsg/parsing/argextend.ml4 ---- coq-8.1.pl1+dfsg~/parsing/argextend.ml4 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/argextend.ml4 2007-08-24 10:56:52.000000000 +0000 -@@ -12,7 +12,7 @@ - open Q_util - open Q_coqast - --let join_loc (deb1,_) (_,fin2) = (deb1,fin2) -+let join_loc = Util.join_loc - let loc = Util.dummy_loc - let default_loc = <:expr< Util.dummy_loc >> - -@@ -226,7 +226,7 @@ - let t, g = interp_entry_name loc e sep in (g, Some (s,t)) - | s = STRING -> - if String.length s > 0 && Util.is_letter s.[0] then -- Pcoq.lexer.Token.using ("", s); -+ Pcoq.lexer.Token.tok_using ("", s); - (<:expr< (Gramext.Stoken (Lexer.terminal $str:s$)) >>, None) - ] ] - ; -diff -urNad coq-8.1.pl1+dfsg~/parsing/egrammar.mli coq-8.1.pl1+dfsg/parsing/egrammar.mli ---- coq-8.1.pl1+dfsg~/parsing/egrammar.mli 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/egrammar.mli 2007-08-24 10:56:52.000000000 +0000 -@@ -45,7 +45,7 @@ - type grammar_tactic_production = - | TacTerm of string - | TacNonTerm of -- loc * (Token.t Gramext.g_symbol * Genarg.argument_type) * string option -+ loc * ((string * string) Gramext.g_symbol * Genarg.argument_type) * string option - - val extend_tactic_grammar : - string -> grammar_tactic_production list list -> unit -@@ -61,7 +61,7 @@ - (* - val reset_extend_grammars_v8 : unit -> unit - *) --val interp_entry_name : int -> string -> entry_type * Token.t Gramext.g_symbol -+val interp_entry_name : int -> string -> entry_type * (string * string) Gramext.g_symbol - - val recover_notation_grammar : - notation -> (precedence * tolerability list) -> notation_grammar -diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.ml4 coq-8.1.pl1+dfsg/parsing/pcoq.ml4 ---- coq-8.1.pl1+dfsg~/parsing/pcoq.ml4 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/pcoq.ml4 2007-08-24 10:56:52.000000000 +0000 -@@ -30,20 +30,23 @@ - lexer. B.B. *) - - let lexer = { -- Token.func = Lexer.func; -- Token.using = Lexer.add_token; -- Token.removing = (fun _ -> ()); -- Token.tparse = Lexer.tparse; -- Token.text = Lexer.token_text } -+ Token.tok_func = Lexer.func; -+ Token.tok_using = Lexer.add_token; -+ Token.tok_removing = (fun _ -> ()); -+ Token.tok_match = Token.default_match; -+ (* Token.parse = Lexer.tparse; *) -+ Token.tok_comm = None; -+ Token.tok_text = Lexer.token_text } - - module L = - struct -+ type te = string * string - let lexer = lexer - end - - (* The parser of Coq *) - --module G = Grammar.Make(L) -+module G = Grammar.GMake(L) - - let grammar_delete e rls = - List.iter -@@ -95,7 +98,7 @@ - | ByGrammar of - grammar_object G.Entry.e * Gramext.position option * - (string option * Gramext.g_assoc option * -- (Token.t Gramext.g_symbol list * Gramext.g_action) list) list -+ ((string * string) Gramext.g_symbol list * Gramext.g_action) list) list - | ByGEXTEND of (unit -> unit) * (unit -> unit) - - let camlp4_state = ref [] -diff -urNad coq-8.1.pl1+dfsg~/parsing/pcoq.mli coq-8.1.pl1+dfsg/parsing/pcoq.mli ---- coq-8.1.pl1+dfsg~/parsing/pcoq.mli 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/pcoq.mli 2007-08-24 10:56:52.000000000 +0000 -@@ -20,9 +20,9 @@ - - (* The lexer and parser of Coq. *) - --val lexer : Token.lexer -+val lexer : (string * string) Token.glexer - --module Gram : Grammar.S with type te = Token.t -+module Gram : Grammar.S with type te = (string * string) - - (* The superclass of all grammar entries *) - type grammar_object -@@ -42,7 +42,7 @@ - val grammar_extend : - grammar_object Gram.Entry.e -> Gramext.position option -> - (string option * Gramext.g_assoc option * -- (Token.t Gramext.g_symbol list * Gramext.g_action) list) list -+ ((string * string) Gramext.g_symbol list * Gramext.g_action) list) list - -> unit - - val remove_grammars : int -> unit -@@ -210,7 +210,7 @@ - (* Binding entry names to campl4 entries *) - - val symbol_of_production : Gramext.g_assoc option -> constr_entry -> -- bool -> constr_production_entry -> Token.t Gramext.g_symbol -+ bool -> constr_production_entry -> (string * string) Gramext.g_symbol - - (* Registering/resetting the level of an entry *) - -diff -urNad coq-8.1.pl1+dfsg~/parsing/ppconstr.ml coq-8.1.pl1+dfsg/parsing/ppconstr.ml ---- coq-8.1.pl1+dfsg~/parsing/ppconstr.ml 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/ppconstr.ml 2007-08-24 10:56:52.000000000 +0000 -@@ -95,9 +95,9 @@ - let pr_delimiters key strm = - strm ++ str ("%"^key) - --let pr_located pr ((b,e),x) = -- if Options.do_translate() && (b,e)<>dummy_loc then -- let (b,e) = unloc (b,e) in -+let pr_located pr (loc,x) = -+ if Options.do_translate() && loc<>dummy_loc then -+ let (b,e) = unloc loc in - comment b ++ pr x ++ comment e - else pr x - -@@ -142,7 +142,7 @@ - | CHole _ -> mt () - | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - --let pr_lident (b,_ as loc,id) = -+let pr_lident (loc,id) = - if loc <> dummy_loc then - let (b,_) = unloc loc in - pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) -diff -urNad coq-8.1.pl1+dfsg~/parsing/ppvernac.ml coq-8.1.pl1+dfsg/parsing/ppvernac.ml ---- coq-8.1.pl1+dfsg~/parsing/ppvernac.ml 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/ppvernac.ml 2007-08-24 10:56:52.000000000 +0000 -@@ -28,7 +28,7 @@ - - let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr - --let pr_lident (b,_ as loc,id) = -+let pr_lident (loc,id) = - if loc <> dummy_loc then - let (b,_) = unloc loc in - pr_located pr_id (make_loc (b,b+String.length(string_of_id id)),id) -@@ -39,7 +39,7 @@ - - let pr_fqid fqid = str (string_of_fqid fqid) - --let pr_lfqid (_,_ as loc,fqid) = -+let pr_lfqid (loc,fqid) = - if loc <> dummy_loc then - let (b,_) = unloc loc in - pr_located pr_fqid (make_loc (b,b+String.length(string_of_fqid fqid)),fqid) -diff -urNad coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4 coq-8.1.pl1+dfsg/parsing/q_coqast.ml4 ---- coq-8.1.pl1+dfsg~/parsing/q_coqast.ml4 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/q_coqast.ml4 2007-08-24 10:56:52.000000000 +0000 -@@ -22,10 +22,8 @@ - let anti loc x = - let e = - let loc = -- ifdef OCAML_308 then -- loc -- else -- (1, snd loc - fst loc) -+ loc -+ (* (1, snd loc - fst loc) *) - in <:expr< $lid:purge_str x$ >> - in - <:expr< $anti:e$ >> -diff -urNad coq-8.1.pl1+dfsg~/parsing/q_util.ml4 coq-8.1.pl1+dfsg/parsing/q_util.ml4 ---- coq-8.1.pl1+dfsg~/parsing/q_util.ml4 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/q_util.ml4 2007-08-24 10:56:52.000000000 +0000 -@@ -37,18 +37,18 @@ - List.fold_right - (fun e1 e2 -> - let e1 = f e1 in -- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in -+ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< [$e1$ :: $e2$] >>) - l (let loc = dummy_loc in <:expr< [] >>) - - let mlexpr_of_pair m1 m2 (a1,a2) = - let e1 = m1 a1 and e2 = m2 a2 in -- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e2)) in -+ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e2) in - <:expr< ($e1$, $e2$) >> - - let mlexpr_of_triple m1 m2 m3 (a1,a2,a3)= - let e1 = m1 a1 and e2 = m2 a2 and e3 = m3 a3 in -- let loc = (fst (MLast.loc_of_expr e1), snd (MLast.loc_of_expr e3)) in -+ let loc = join_loc (MLast.loc_of_expr e1) (MLast.loc_of_expr e3) in - <:expr< ($e1$, $e2$, $e3$) >> - - (* We don't give location for tactic quotation! *) -diff -urNad coq-8.1.pl1+dfsg~/parsing/tacextend.ml4 coq-8.1.pl1+dfsg/parsing/tacextend.ml4 ---- coq-8.1.pl1+dfsg~/parsing/tacextend.ml4 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/tacextend.ml4 2007-08-24 10:56:52.000000000 +0000 -@@ -13,7 +13,7 @@ - open Q_coqast - open Argextend - --let join_loc (deb1,_) (_,fin2) = (deb1,fin2) -+let join_loc = Util.join_loc - let loc = Util.dummy_loc - let default_loc = <:expr< Util.dummy_loc >> - -diff -urNad coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4 coq-8.1.pl1+dfsg/parsing/vernacextend.ml4 ---- coq-8.1.pl1+dfsg~/parsing/vernacextend.ml4 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/parsing/vernacextend.ml4 2007-08-24 10:56:52.000000000 +0000 -@@ -13,7 +13,7 @@ - open Q_coqast - open Argextend - --let join_loc (deb1,_) (_,fin2) = (deb1,fin2) -+let join_loc = Util.join_loc - let loc = Util.dummy_loc - let default_loc = <:expr< Util.dummy_loc >> - -diff -urNad coq-8.1.pl1+dfsg~/scripts/coqmktop.ml coq-8.1.pl1+dfsg/scripts/coqmktop.ml ---- coq-8.1.pl1+dfsg~/scripts/coqmktop.ml 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/scripts/coqmktop.ml 2007-08-24 10:57:13.000000000 +0000 -@@ -32,7 +32,7 @@ - - (* 3. Toplevel objects *) - let camlp4topobjs = -- ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] -+ ["camlp5_top.cma"; "camlp5o.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"] - let topobjs = camlp4topobjs - - let gramobjs = [] -@@ -285,12 +285,12 @@ - (* native code *) - if !top then failwith "no custom toplevel in native code !"; - let ocamloptexec = Filename.concat Coq_config.camldir "ocamlopt" in -- (if !caml_inline_0 then ocamloptexec^" -linkall"^" -inline 0" else ocamloptexec^" -linkall") -+ (if !caml_inline_0 then ocamloptexec^" -linkall -rectypes"^" -inline 0" else ocamloptexec^" -linkall -rectypes") - end else - (* bytecode (we shunt ocamlmktop script which fails on win32) *) - let ocamlmktoplib = " toplevellib.cma" in - let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in -- let ocamlccustom = ocamlcexec^" -custom -linkall" in -+ let ocamlccustom = ocamlcexec^" -custom -linkall -rectypes" in - (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom) - in - (* files to link *) -diff -urNad coq-8.1.pl1+dfsg~/tools/coq_makefile.ml4 coq-8.1.pl1+dfsg/tools/coq_makefile.ml4 ---- coq-8.1.pl1+dfsg~/tools/coq_makefile.ml4 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/tools/coq_makefile.ml4 2007-08-24 10:56:52.000000000 +0000 -@@ -175,7 +175,7 @@ - | _ :: r -> var_aux r - in - section "Variables definitions."; -- print "CAMLP4LIB=`camlp4 -where`\n"; -+ print "CAMLP4LIB=`camlp5 -where`\n"; - (* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *) - print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\ - -I $(COQTOP)/library -I $(COQTOP)/parsing \\ -@@ -204,8 +204,8 @@ - print "CAMLOPTLINK=ocamlopt\n"; - print "COQDEP=$(COQBIN)coqdep -c\n"; - print "GRAMMARS=grammar.cma\n"; -- print "CAMLP4EXTEND=pa_extend.cmo pa_ifdef.cmo q_MLast.cmo\n"; -- print "PP=-pp \"camlp4o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; -+ print "CAMLP4EXTEND=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; -+ print "PP=-pp \"camlp5o -I . -I $(COQTOP)/parsing $(CAMLP4EXTEND) $(GRAMMARS) -impl\"\n"; - var_aux l; - print "\n" - -diff -urNad coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml coq-8.1.pl1+dfsg/toplevel/metasyntax.ml ---- coq-8.1.pl1+dfsg~/toplevel/metasyntax.ml 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/toplevel/metasyntax.ml 2007-08-24 10:56:52.000000000 +0000 -@@ -28,7 +28,7 @@ - (**********************************************************************) - (* Tokens *) - --let cache_token (_,s) = Pcoq.lexer.Token.using ("", s) -+let cache_token (_,s) = Pcoq.lexer.Token.tok_using ("", s) - - let (inToken, outToken) = - declare_object {(default_object "TOKEN") with -diff -urNad coq-8.1.pl1+dfsg~/toplevel/mltop.ml4 coq-8.1.pl1+dfsg/toplevel/mltop.ml4 ---- coq-8.1.pl1+dfsg~/toplevel/mltop.ml4 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/toplevel/mltop.ml4 2007-08-24 10:56:52.000000000 +0000 -@@ -98,7 +98,7 @@ - str s; str" to Coq code." >]) - (* TO DO: .cma loading without toplevel *) - | WithoutTop -> -- ifdef Byte then -+ IFDEF Byte THEN - let _,gname = where_in_path !coq_mlpath_copy s in - try - Dynlink.loadfile gname; -@@ -108,7 +108,7 @@ - [Filename.dirname gname] - with | Dynlink.Error a -> - errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >] -- else () -+ ELSE () END - | Native -> - errorlabstrm "Mltop.no_load_object" - [< str"Loading of ML object file forbidden in a native Coq" >] -diff -urNad coq-8.1.pl1+dfsg~/toplevel/toplevel.ml coq-8.1.pl1+dfsg/toplevel/toplevel.ml ---- coq-8.1.pl1+dfsg~/toplevel/toplevel.ml 2007-08-24 10:56:51.000000000 +0000 -+++ coq-8.1.pl1+dfsg/toplevel/toplevel.ml 2007-08-24 10:56:52.000000000 +0000 -@@ -139,16 +139,16 @@ - - (* Functions to report located errors in a file. *) - --let print_location_in_file s inlibrary fname (bp,ep) = -+let print_location_in_file s inlibrary fname loc = - let errstrm = (str"Error while reading " ++ str s ++ str" :" ++ fnl ()) in -- if (bp,ep) = dummy_loc then -+ if loc = dummy_loc then - (errstrm ++ str", unknown location." ++ fnl ()) - else - if inlibrary then - (errstrm ++ str"Module " ++ str ("\""^fname^"\"") ++ -- str" characters " ++ Cerrors.print_loc (bp,ep) ++ fnl ()) -+ str" characters " ++ Cerrors.print_loc loc ++ fnl ()) - else -- let (bp,ep) = unloc (bp,ep) in -+ let (bp,ep) = unloc loc in - let ic = open_in fname in - let rec line_of_pos lin bol cnt = - if cnt < bp then -@@ -172,15 +172,16 @@ - str(String.sub ib.str (bp-ib.start) (ep-bp)) ++ fnl ()) - | None -> (mt ()) - --let valid_loc dloc (b,e) = -- (b,e) <> dummy_loc -+let valid_loc dloc loc = -+ let b, e = unloc loc in -+ loc <> dummy_loc - & match dloc with -- | Some (bd,ed) -> bd<=b & e<=ed -+ | Some dloc -> let bd,ed = unloc dloc in bd<=b & e<=ed - | _ -> true - --let valid_buffer_loc ib dloc (b,e) = -- valid_loc dloc (b,e) & -- let (b,e) = unloc (b,e) in b-ib.start >= 0 & e-ib.start < ib.len & b<=e -+let valid_buffer_loc ib dloc loc = -+ valid_loc dloc loc & -+ let (b,e) = unloc loc in b-ib.start >= 0 & e-ib.start < ib.len & b<=e - - (*s The Coq prompt is the name of the focused proof, if any, and "Coq" - otherwise. We trap all exceptions to prevent the error message printing diff --git a/debian/patches/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch index fb618f56..f59f52e0 100755 --- a/debian/patches/coqdoc_stdlib.dpatch +++ b/debian/patches/coqdoc_stdlib.dpatch @@ -6,14 +6,14 @@ ## DP: to be able to build the documentation before coqdoc is installed. @DPATCH@ -diff -urNad coq-8.0pl3+8.1beta~/doc/Makefile coq-8.0pl3+8.1beta/doc/Makefile ---- coq-8.0pl3+8.1beta~/doc/Makefile 2006-06-16 13:02:33.000000000 +0000 -+++ coq-8.0pl3+8.1beta/doc/Makefile 2006-06-16 13:19:11.000000000 +0000 -@@ -216,6 +216,7 @@ +diff -urNad coq-8.1.pl2+dfsg~/doc/Makefile coq-8.1.pl2+dfsg/doc/Makefile +--- coq-8.1.pl2+dfsg~/doc/Makefile 2007-10-15 11:45:13.000000000 +0000 ++++ coq-8.1.pl2+dfsg/doc/Makefile 2007-10-15 11:45:40.000000000 +0000 +@@ -222,6 +222,7 @@ mkdir stdlib/html (cd stdlib/html;\ $(COQDOC) -q --multi-index --html --glob-from $(GLOBDUMP)\ -+ --coqlib_path $(COQTOP) \ - -R $(COQTOP)/theories Coq $(COQTOP)/theories/*/*.v) ++ --coqlib_path $(COQSRC) \ + -R $(COQSRC)/theories Coq $(COQSRC)/theories/*/*.v) mv stdlib/html/index.html stdlib/index-body.html diff --git a/debian/patches/makefile.dpatch b/debian/patches/makefile.dpatch index b656a9bb..d16030ca 100755 --- a/debian/patches/makefile.dpatch +++ b/debian/patches/makefile.dpatch @@ -6,15 +6,15 @@ ## DP: when compiling on non-native archs. @DPATCH@ -diff -urNad coq-8.0pl3+8.1alpha~/Makefile coq-8.0pl3+8.1alpha/Makefile ---- coq-8.0pl3+8.1alpha~/Makefile 2006-04-07 15:08:12.000000000 +0000 -+++ coq-8.0pl3+8.1alpha/Makefile 2006-04-30 11:41:09.000000000 +0000 -@@ -1401,7 +1401,7 @@ +diff -urNad coq-8.1.pl2+dfsg~/Makefile coq-8.1.pl2+dfsg/Makefile +--- coq-8.1.pl2+dfsg~/Makefile 2007-10-15 11:02:54.000000000 +0000 ++++ coq-8.1.pl2+dfsg/Makefile 2007-10-15 11:03:55.000000000 +0000 +@@ -1479,7 +1479,7 @@ parsing/grammar.cma: $(GRAMMARCMO) $(SHOW)'Testing $@' @touch test.ml4 -- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar -+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar +- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar ++ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENSIONS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@ -- cgit v1.2.3