Skip to content

Commit

Permalink
Set officially the minimal OCaml requirement to 3.12.1
Browse files Browse the repository at this point in the history 
 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 ;-)
  • Loading branch information
@letouzey
letouzey committed Mar 2, 2014
1 parent f694544 commit 9130ea9
Show file tree
Hide file tree
Showing 14 changed files with 18 additions and 278 deletions.
4 changes: 2 additions & 2 deletions INSTALL
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ WHAT DO YOU NEED ?


Should you need or prefer to compile Coq V8.4 yourself, 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/) (available at http://caml.inria.fr/)


- Camlp5 (version <= 4.08, or 5.* transitional) - Camlp5 (version <= 4.08, or 5.* transitional)
Expand Down Expand Up @@ -88,7 +88,7 @@ QUICK INSTALLATION PROCEDURE.
INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). 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 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 "ocamlc.opt") lie in a directory which is present in your $PATH environment
variable. variable.
Expand Down
2 changes: 1 addition & 1 deletion INSTALL.ide
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ On Gentoo GNU/Linux, do:
Else, read the rest of this document to compile your own CoqIde. Else, read the rest of this document to compile your own CoqIde.


REQUIREMENT: REQUIREMENT:
- OCaml >= 3.11.2 with native threads support. - OCaml >= 3.12.1 with native threads support.
- make world must succeed. - make world must succeed.
- The graphical toolkit GTK+ 2.x. See http://www.gtk.org. - The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
The official supported version is at least 2.24.x. The official supported version is at least 2.24.x.
Expand Down
8 changes: 4 additions & 4 deletions Makefile.build
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS)


BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS) BYTEFLAGS=$(CAMLDEBUG) $(USERFLAGS)
OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS) OPTFLAGS=$(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
DEPFLAGS= $(LOCALINCLUDES) DEPFLAGS= $(LOCALINCLUDES) -I ide -I ide/utils


define bestocaml define bestocaml
$(if $(OPT),\ $(if $(OPT),\
Expand Down Expand Up @@ -928,10 +928,10 @@ endif
$(SHOW)'CAMLP4DEPS $<' $(SHOW)'CAMLP4DEPS $<'
$(HIDE)echo "$*.ml: $(if $(NO_RECOMPILE_ML4),$(ORDER_ONLY_SEP)) $(call CAMLP4DEPS,$<)" $(TOTARGET) $(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 # Since OCaml 3.12.1, we could use again ocamldep directly, thanks to
# of .ml4 files # 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) checker/%.ml.d: $(D_DEPEND_BEFORE_SRC) checker/%.ml $(D_DEPEND_AFTER_SRC) $(COQDEPBOOT) $(GENFILES)
$(SHOW)'OCAMLDEP $<' $(SHOW)'OCAMLDEP $<'
Expand Down
4 changes: 2 additions & 2 deletions configure.ml
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -493,14 +493,14 @@ let caml_version_nums =
"Is it installed properly?") "Is it installed properly?")


let check_caml_version () = 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 printf "You have OCaml %s. Good!\n" caml_version
else else
let () = printf "Your version of OCaml is %s.\n" caml_version in let () = printf "Your version of OCaml is %s.\n" caml_version in
if !Prefs.force_caml_version then if !Prefs.force_caml_version then
printf "*Warning* Your version of OCaml is outdated.\n" printf "*Warning* Your version of OCaml is outdated.\n"
else else
die "You need OCaml 3.11.2 or later." die "You need OCaml 3.12.1 or later."


let _ = check_caml_version () let _ = check_caml_version ()


Expand Down
8 changes: 0 additions & 8 deletions dev/doc/debugging.txt
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -21,14 +21,6 @@ Debugging from Coq toplevel using Caml trace mechanism
notations, ...), use "Set Printing All". It will affect the #trace notations, ...), use "Set Printing All". It will affect the #trace
printers too. 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 Debugging from Caml debugger
============================ ============================
Expand Down
31 changes: 0 additions & 31 deletions dev/doc/patch.ocaml-3.10.drop.rectypes
View file

This file was deleted.

3 changes: 2 additions & 1 deletion dev/include
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -10,8 +10,9 @@
Alternatively, you can avoid typing #use "include" after each Drop Alternatively, you can avoid typing #use "include" after each Drop
by adding the following lines in your $HOME/.ocamlinit : by adding the following lines in your $HOME/.ocamlinit :


#directory "+compiler-libs";;
if Filename.basename Sys.argv.(0) = "coqtop.byte" 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: (* For OCaml 3.10.x:
Expand Down
30 changes: 1 addition & 29 deletions lib/cArray.ml
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -6,35 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *) (* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************) (***********************************************************************)


module type S = module type S = module type of Array
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 ExtS = module type ExtS =
sig sig
Expand Down
32 changes: 1 addition & 31 deletions lib/cArray.mli
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -6,37 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *) (* * 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 = module type of Array

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 ExtS = module type ExtS =
sig sig
Expand Down
45 changes: 1 addition & 44 deletions lib/cList.ml
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -9,50 +9,7 @@
type 'a cmp = 'a -> 'a -> int type 'a cmp = 'a -> 'a -> int
type 'a eq = 'a -> 'a -> bool type 'a eq = 'a -> 'a -> bool


module type S = module type S = module type of List
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 ExtS = module type ExtS =
sig sig
Expand Down
47 changes: 1 addition & 46 deletions lib/cList.mli
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -6,56 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *) (* * 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 cmp = 'a -> 'a -> int
type 'a eq = 'a -> 'a -> bool type 'a eq = 'a -> 'a -> bool


(** Module type [S] is the one from OCaml Stdlib. *) (** Module type [S] is the one from OCaml Stdlib. *)
module type S = module type S = module type of List
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 ExtS = module type ExtS =
sig sig
Expand Down
36 changes: 1 addition & 35 deletions lib/cString.ml
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -6,41 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *) (* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************) (************************************************************************)


(** FIXME: use module type of *) module type S = module type of String
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 ExtS = module type ExtS =
sig sig
Expand Down
37 changes: 1 addition & 36 deletions lib/cString.mli
View file
Original file line number Original file line Diff line number Diff line change
Expand Up @@ -6,43 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *) (* * 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] is the one from OCaml Stdlib. *)
module type S = module type S = module type of String
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 ExtS = module type ExtS =
sig sig
Expand Down
Loading

0 comments on commit 9130ea9

Please sign in to comment.