From c0b8f31b4a47183309c8599338a5394f16e1684e Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Started to package the upcoming 8.1 release. --- debian/changelog | 10 + debian/control | 19 +- debian/coq-libs.dirs | 2 + debian/coq-libs.doc-base | 9 + debian/coq-libs.install | 2 +- debian/coq.install | 1 - debian/coq7-libs.install | 3 - debian/coqide.install | 3 +- debian/patches/00list | 2 +- debian/patches/coq-8.0pl3-ocaml-3.09.dpatch | 507 ---------------------------- debian/patches/coqdoc_stdlib.dpatch | 72 ++++ debian/rules | 18 +- 12 files changed, 110 insertions(+), 538 deletions(-) create mode 100644 debian/coq-libs.dirs create mode 100644 debian/coq-libs.doc-base delete mode 100644 debian/coq7-libs.install delete mode 100755 debian/patches/coq-8.0pl3-ocaml-3.09.dpatch create mode 100755 debian/patches/coqdoc_stdlib.dpatch (limited to 'debian') diff --git a/debian/changelog b/debian/changelog index afb42a67..b60769ed 100644 --- a/debian/changelog +++ b/debian/changelog @@ -1,3 +1,13 @@ +coq (8.0pl3+8.1alpha-1) experimental; urgency=low + + * New upstream release. + * Disabling checks for now as they don't succeed. + * Removed coq-8.0pl3-ocaml-3.09.dpatch. + * No longer providing the compatibility coq7-libs package. + * coq-libs is now providing its documentation in html format. + + -- Samuel Mimram Thu, 27 Apr 2006 13:43:16 +0000 + coq (8.0pl3-2) unstable; urgency=low * Added coq-8.0pl3-ocaml-3.09.dpatch in order to prevent intuition from diff --git a/debian/control b/debian/control index 9ec22d2f..bd35a5ba 100644 --- a/debian/control +++ b/debian/control @@ -4,7 +4,7 @@ Priority: optional Maintainer: Debian OCaml Maintainers Uploaders: Ralf Treinen , Sven Luther , Remi Vanicat , Stefano Zacchiroli , Samuel Mimram Standards-Version: 3.6.2 -Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), chrpath +Build-Depends: debhelper (>= 4.0.0), dpatch, ocaml-nox (>= 3.09.0), ocaml-best-compilers, liblablgtk2-ocaml-dev (>= 2.4.0), chrpath, tetex-bin Package: coq Architecture: any @@ -39,7 +39,7 @@ Description: proof assistant for higher-order logic (gtk interface) Package: coq-libs Architecture: all Recommends: coq (>= 8.0) -Conflicts: coq (<< 8.0) +Conflicts: coq (<< 8.0), coq-doc (<= 8.0pl1.0-2) Description: proof assistant for higher-order logic (theories) Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal @@ -48,18 +48,3 @@ 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: coq7-libs -Architecture: all -Recommends: coq (>= 8.0) -Description: proof assistant for higher-order logic (Coq 7 theories) - 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 Camlp4. - For more information, see . - . - This package provides existing theories from Coq 7 in Coq 8, and - allows proofs that were developed in Coq 7 to be used in Coq 8. - It is also required to translate theories in Coq 7 syntax into - the new syntax introduced in Coq 8. However, this package does - not need to be installed to use Coq 7. diff --git a/debian/coq-libs.dirs b/debian/coq-libs.dirs new file mode 100644 index 00000000..aadcf27a --- /dev/null +++ b/debian/coq-libs.dirs @@ -0,0 +1,2 @@ +usr/share/doc/coq-libs +usr/share/doc/coq diff --git a/debian/coq-libs.doc-base b/debian/coq-libs.doc-base new file mode 100644 index 00000000..1a62a262 --- /dev/null +++ b/debian/coq-libs.doc-base @@ -0,0 +1,9 @@ +Document: coq-library +Title: The Coq Standard Library +Author: The Coq Development Team +Abstract: Standard Library documentation of version 8.0 of the Coq proof assistant which is a system designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that programs are correct with respect to their specification. +Section: Apps/Math + +Format: HTML +Index: /usr/share/doc/coq-libs/html/index.html +Files: /usr/share/doc/coq-libs/html/*.html diff --git a/debian/coq-libs.install b/debian/coq-libs.install index c721f0c8..653e2b54 100644 --- a/debian/coq-libs.install +++ b/debian/coq-libs.install @@ -1,4 +1,4 @@ usr/lib/coq/contrib usr/lib/coq/states usr/lib/coq/theories -usr/lib/coq/ide/utf8.vo usr/lib/coq +usr/lib/coq/ide/utf8.vo usr/lib/coq diff --git a/debian/coq.install b/debian/coq.install index d1182ab6..155e13af 100644 --- a/debian/coq.install +++ b/debian/coq.install @@ -9,7 +9,6 @@ usr/bin/coqtop* usr/bin/coqwc usr/bin/gallina usr/share/emacs/site-lisp/coq -usr/share/emacs/site-lisp/coqdoc.sty usr/share/man/man1/c* usr/share/man/man1/gallina.1 usr/share/texmf/tex/latex/misc/* diff --git a/debian/coq7-libs.install b/debian/coq7-libs.install deleted file mode 100644 index e888a17f..00000000 --- a/debian/coq7-libs.install +++ /dev/null @@ -1,3 +0,0 @@ -usr/lib/coq/contrib7 -usr/lib/coq/states7 -usr/lib/coq/theories7 diff --git a/debian/coqide.install b/debian/coqide.install index 7df75581..f214e01c 100644 --- a/debian/coqide.install +++ b/debian/coqide.install @@ -1,5 +1,4 @@ usr/bin/coqide* -usr/lib/coq/ide/coq.ico -usr/lib/coq/ide/coq2.ico +usr/lib/coq/ide/coq.png usr/lib/coq/ide/utf8.vo usr/lib/coq/ide/.coqide-gtk2rc diff --git a/debian/patches/00list b/debian/patches/00list index 3804c9ad..fa82f62e 100644 --- a/debian/patches/00list +++ b/debian/patches/00list @@ -1 +1 @@ -coq-8.0pl3-ocaml-3.09 +coqdoc_stdlib diff --git a/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch b/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch deleted file mode 100755 index 90b4d583..00000000 --- a/debian/patches/coq-8.0pl3-ocaml-3.09.dpatch +++ /dev/null @@ -1,507 +0,0 @@ -#! /bin/sh /usr/share/dpatch/dpatch-run -## coq-8.0pl3-ocaml-3.09.dpatch by Samuel Mimram -## -## All lines beginning with `## DP:' are a description of the patch. -## DP: Patch provided by coq's upstream to fix problems with OCaml 3.09. -## DP: ftp://ftp.inria.fr/INRIA/coq/V8.0pl3/patch-coq-8.0pl3-ocaml-3.09 - -@DPATCH@ -diff -urNad coq-8.0pl3~/Makefile coq-8.0pl3/Makefile ---- coq-8.0pl3~/Makefile 2006-01-11 23:18:05.000000000 +0000 -+++ coq-8.0pl3/Makefile 2006-02-19 11:28:43.000000000 +0000 -@@ -77,8 +77,8 @@ - - MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) - --BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) --OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -+BYTEFLAGS=$(MLINCLUDES) $(CAMLDEBUG) -w y -+OPTFLAGS=$(MLINCLUDES) $(CAMLTIMEPROF) -w y - OCAMLDEP=ocamldep - DEPFLAGS=-slash $(LOCALINCLUDES) - -diff -urNad coq-8.0pl3~/contrib/first-order/sequent.ml coq-8.0pl3/contrib/first-order/sequent.ml ---- coq-8.0pl3~/contrib/first-order/sequent.ml 2004-07-16 19:30:10.000000000 +0000 -+++ coq-8.0pl3/contrib/first-order/sequent.ml 2006-02-19 11:28:43.000000000 +0000 -@@ -6,7 +6,7 @@ - (* * GNU Lesser General Public License Version 2.1 *) - (************************************************************************) - --(* $Id: sequent.ml,v 1.17.2.1 2004/07/16 19:30:10 herbelin Exp $ *) -+(* $Id: sequent.ml,v 1.17.2.2 2006/01/25 22:40:30 herbelin Exp $ *) - - open Term - open Util -@@ -278,7 +278,7 @@ - let h dbname= - let hdb= - try -- Util.Stringmap.find dbname !searchtable -+ searchtable_map dbname - with Not_found-> - error ("Firstorder: "^dbname^" : No such Hint database") in - Hint_db.iter g hdb in -diff -urNad coq-8.0pl3~/contrib/interface/blast.ml coq-8.0pl3/contrib/interface/blast.ml ---- coq-8.0pl3~/contrib/interface/blast.ml 2004-07-16 19:30:11.000000000 +0000 -+++ coq-8.0pl3/contrib/interface/blast.ml 2006-02-19 11:28:43.000000000 +0000 -@@ -351,16 +351,16 @@ - let db_list = - List.map - (fun x -> -- try Stringmap.find x !searchtable -+ try searchtable_map x - with Not_found -> error ("EAuto: "^x^": No such Hint database")) - ("core"::dbnames) - in - tclTRY (e_search_auto debug np db_list) - - let full_eauto debug n gl = -- let dbnames = stringmap_dom !searchtable in -+ let dbnames = current_db_names () in - let dbnames = list_subtract dbnames ["v62"] in -- let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in -+ let db_list = List.map searchtable_map dbnames in - let local_db = make_local_hint_db gl in - tclTRY (e_search_auto debug n db_list) gl - -@@ -369,8 +369,6 @@ - (********************************************************************** - copié de tactics/auto.ml on a juste modifié search_gen - *) --let searchtable_map name = -- Stringmap.find name !searchtable - - (* local_db is a Hint database containing the hypotheses of current goal *) - (* Papageno : cette fonction a été pas mal simplifiée depuis que la base -@@ -499,9 +497,9 @@ - let default_search_depth = ref 5 - - let full_auto n gl = -- let dbnames = stringmap_dom !searchtable in -+ let dbnames = current_db_names () in - let dbnames = list_subtract dbnames ["v62"] in -- let db_list = List.map (fun x -> searchtable_map x) dbnames in -+ let db_list = List.map searchtable_map dbnames in - let hyps = pf_hyps gl in - tclTRY (search n db_list (make_local_hint_db gl) hyps) gl - -diff -urNad coq-8.0pl3~/interp/symbols.ml coq-8.0pl3/interp/symbols.ml ---- coq-8.0pl3~/interp/symbols.ml 2004-11-17 09:33:38.000000000 +0000 -+++ coq-8.0pl3/interp/symbols.ml 2006-02-19 11:28:43.000000000 +0000 -@@ -6,7 +6,7 @@ - (* * GNU Lesser General Public License Version 2.1 *) - (************************************************************************) - --(* $Id: symbols.ml,v 1.31.2.2 2004/11/17 09:33:38 herbelin Exp $ *) -+(* $Id: symbols.ml,v 1.31.2.3 2006/01/25 22:40:30 herbelin Exp $ *) - - (*i*) - open Util -@@ -43,18 +43,18 @@ - type delimiters = string - - type scope = { -- notations: (interpretation * (dir_path * string) * bool) Stringmap.t; -+ notations: (string, interpretation * (dir_path * string) * bool) Gmap.t; - delimiters: delimiters option - } - - (* Uninterpreted notation map: notation -> level * dir_path *) --let notation_level_map = ref Stringmap.empty -+let notation_level_map = ref Gmap.empty - - (* Scopes table: scope_name -> symbol_interpretation *) --let scope_map = ref Stringmap.empty -+let scope_map = ref Gmap.empty - - let empty_scope = { -- notations = Stringmap.empty; -+ notations = Gmap.empty; - delimiters = None - } - -@@ -62,20 +62,20 @@ - let type_scope = "type_scope" (* special scope used for interpreting types *) - - let init_scope_map () = -- scope_map := Stringmap.add default_scope empty_scope !scope_map; -- scope_map := Stringmap.add type_scope empty_scope !scope_map -+ scope_map := Gmap.add default_scope empty_scope !scope_map; -+ scope_map := Gmap.add type_scope empty_scope !scope_map - - (**********************************************************************) - (* Operations on scopes *) - - let declare_scope scope = -- try let _ = Stringmap.find scope !scope_map in () -+ try let _ = Gmap.find scope !scope_map in () - with Not_found -> - (* Options.if_verbose message ("Creating scope "^scope);*) -- scope_map := Stringmap.add scope empty_scope !scope_map -+ scope_map := Gmap.add scope empty_scope !scope_map - - let find_scope scope = -- try Stringmap.find scope !scope_map -+ try Gmap.find scope !scope_map - with Not_found -> error ("Scope "^scope^" is not declared") - - let check_scope sc = let _ = find_scope sc in () -@@ -124,7 +124,7 @@ - (**********************************************************************) - (* Delimiters *) - --let delimiters_map = ref Stringmap.empty -+let delimiters_map = ref Gmap.empty - - let declare_delimiters scope key = - let sc = find_scope scope in -@@ -134,15 +134,15 @@ - warning ("Overwritting previous delimiting key "^old^" in scope "^scope) - end; - let sc = { sc with delimiters = Some key } in -- scope_map := Stringmap.add scope sc !scope_map; -- if Stringmap.mem key !delimiters_map then begin -- let oldsc = Stringmap.find key !delimiters_map in -+ scope_map := Gmap.add scope sc !scope_map; -+ if Gmap.mem key !delimiters_map then begin -+ let oldsc = Gmap.find key !delimiters_map in - Options.if_verbose warning ("Hidding binding of key "^key^" to "^oldsc) - end; -- delimiters_map := Stringmap.add key scope !delimiters_map -+ delimiters_map := Gmap.add key scope !delimiters_map - - let find_delimiters_scope loc key = -- try Stringmap.find key !delimiters_map -+ try Gmap.find key !delimiters_map - with Not_found -> - user_err_loc - (loc, "find_delimiters", str ("Unknown scope delimiting key "^key)) -@@ -229,7 +229,7 @@ - let find_with_delimiters = function - | None -> None - | Some scope -> -- match (Stringmap.find scope !scope_map).delimiters with -+ match (Gmap.find scope !scope_map).delimiters with - | Some key -> Some (Some scope, Some key) - | None -> None - -@@ -257,23 +257,23 @@ - (* Uninterpreted notation levels *) - - let declare_notation_level ntn level = -- if not !Options.v7 & Stringmap.mem ntn !notation_level_map then -+ if not !Options.v7 & Gmap.mem ntn !notation_level_map then - error ("Notation "^ntn^" is already assigned a level"); -- notation_level_map := Stringmap.add ntn level !notation_level_map -+ notation_level_map := Gmap.add ntn level !notation_level_map - - let level_of_notation ntn = -- Stringmap.find ntn !notation_level_map -+ Gmap.find ntn !notation_level_map - - (* The mapping between notations and their interpretation *) - - let declare_notation_interpretation ntn scopt pat df pp8only = - let scope = match scopt with Some s -> s | None -> default_scope in - let sc = find_scope scope in -- if Stringmap.mem ntn sc.notations && Options.is_verbose () then -+ if Gmap.mem ntn sc.notations && Options.is_verbose () then - warning ("Notation "^ntn^" was already used"^ - (if scopt = None then "" else " in scope "^scope)); -- let sc = { sc with notations = Stringmap.add ntn (pat,df,pp8only) sc.notations } in -- scope_map := Stringmap.add scope sc !scope_map; -+ let sc = { sc with notations = Gmap.add ntn (pat,df,pp8only) sc.notations } in -+ scope_map := Gmap.add scope sc !scope_map; - if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack - - let declare_uninterpretation rule (metas,c as pat) = -@@ -292,7 +292,7 @@ - let rec interp_notation loc ntn scopes = - let f sc = - let scope = find_scope sc in -- let (pat,df,pp8only) = Stringmap.find ntn scope.notations in -+ let (pat,df,pp8only) = Gmap.find ntn scope.notations in - if pp8only then raise Not_found; - pat,(df,if sc = default_scope then None else Some sc) in - try find_interpretation f (List.fold_right push_scope scopes !scope_stack) -@@ -308,7 +308,7 @@ - - let availability_of_notation (ntn_scope,ntn) scopes = - let f scope = -- Stringmap.mem ntn (Stringmap.find scope !scope_map).notations in -+ Gmap.mem ntn (Gmap.find scope !scope_map).notations in - find_without_delimiters f (ntn_scope,Some ntn) scopes - - let rec interp_numeral_gen loc f n = function -@@ -356,8 +356,8 @@ - let exists_notation_in_scope scopt ntn r = - let scope = match scopt with Some s -> s | None -> default_scope in - try -- let sc = Stringmap.find scope !scope_map in -- let (r',_,pp8only) = Stringmap.find ntn sc.notations in -+ let sc = Gmap.find scope !scope_map in -+ let (r',_,pp8only) = Gmap.find ntn sc.notations in - r' = r, pp8only - with Not_found -> false, false - -@@ -487,14 +487,14 @@ - - let pr_named_scope prraw scope sc = - (if scope = default_scope then -- match Stringmap.fold (fun _ _ x -> x+1) sc.notations 0 with -+ match Gmap.fold (fun _ _ x -> x+1) sc.notations 0 with - | 0 -> str "No lonely notation" - | n -> str "Lonely notation" ++ (if n=1 then mt() else str"s") - else - str "Scope " ++ str scope ++ fnl () ++ pr_delimiters_info sc.delimiters) - ++ fnl () - ++ pr_scope_classes scope -- ++ Stringmap.fold -+ ++ Gmap.fold - (fun ntn ((_,r),(_,df),_) strm -> - pr_notation_info prraw df r ++ fnl () ++ strm) - sc.notations (mt ()) -@@ -502,12 +502,12 @@ - let pr_scope prraw scope = pr_named_scope prraw scope (find_scope scope) - - let pr_scopes prraw = -- Stringmap.fold -+ Gmap.fold - (fun scope sc strm -> pr_named_scope prraw scope sc ++ fnl () ++ strm) - !scope_map (mt ()) - - let rec find_default ntn = function -- | Scope scope::_ when Stringmap.mem ntn (find_scope scope).notations -> -+ | Scope scope::_ when Gmap.mem ntn (find_scope scope).notations -> - Some scope - | SingleNotation ntn'::_ when ntn = ntn' -> Some default_scope - | _::scopes -> find_default ntn scopes -@@ -531,9 +531,9 @@ - if String.contains ntn ' ' then (=) ntn - else fun ntn' -> List.mem (Terminal ntn) (decompose_notation_key ntn') in - let l = -- Stringmap.fold -+ Gmap.fold - (fun scope_name sc -> -- Stringmap.fold (fun ntn ((_,r),df,_) l -> -+ Gmap.fold (fun ntn ((_,r),df,_) l -> - if find ntn then (ntn,(scope_name,r,df))::l else l) sc.notations) - map [] in - let l = List.sort (fun x y -> Pervasives.compare (fst x) (fst y)) l in -@@ -560,7 +560,7 @@ - - let collect_notation_in_scope scope sc known = - assert (scope <> default_scope); -- Stringmap.fold -+ Gmap.fold - (fun ntn ((_,r),(_,df),_) (l,known as acc) -> - if List.mem ntn known then acc else ((df,r)::l,ntn::known)) - sc.notations ([],known) -@@ -578,7 +578,7 @@ - if List.mem ntn knownntn then (all,knownntn) - else - let ((_,r),(_,df),_) = -- Stringmap.find ntn (find_scope default_scope).notations in -+ Gmap.find ntn (find_scope default_scope).notations in - let all' = match all with - | (s,lonelyntn)::rest when s = default_scope -> - (s,(df,r)::lonelyntn)::rest -@@ -614,13 +614,13 @@ - - (* Concrete syntax for symbolic-extension table *) - let printing_rules = -- ref (Stringmap.empty : unparsing_rule Stringmap.t) -+ ref (Gmap.empty : (string, unparsing_rule) Gmap.t) - - let declare_notation_printing_rule ntn unpl = -- printing_rules := Stringmap.add ntn unpl !printing_rules -+ printing_rules := Gmap.add ntn unpl !printing_rules - - let find_notation_printing_rule ntn = -- try Stringmap.find ntn !printing_rules -+ try Gmap.find ntn !printing_rules - with Not_found -> anomaly ("No printing rule found for "^ntn) - - (**********************************************************************) -@@ -644,13 +644,13 @@ - let init () = - init_scope_map (); - (* -- scope_stack := Stringmap.empty -+ scope_stack := Gmap.empty - arguments_scope := Refmap.empty - *) -- notation_level_map := Stringmap.empty; -- delimiters_map := Stringmap.empty; -+ notation_level_map := Gmap.empty; -+ delimiters_map := Gmap.empty; - notations_key_table := Gmapl.empty; -- printing_rules := Stringmap.empty; -+ printing_rules := Gmap.empty; - class_scope_map := Gmap.add CL_SORT "type_scope" Gmap.empty - - let _ = -diff -urNad coq-8.0pl3~/tactics/auto.ml coq-8.0pl3/tactics/auto.ml ---- coq-8.0pl3~/tactics/auto.ml 2005-05-15 12:47:04.000000000 +0000 -+++ coq-8.0pl3/tactics/auto.ml 2006-02-19 11:28:43.000000000 +0000 -@@ -6,7 +6,7 @@ - (* * GNU Lesser General Public License Version 2.1 *) - (************************************************************************) - --(* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *) -+(* $Id: auto.ml,v 1.63.2.4 2006/01/25 22:40:29 herbelin Exp $ *) - - open Pp - open Util -@@ -134,24 +134,28 @@ - - end - --type frozen_hint_db_table = Hint_db.t Stringmap.t -+module Hintdbmap = Gmap - --type hint_db_table = Hint_db.t Stringmap.t ref -+type frozen_hint_db_table = (string,Hint_db.t) Hintdbmap.t -+ -+type hint_db_table = (string,Hint_db.t) Hintdbmap.t ref - - type hint_db_name = string - --let searchtable = (ref Stringmap.empty : hint_db_table) -+let searchtable = (ref Hintdbmap.empty : hint_db_table) - - let searchtable_map name = -- Stringmap.find name !searchtable -+ Hintdbmap.find name !searchtable - let searchtable_add (name,db) = -- searchtable := Stringmap.add name db !searchtable -+ searchtable := Hintdbmap.add name db !searchtable -+let current_db_names () = -+ Hintdbmap.dom !searchtable - - (**************************************************************************) - (* Definition of the summary *) - (**************************************************************************) - --let init () = searchtable := Stringmap.empty -+let init () = searchtable := Hintdbmap.empty - let freeze () = !searchtable - let unfreeze fs = searchtable := fs - -@@ -498,7 +502,7 @@ - - (* Print all hints associated to head c in any database *) - let fmt_hint_list_for_head c = -- let dbs = stringmap_to_list !searchtable in -+ let dbs = Hintdbmap.to_list !searchtable in - let valid_dbs = - map_succeed - (fun (name,db) -> (name,db,Hint_db.map_all c db)) -@@ -523,7 +527,7 @@ - | [] -> assert false - in - let hd = head_of_constr_reference hdc in -- let dbs = stringmap_to_list !searchtable in -+ let dbs = Hintdbmap.to_list !searchtable in - let valid_dbs = - if occur_existential cl then - map_succeed -@@ -568,7 +572,7 @@ - - (* displays all the hints of all databases *) - let print_searchtable () = -- Stringmap.iter -+ Hintdbmap.iter - (fun name db -> - msg (str "In the database " ++ str name ++ fnl ()); - print_hint_db db) -@@ -693,7 +697,7 @@ - tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl - - let full_trivial gl = -- let dbnames = stringmap_dom !searchtable in -+ let dbnames = Hintdbmap.dom !searchtable in - let dbnames = list_subtract dbnames ["v62"] in - let db_list = List.map (fun x -> searchtable_map x) dbnames in - tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl -@@ -798,7 +802,7 @@ - let default_auto = auto !default_search_depth [] - - let full_auto n gl = -- let dbnames = stringmap_dom !searchtable in -+ let dbnames = Hintdbmap.dom !searchtable in - let dbnames = list_subtract dbnames ["v62"] in - let db_list = List.map (fun x -> searchtable_map x) dbnames in - let hyps = pf_hyps gl in -@@ -911,7 +915,7 @@ - to_add empty_named_context in - let db0 = list_map_append (make_resolve_hyp (pf_env g) (project g)) sigma in - let db = Hint_db.add_list db0 (make_local_hint_db g) in -- super_search n [Stringmap.find "core" !searchtable] db argl g -+ super_search n [Hintdbmap.find "core" !searchtable] db argl g - - let superauto n to_add argl = - tclTRY (tclCOMPLETE (search_superauto n to_add argl)) -diff -urNad coq-8.0pl3~/tactics/auto.mli coq-8.0pl3/tactics/auto.mli ---- coq-8.0pl3~/tactics/auto.mli 2005-01-21 16:41:52.000000000 +0000 -+++ coq-8.0pl3/tactics/auto.mli 2006-02-19 11:28:43.000000000 +0000 -@@ -6,7 +6,7 @@ - (* * GNU Lesser General Public License Version 2.1 *) - (************************************************************************) - --(*i $Id: auto.mli,v 1.22.2.2 2005/01/21 16:41:52 herbelin Exp $ i*) -+(*i $Id: auto.mli,v 1.22.2.3 2006/01/25 22:40:29 herbelin Exp $ i*) - - (*i*) - open Util -@@ -56,12 +56,16 @@ - val iter : (constr_label -> stored_data list -> unit) -> t -> unit - end - --type frozen_hint_db_table = Hint_db.t Stringmap.t -+type frozen_hint_db_table - --type hint_db_table = Hint_db.t Stringmap.t ref -+type hint_db_table - - type hint_db_name = string - -+val searchtable_map : hint_db_name -> Hint_db.t -+ -+val current_db_names : unit -> hint_db_name list -+ - val add_hints : locality_flag -> hint_db_name list -> hints -> unit - - val print_searchtable : unit -> unit -diff -urNad coq-8.0pl3~/tactics/eauto.ml4 coq-8.0pl3/tactics/eauto.ml4 ---- coq-8.0pl3~/tactics/eauto.ml4 2004-07-16 19:30:52.000000000 +0000 -+++ coq-8.0pl3/tactics/eauto.ml4 2006-02-19 11:28:43.000000000 +0000 -@@ -8,7 +8,7 @@ - - (*i camlp4deps: "parsing/grammar.cma" i*) - --(* $Id: eauto.ml4,v 1.11.2.1 2004/07/16 19:30:52 herbelin Exp $ *) -+(* $Id: eauto.ml4,v 1.11.2.2 2006/01/25 22:40:29 herbelin Exp $ *) - - open Pp - open Util -@@ -391,16 +391,16 @@ - let db_list = - List.map - (fun x -> -- try Stringmap.find x !searchtable -+ try searchtable_map x - with Not_found -> error ("EAuto: "^x^": No such Hint database")) - ("core"::dbnames) - in - tclTRY (e_search_auto debug np db_list) - - let full_eauto debug n gl = -- let dbnames = stringmap_dom !searchtable in -+ let dbnames = current_db_names () in - let dbnames = list_subtract dbnames ["v62"] in -- let db_list = List.map (fun x -> Stringmap.find x !searchtable) dbnames in -+ let db_list = List.map (fun x -> searchtable_map x) dbnames in - let local_db = make_local_hint_db gl in - tclTRY (e_search_auto debug n db_list) gl - diff --git a/debian/patches/coqdoc_stdlib.dpatch b/debian/patches/coqdoc_stdlib.dpatch new file mode 100755 index 00000000..d81ce3c8 --- /dev/null +++ b/debian/patches/coqdoc_stdlib.dpatch @@ -0,0 +1,72 @@ +#! /bin/sh /usr/share/dpatch/dpatch-run +## coqdoc_stdlib.dpatch by Samuel Mimram +## +## All lines beginning with `## DP:' are a description of the patch. +## DP: No description. + +@DPATCH@ +diff -urNad coq-8.0pl3+8.1alpha~/doc/Makefile coq-8.0pl3+8.1alpha/doc/Makefile +--- coq-8.0pl3+8.1alpha~/doc/Makefile 2006-04-07 15:08:12.000000000 +0000 ++++ coq-8.0pl3+8.1alpha/doc/Makefile 2006-04-28 13:43:28.000000000 +0000 +@@ -216,6 +216,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) + mv stdlib/html/index.html stdlib/index-body.html + +@@ -232,6 +233,7 @@ + stdlib/Library.coqdoc.tex: + (for dir in $(LIBDIRS) ; do \ + $(COQDOC) -q --gallina --body-only --latex --stdout \ ++ --coqlib_path $(COQTOP) \ + -R $(COQTOP)/theories Coq "$(COQTOP)/theories/$$dir/"*.v >> $@ ; done) + + stdlib/Library.dvi: $(COMMON) stdlib/Library.coqdoc.tex stdlib/Library.tex +diff -urNad coq-8.0pl3+8.1alpha~/tools/coqdoc/cdglobals.ml coq-8.0pl3+8.1alpha/tools/coqdoc/cdglobals.ml +--- coq-8.0pl3+8.1alpha~/tools/coqdoc/cdglobals.ml 2006-03-08 10:47:12.000000000 +0000 ++++ coq-8.0pl3+8.1alpha/tools/coqdoc/cdglobals.ml 2006-04-28 13:41:09.000000000 +0000 +@@ -44,6 +44,7 @@ + let title = ref "" + let externals = ref true + let coqlib = ref "http://coq.inria.fr/library/" ++let coqlib_path = ref Coq_config.coqlib + let raw_comments = ref false + + let charset = ref "iso-8859-1" +diff -urNad coq-8.0pl3+8.1alpha~/tools/coqdoc/main.ml coq-8.0pl3+8.1alpha/tools/coqdoc/main.ml +--- coq-8.0pl3+8.1alpha~/tools/coqdoc/main.ml 2006-03-28 17:34:15.000000000 +0000 ++++ coq-8.0pl3+8.1alpha/tools/coqdoc/main.ml 2006-04-28 13:41:09.000000000 +0000 +@@ -54,6 +54,8 @@ + prerr_endline " --no-externals no links to Coq standard library"; + prerr_endline " --coqlib set URL for Coq standard library"; + prerr_endline " (default is http://coq.inria.fr/library/)"; ++ prerr_endline " --coqlib_path path of the coqlibrary"; ++ prerr_endline (" (default is " ^ !Cdglobals.coqlib_path ^ ")"); + prerr_endline " -R map physical dir to Coq dir"; + prerr_endline " --latin1 set ISO-8859-1 input language"; + prerr_endline " --utf8 set UTF-8 input language"; +@@ -315,6 +317,8 @@ + Cdglobals.externals := false; parse_rec rem + | ("--coqlib" | "-coqlib") :: u :: rem -> + Cdglobals.coqlib := u; parse_rec rem ++ | ("--coqlib_path" | "-coqlib_path") :: u :: rem -> ++ Cdglobals.coqlib_path := u; parse_rec rem + | ("--coqlib" | "-coqlib") :: [] -> + usage () + | f :: rem -> +@@ -420,11 +424,11 @@ + let produce_document l = + List.iter index_module l; + (if !target_language=HTML then +- let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.css") in ++ let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.css") in + let dst = if !output_dir <> "" then Filename.concat !output_dir "coqdoc.css" else "coqdoc.css" in + copy src dst); + (if !target_language=LaTeX then +- let src = (Filename.concat Coq_config.coqlib "/tools/coqdoc/coqdoc.sty") in ++ let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in + let dst = if !output_dir <> "" then + Filename.concat !output_dir "coqdoc.sty" + else "coqdoc.sty" in diff --git a/debian/rules b/debian/rules index b4498d12..2971382b 100755 --- a/debian/rules +++ b/debian/rules @@ -10,11 +10,10 @@ export DH_OPTIONS # We want to use dpatch include /usr/share/dpatch/dpatch.make -COQPREF=$(CURDIR)/debian/tmp -ADDPREF=COQINSTALLPREFIX=$(COQPREF) +COQPREF := $(CURDIR)/debian/tmp +ADDPREF := COQINSTALLPREFIX=$(COQPREF) -CONFIGUREOPTS=--prefix /usr --mandir /usr/share/man \ - --emacslib /usr/share/emacs/site-lisp/coq --reals all +CONFIGUREOPTS := --prefix /usr --mandir /usr/share/man --emacslib /usr/share/emacs/site-lisp/coq --reals all configure: configure-stamp configure-stamp: @@ -30,7 +29,8 @@ configure-stamp: build: patch-stamp configure-stamp build-stamp build-stamp: dh_testdir - if grep -q BEST=opt config/Makefile; \ + $(MAKE) world +# if grep -q BEST=opt config/Makefile; \ then \ ($(MAKE) check \ && touch opt-stamp) \ @@ -43,6 +43,9 @@ build-stamp: else \ $(MAKE) BEST=byte HASCOQIDE=byte check; \ fi + $(MAKE) glob.dump + cp tools/coqdoc/coqdoc.sty doc/stdlib/ + $(MAKE) -C doc stdlib touch build-stamp clean: unpatch @@ -55,6 +58,8 @@ clean: unpatch rm -f bin/parser.opt rm -f tools/coqdoc/*.cm[oi] rm -f config/coq_config.ml config/Makefile test-suite/check.log + rm -f dev/ocamldebug-v7 + rm -f ide/undo.mli glob.dump dh_clean @@ -96,7 +101,8 @@ install: build cp debian/coqmktop.1 debian/coq/usr/share/man/man1/coqmktop.1 cp debian/coqtop.1 debian/coq/usr/share/man/man1/coqtop.1 - chmod -x debian/tmp/usr/lib/coq/ide/coq2.ico + cp -r doc/stdlib/html debian/coq-libs/usr/share/doc/coq-libs/ + cd debian/coq-libs/usr/share/doc/coq; ln -s ../coq-libs/html stdlib # These are installed as docs rm -f $(COQPREF)/usr/lib/coq/ide/utf8.v $(COQPREF)/usr/lib/coq/ide/FAQ -- cgit v1.2.3