From 9130ea9cbc657cd7adf02830e40a89f6de3953f3 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sun, 2 Mar 2014 00:17:29 +0100 Subject: Set officially the minimal OCaml requirement to 3.12.1 Anyway, a few syntactic features of 3.12 were already used here and there (e.g. local opening via Foo.(...), or the record shortcut { field; ... }). Hence compiling with 3.11 wasn't working anymore. Already take advantage of the following 3.12.1 features : - "module type of ..." in CArray, CList, CString ... - "ocamldep -ml-synonym" : no need anymore to hack the ocamldep output via our coqdep to localize the .ml4 modules :-) The -ml-synonym option (+ various bugfixes) is the reason for asking 3.12.1 directly and not just 3.12.0. After all, if debian stable is providing 3.12.1, then everybody has it ;-) --- INSTALL | 4 +-- INSTALL.ide | 2 +- Makefile.build | 8 +++--- configure.ml | 4 +-- dev/doc/debugging.txt | 8 ------ dev/doc/patch.ocaml-3.10.drop.rectypes | 31 ---------------------- dev/include | 3 ++- lib/cArray.ml | 30 +--------------------- lib/cArray.mli | 32 +---------------------- lib/cList.ml | 45 +------------------------------- lib/cList.mli | 47 +--------------------------------- lib/cString.ml | 36 +------------------------- lib/cString.mli | 37 +------------------------- tools/coqdoc/cpretty.mll | 9 +------ 14 files changed, 18 insertions(+), 278 deletions(-) delete mode 100644 dev/doc/patch.ocaml-3.10.drop.rectypes diff --git a/INSTALL b/INSTALL index ca8d705c5..276c57601 100644 --- a/INSTALL +++ b/INSTALL @@ -41,7 +41,7 @@ WHAT DO YOU NEED ? Should you need or prefer to compile Coq V8.4 yourself, you need: - - Objective Caml version 3.11.2 or later + - Objective Caml version 3.12.1 or later (available at http://caml.inria.fr/) - Camlp5 (version <= 4.08, or 5.* transitional) @@ -88,7 +88,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.11.2 (or later) +1- Check that you have the Objective Caml compiler version 3.12.1 (or later) installed on your computer and that "ocamlc" (or its native code version "ocamlc.opt") lie in a directory which is present in your $PATH environment variable. diff --git a/INSTALL.ide b/INSTALL.ide index b06fab1f6..2bbb4a5fc 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -23,7 +23,7 @@ On Gentoo GNU/Linux, do: Else, read the rest of this document to compile your own CoqIde. REQUIREMENT: - - OCaml >= 3.11.2 with native threads support. + - OCaml >= 3.12.1 with native threads support. - make world must succeed. - The graphical toolkit GTK+ 2.x. See http://www.gtk.org. The official supported version is at least 2.24.x. diff --git a/Makefile.build b/Makefile.build index f8895b2ed..7bfc6f953 100644 --- a/Makefile.build +++ b/Makefile.build @@ -106,7 +106,7 @@ OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) -DEPFLAGS= $(LOCALINCLUDES) +DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils define bestocaml $(if $(OPT),\ @@ -928,10 +928,10 @@ endif $(SHOW)'CAMLP4DEPS $<' $(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET) -# We now use coqdep_boot to wrap around ocamldep -modules, since it is aware -# of .ml4 files +# Since OCaml 3.12.1, we could use again ocamldep directly, thanks to +# the option -ml-synonym -OCAMLDEP_NG = $(COQDEPBOOT) -mldep $(OCAMLDEP) +OCAMLDEP_NG = $(OCAMLDEP) -slash -ml-synonym .ml4 checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES) $(SHOW)'OCAMLDEP $<' diff --git a/configure.ml b/configure.ml index 1c037269d..569e6ebd4 100644 --- a/configure.ml +++ b/configure.ml @@ -493,14 +493,14 @@ let caml_version_nums = "Is it installed properly?") let check_caml_version () = - if caml_version_nums >= [3;11;2] then + if caml_version_nums >= [3;12;1] then printf "You have OCaml %s. Good!\n" caml_version else let () = printf "Your version of OCaml is %s.\n" caml_version in if !Prefs.force_caml_version then printf "*Warning* Your version of OCaml is outdated.\n" else - die "You need OCaml 3.11.2 or later." + die "You need OCaml 3.12.1 or later." let _ = check_caml_version () diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index 2480b8edb..f0df2fc37 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -21,14 +21,6 @@ Debugging from Coq toplevel using Caml trace mechanism notations, ...), use "Set Printing All". It will affect the #trace printers too. -Note for Ocaml 3.10.x: Ocaml 3.10.x requires that modules compiled -with -rectypes are loaded in an environment with -rectypes set but -there is no way to tell the toplevel to support -rectypes. To make it -works, use "patch -p0 < dev/doc/patch.ocaml-3.10.drop.rectypes" to -hack script/coqmktop.ml, then recompile coqtop.byte. The procedure -above then works as soon as coqtop.byte is called with at least one -argument (add neutral option -byte to ensure at least one argument). - Debugging from Caml debugger ============================ diff --git a/dev/doc/patch.ocaml-3.10.drop.rectypes b/dev/doc/patch.ocaml-3.10.drop.rectypes deleted file mode 100644 index ba7a3e950..000000000 --- a/dev/doc/patch.ocaml-3.10.drop.rectypes +++ /dev/null @@ -1,31 +0,0 @@ -Index: scripts/coqmktop.ml -=================================================================== ---- scripts/coqmktop.ml (révision 12084) -+++ scripts/coqmktop.ml (copie de travail) -@@ -231,12 +231,25 @@ - end;; - - let ppf = Format.std_formatter;; -+ let set_rectypes_hack () = -+ if String.length (Sys.ocaml_version) >= 4 & -+ String.sub (Sys.ocaml_version) 0 4 = \"3.10\" -+ then -+ (* ocaml 3.10 does not have #rectypes but needs it *) -+ (* simulate a call with option -rectypes before *) -+ (* jumping to the ocaml toplevel *) -+ for i = 1 to Array.length Sys.argv - 1 do -+ Sys.argv.(i) <- \"-rectypes\" -+ done -+ else -+ () in -+ - Mltop.set_top - {Mltop.load_obj= - (fun f -> if not (Topdirs.load_file ppf f) then failwith \"error\"); - Mltop.use_file=Topdirs.dir_use ppf; - Mltop.add_dir=Topdirs.dir_directory; -- Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\n" -+ Mltop.ml_loop=(fun () -> set_rectypes_hack(); Topmain.main()) };;\n" - - (* create a temporary main file to link *) - let create_tmp_main_file modules = diff --git a/dev/include b/dev/include index 9518034df..5eea5cc03 100644 --- a/dev/include +++ b/dev/include @@ -10,8 +10,9 @@ Alternatively, you can avoid typing #use "include" after each Drop by adding the following lines in your $HOME/.ocamlinit : + #directory "+compiler-libs";; if Filename.basename Sys.argv.(0) = "coqtop.byte" - then ignore (Toploop.use_silently Format.std_formatter "include") + then ignore (Toploop.use_silently Format.std_formatter "dev/include") *) (* For OCaml 3.10.x: diff --git a/lib/cArray.ml b/lib/cArray.ml index 77fb04322..ab3a4ba51 100644 --- a/lib/cArray.ml +++ b/lib/cArray.ml @@ -6,35 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -module type S = -sig - external length : 'a array -> int = "%array_length" - external get : 'a array -> int -> 'a = "%array_safe_get" - external set : 'a array -> int -> 'a -> unit = "%array_safe_set" - external make : int -> 'a -> 'a array = "caml_make_vect" - val init : int -> (int -> 'a) -> 'a array - val make_matrix : int -> int -> 'a -> 'a array array - val create_matrix : int -> int -> 'a -> 'a array array - val append : 'a array -> 'a array -> 'a array - val concat : 'a array list -> 'a array - val sub : 'a array -> int -> int -> 'a array - val copy : 'a array -> 'a array - val fill : 'a array -> int -> int -> 'a -> unit - val blit : 'a array -> int -> 'a array -> int -> int -> unit - val to_list : 'a array -> 'a list - val of_list : 'a list -> 'a array - val iter : ('a -> unit) -> 'a array -> unit - val map : ('a -> 'b) -> 'a array -> 'b array - val iteri : (int -> 'a -> unit) -> 'a array -> unit - val mapi : (int -> 'a -> 'b) -> 'a array -> 'b array - val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a - val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a - val sort : ('a -> 'a -> int) -> 'a array -> unit - val stable_sort : ('a -> 'a -> int) -> 'a array -> unit - val fast_sort : ('a -> 'a -> int) -> 'a array -> unit - external unsafe_get : 'a array -> int -> 'a = "%array_unsafe_get" - external unsafe_set : 'a array -> int -> 'a -> unit = "%array_unsafe_set" -end +module type S = module type of Array module type ExtS = sig diff --git a/lib/cArray.mli b/lib/cArray.mli index 83036e27c..e3a3bd7f5 100644 --- a/lib/cArray.mli +++ b/lib/cArray.mli @@ -6,37 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *) - -module type S = -sig - external length : 'a array -> int = "%array_length" - external get : 'a array -> int -> 'a = "%array_safe_get" - external set : 'a array -> int -> 'a -> unit = "%array_safe_set" - external make : int -> 'a -> 'a array = "caml_make_vect" - val init : int -> (int -> 'a) -> 'a array - val make_matrix : int -> int -> 'a -> 'a array array - val create_matrix : int -> int -> 'a -> 'a array array - val append : 'a array -> 'a array -> 'a array - val concat : 'a array list -> 'a array - val sub : 'a array -> int -> int -> 'a array - val copy : 'a array -> 'a array - val fill : 'a array -> int -> int -> 'a -> unit - val blit : 'a array -> int -> 'a array -> int -> int -> unit - val to_list : 'a array -> 'a list - val of_list : 'a list -> 'a array - val iter : ('a -> unit) -> 'a array -> unit - val map : ('a -> 'b) -> 'a array -> 'b array - val iteri : (int -> 'a -> unit) -> 'a array -> unit - val mapi : (int -> 'a -> 'b) -> 'a array -> 'b array - val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b array -> 'a - val fold_right : ('b -> 'a -> 'a) -> 'b array -> 'a -> 'a - val sort : ('a -> 'a -> int) -> 'a array -> unit - val stable_sort : ('a -> 'a -> int) -> 'a array -> unit - val fast_sort : ('a -> 'a -> int) -> 'a array -> unit - external unsafe_get : 'a array -> int -> 'a = "%array_unsafe_get" - external unsafe_set : 'a array -> int -> 'a -> unit = "%array_unsafe_set" -end +module type S = module type of Array module type ExtS = sig diff --git a/lib/cList.ml b/lib/cList.ml index 1a1993cd6..385c80b62 100644 --- a/lib/cList.ml +++ b/lib/cList.ml @@ -9,50 +9,7 @@ type 'a cmp = 'a -> 'a -> int type 'a eq = 'a -> 'a -> bool -module type S = -sig - val length : 'a list -> int - val hd : 'a list -> 'a - val tl : 'a list -> 'a list - val nth : 'a list -> int -> 'a - val rev : 'a list -> 'a list - val append : 'a list -> 'a list -> 'a list - val rev_append : 'a list -> 'a list -> 'a list - val concat : 'a list list -> 'a list - val flatten : 'a list list -> 'a list - val iter : ('a -> unit) -> 'a list -> unit - val map : ('a -> 'b) -> 'a list -> 'b list - val rev_map : ('a -> 'b) -> 'a list -> 'b list - val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a - val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b - val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit - val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list - val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list - val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a - val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c - val for_all : ('a -> bool) -> 'a list -> bool - val exists : ('a -> bool) -> 'a list -> bool - val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool - val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool - val mem : 'a -> 'a list -> bool - val memq : 'a -> 'a list -> bool - val find : ('a -> bool) -> 'a list -> 'a - val filter : ('a -> bool) -> 'a list -> 'a list - val find_all : ('a -> bool) -> 'a list -> 'a list - val partition : ('a -> bool) -> 'a list -> 'a list * 'a list - val assoc : 'a -> ('a * 'b) list -> 'b - val assq : 'a -> ('a * 'b) list -> 'b - val mem_assoc : 'a -> ('a * 'b) list -> bool - val mem_assq : 'a -> ('a * 'b) list -> bool - val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list - val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list - val split : ('a * 'b) list -> 'a list * 'b list - val combine : 'a list -> 'b list -> ('a * 'b) list - val sort : ('a -> 'a -> int) -> 'a list -> 'a list - val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list - val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list - val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list -end +module type S = module type of List module type ExtS = sig diff --git a/lib/cList.mli b/lib/cList.mli index 6af32fdd0..15900260c 100644 --- a/lib/cList.mli +++ b/lib/cList.mli @@ -6,56 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *) - type 'a cmp = 'a -> 'a -> int type 'a eq = 'a -> 'a -> bool (** Module type [S] is the one from OCaml Stdlib. *) -module type S = -sig - val length : 'a list -> int - val hd : 'a list -> 'a - val tl : 'a list -> 'a list - val nth : 'a list -> int -> 'a - val rev : 'a list -> 'a list - val append : 'a list -> 'a list -> 'a list - val rev_append : 'a list -> 'a list -> 'a list - val concat : 'a list list -> 'a list - val flatten : 'a list list -> 'a list - val iter : ('a -> unit) -> 'a list -> unit - val map : ('a -> 'b) -> 'a list -> 'b list - val rev_map : ('a -> 'b) -> 'a list -> 'b list - val fold_left : ('a -> 'b -> 'a) -> 'a -> 'b list -> 'a - val fold_right : ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b - val iter2 : ('a -> 'b -> unit) -> 'a list -> 'b list -> unit - val map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list - val rev_map2 : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list - val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a - val fold_right2 : ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c - val for_all : ('a -> bool) -> 'a list -> bool - val exists : ('a -> bool) -> 'a list -> bool - val for_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool - val exists2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool - val mem : 'a -> 'a list -> bool - val memq : 'a -> 'a list -> bool - val find : ('a -> bool) -> 'a list -> 'a - val filter : ('a -> bool) -> 'a list -> 'a list - val find_all : ('a -> bool) -> 'a list -> 'a list - val partition : ('a -> bool) -> 'a list -> 'a list * 'a list - val assoc : 'a -> ('a * 'b) list -> 'b - val assq : 'a -> ('a * 'b) list -> 'b - val mem_assoc : 'a -> ('a * 'b) list -> bool - val mem_assq : 'a -> ('a * 'b) list -> bool - val remove_assoc : 'a -> ('a * 'b) list -> ('a * 'b) list - val remove_assq : 'a -> ('a * 'b) list -> ('a * 'b) list - val split : ('a * 'b) list -> 'a list * 'b list - val combine : 'a list -> 'b list -> ('a * 'b) list - val sort : ('a -> 'a -> int) -> 'a list -> 'a list - val stable_sort : ('a -> 'a -> int) -> 'a list -> 'a list - val fast_sort : ('a -> 'a -> int) -> 'a list -> 'a list - val merge : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list -end +module type S = module type of List module type ExtS = sig diff --git a/lib/cString.ml b/lib/cString.ml index 9be81bd3d..5c857077a 100644 --- a/lib/cString.ml +++ b/lib/cString.ml @@ -6,41 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** FIXME: use module type of *) -module type S = -sig - external length : string -> int = "%string_length" - external get : string -> int -> char = "%string_safe_get" - external set : string -> int -> char -> unit = "%string_safe_set" - external create : int -> string = "caml_create_string" - val make : int -> char -> string - val copy : string -> string - val sub : string -> int -> int -> string - val fill : string -> int -> int -> char -> unit - val blit : string -> int -> string -> int -> int -> unit - val concat : string -> string list -> string - val iter : (char -> unit) -> string -> unit - val escaped : string -> string - val index : string -> char -> int - val rindex : string -> char -> int - val index_from : string -> int -> char -> int - val rindex_from : string -> int -> char -> int - val contains : string -> char -> bool - val contains_from : string -> int -> char -> bool - val rcontains_from : string -> int -> char -> bool - val uppercase : string -> string - val lowercase : string -> string - val capitalize : string -> string - val uncapitalize : string -> string - type t = string - val compare: t -> t -> int - external unsafe_get : string -> int -> char = "%string_unsafe_get" - external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set" - external unsafe_blit : - string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc" - external unsafe_fill : - string -> int -> int -> char -> unit = "caml_fill_string" "noalloc" -end +module type S = module type of String module type ExtS = sig diff --git a/lib/cString.mli b/lib/cString.mli index 5f3616231..6aa10875c 100644 --- a/lib/cString.mli +++ b/lib/cString.mli @@ -6,43 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *) - (** Module type [S] is the one from OCaml Stdlib. *) -module type S = -sig - external length : string -> int = "%string_length" - external get : string -> int -> char = "%string_safe_get" - external set : string -> int -> char -> unit = "%string_safe_set" - external create : int -> string = "caml_create_string" - val make : int -> char -> string - val copy : string -> string - val sub : string -> int -> int -> string - val fill : string -> int -> int -> char -> unit - val blit : string -> int -> string -> int -> int -> unit - val concat : string -> string list -> string - val iter : (char -> unit) -> string -> unit - val escaped : string -> string - val index : string -> char -> int - val rindex : string -> char -> int - val index_from : string -> int -> char -> int - val rindex_from : string -> int -> char -> int - val contains : string -> char -> bool - val contains_from : string -> int -> char -> bool - val rcontains_from : string -> int -> char -> bool - val uppercase : string -> string - val lowercase : string -> string - val capitalize : string -> string - val uncapitalize : string -> string - type t = string - val compare: t -> t -> int - external unsafe_get : string -> int -> char = "%string_unsafe_get" - external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set" - external unsafe_blit : - string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc" - external unsafe_fill : - string -> int -> int -> char -> unit = "caml_fill_string" "noalloc" -end +module type S = module type of String module type ExtS = sig diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 2c58a05e2..d8a30ee36 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -12,13 +12,6 @@ open Printf open Lexing - (* A function that emulates Lexing.new_line (which does not exist in OCaml < 3.11.0) *) - let new_line lexbuf = - let pos = lexbuf.lex_curr_p in - lexbuf.lex_curr_p <- { pos with - pos_lnum = pos.pos_lnum + 1; - pos_bol = pos.pos_cnum } - (* A list function we need *) let rec take n ls = if n = 0 then [] else @@ -1065,7 +1058,7 @@ and body_bol = parse | _ { backtrack lexbuf; Output.indentation 0; body lexbuf } and body = parse - | nl {Tokens.flush_sublexer(); Output.line_break(); new_line lexbuf; body_bol lexbuf} + | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf} | nl+ space* "]]" space* nl { Tokens.flush_sublexer(); if not !formatted then -- cgit v1.2.3