diff options
| -rw-r--r-- | INSTALL | 8 | ||||
| -rw-r--r-- | INSTALL.ide | 2 | ||||
| -rw-r--r-- | README.win | 2 | ||||
| -rwxr-xr-x | configure | 21 | ||||
| -rw-r--r-- | kernel/byterun/coq_interp.c | 19 | ||||
| -rw-r--r-- | lib/compat.ml4 | 50 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 9 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 13 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 8 |
9 files changed, 25 insertions, 107 deletions
@@ -41,12 +41,10 @@ WHAT DO YOU NEED ? Should you need or prefer to compile Coq V8.2 yourself, you need: - - Objective Caml version 3.09.3 or later + - Objective Caml version 3.10.0 or later (available at http://caml.inria.fr/) - For Ocaml version >= 3.10.0, you also need to install camlp5 - (version <= 4.08, or 5.01 transitional) - + - Camlp5 (version <= 4.08, or 5.* transitional) - GNU Make version 3.81 or later ( @@ -89,7 +87,7 @@ QUICK INSTALLATION PROCEDURE. INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS). ================================================= -1- Check that you have the Objective Caml compiler version 3.09.3 (or later) +1- Check that you have the Objective Caml compiler version 3.10.0 (or later) installed on your computer and that "ocamlmktop" and "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 757d83548..d09df2eb0 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.09.3 with native threads support. + - OCaml >= 3.10 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.8.x. diff --git a/README.win b/README.win index 7e0d21105..9f6eff799 100644 --- a/README.win +++ b/README.win @@ -20,7 +20,7 @@ COMPILATION. distribution. If you really need to recompile under Windows, here are some indications: - 1- Install ocaml for Windows (MinGW port), preferably version 3.09.3. + 1- Install ocaml for Windows (MinGW port). See: http://caml.inria.fr 2- Install a shell environment with at least: @@ -420,16 +420,16 @@ esac CAMLVERSION=`"$bytecamlc" -version` case $CAMLVERSION in - 1.*|2.*|3.00|3.01|3.02|3.03|3.03alpha|3.04|3.05beta|3.05|3.06|3.07*|3.08*|3.09.[012]) + 1.*|2.*|3.0*) echo "Your version of Objective-Caml is $CAMLVERSION." if [ "$force_caml_version" = "yes" ]; then echo "*Warning* You are compiling Coq with an outdated version of Objective-Caml." else - echo " You need Objective-Caml 3.09.3 or later." + echo " You need Objective-Caml 3.10.0 or later." echo " Configuration script failed!" exit 1 fi;; - ?*) + 3.1*) CAMLP4COMPAT="-loc loc" echo "You have Objective-Caml $CAMLVERSION. Good!";; *) @@ -450,12 +450,6 @@ case $ARCH in CAMLLIB=`"$CAMLC" -where` esac -# We need to set a special flag for OCaml 3.07 -case $CAMLVERSION in - 3.07*) - cflags="$cflags -DOCAML_307";; -esac - if [ "$coq_debug_flag" = "-g" ]; then case $CAMLTAG in OCAML31*) @@ -547,14 +541,7 @@ CAMLP4BIN=${CAMLBIN} if [ "$best_compiler" = "opt" ] ; then if test -e "$nativecamlc" || test -e "`which $nativecamlc`"; then CAMLOPTVERSION=`"$nativecamlc" -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' ` - if [ "`uname -s`" = "Darwin" -a "$ARCH" = "i386" ]; then - case $CAMLOPTVERSION in - 3.09.3|3.1?*) ;; - *) echo "Native compilation on MacOS X Pentium requires Objective-Caml >= 3.09.3," - best_compiler=byte - echo "only the bytecode version of Coq will be available." - esac - elif [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then + if [ ! -f $FULLCAMLP4LIB/gramlib.cmxa ]; then best_compiler=byte echo "Cannot find native-code $CAMLP4," echo "only the bytecode version of Coq will be available." diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 98ef27911..a45183f30 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -80,13 +80,6 @@ sp is a local copy of the global variable extern_sp. */ # define print_int(i) #endif -/* Wrapper pour caml_modify */ -#ifdef OCAML_307 -#define CAML_MODIFY(a,b) modify(a,b) -#else -#define CAML_MODIFY(a,b) caml_modify(a,b) -#endif - /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } @@ -659,7 +652,7 @@ value coq_interprete Field(accu, 0) = sp[0]; *sp = accu; /* mise a jour du block accumulate */ - CAML_MODIFY(&Field(p[i], 1),*sp); + caml_modify(&Field(p[i], 1),*sp); sp++; } pc += nfunc; @@ -830,7 +823,7 @@ value coq_interprete Instruct(SETFIELD0){ print_instr("SETFIELD0"); - CAML_MODIFY(&Field(accu, 0),*sp); + caml_modify(&Field(accu, 0),*sp); sp++; Next; } @@ -838,7 +831,7 @@ value coq_interprete Instruct(SETFIELD1){ int i, j, size, size_aux; print_instr("SETFIELD1"); - CAML_MODIFY(&Field(accu, 1),*sp); + caml_modify(&Field(accu, 1),*sp); sp++; Next; } @@ -856,9 +849,9 @@ value coq_interprete *sp = accu; Alloc_small(accu, 1, ATOM_COFIX_TAG); Field(accu, 0) = Field(Field(*sp, 1), 0); - CAML_MODIFY(&Field(*sp, 1), accu); + caml_modify(&Field(*sp, 1), accu); accu = *sp; sp++; - CAML_MODIFY(&Field(*sp, i), accu); + caml_modify(&Field(*sp, i), accu); } } sp++; @@ -867,7 +860,7 @@ value coq_interprete Instruct(SETFIELD){ print_instr("SETFIELD"); - CAML_MODIFY(&Field(accu, *pc),*sp); + caml_modify(&Field(accu, *pc),*sp); sp++; pc++; Next; } diff --git a/lib/compat.ml4 b/lib/compat.ml4 index 7566624b8..4ec4d915c 100644 --- a/lib/compat.ml4 +++ b/lib/compat.ml4 @@ -10,10 +10,8 @@ (* Compatibility file depending on ocaml version *) -IFDEF OCAML309 THEN DEFINE OCAML308 END - IFDEF CAMLP5 THEN -module M = struct + type loc = Stdpp.location let dummy_loc = Stdpp.dummy_loc let make_loc = Stdpp.make_loc @@ -23,45 +21,9 @@ let join_loc loc1 loc2 = else Stdpp.encl_loc loc1 loc2 type token = string*string type lexer = token Token.glexer -end -ELSE IFDEF OCAML308 THEN -module M = struct -type loc = Token.flocation -let dummy_loc = Token.dummy_loc -let make_loc loc = Token.make_loc loc -let unloc (b,e) = - let loc = (b.Lexing.pos_cnum,e.Lexing.pos_cnum) in - (* Ensure that we unpack a char location that was encoded as a line-col - location by make_loc *) -(* Gram.Entry.parse may send bad loc in 3.08, see caml-bugs #2954 - assert (dummy_loc = (b,e) or make_loc loc = (b,e)); -*) - loc -let join_loc loc1 loc2 = - if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc - else (fst loc1, snd loc2) -type token = Token.t -type lexer = Token.lexer -end -ELSE -module M = struct -type loc = int * int -let dummy_loc = (0,0) -let make_loc x = x -let unloc x = x -let join_loc loc1 loc2 = - if loc1 = dummy_loc or loc2 = dummy_loc then dummy_loc - else (fst loc1, snd loc2) -type token = Token.t -type lexer = Token.lexer -end -END -END -type loc = M.loc -let dummy_loc = M.dummy_loc -let make_loc = M.make_loc -let unloc = M.unloc -let join_loc = M.join_loc -type token = M.token -type lexer = M.lexer +ELSE (* official camlp4 of ocaml >= 3.10 *) + +TODO + +END diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index e11cdd96f..087bfc5b7 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -32,14 +32,9 @@ module L = module G = Grammar.GMake(L) -ELSE +ELSE (* official camlp4 of ocaml >= 3.10 *) -module L = - struct - let lexer = Lexer.lexer - end - -module G = Grammar.Make(L) +TODO END diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 89a1c2ed5..914b6b8f6 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -19,19 +19,8 @@ let purge_str s = if String.length s == 0 || s.[0] <> '$' then s else String.sub s 1 (String.length s - 1) -IFDEF OCAML308 THEN DEFINE NOP END -IFDEF OCAML309 THEN DEFINE NOP END -IFDEF CAMLP5 THEN DEFINE NOP END - let anti loc x = - let e = - let loc = - IFDEF NOP THEN - loc - ELSE - (1, snd loc - fst loc) - END - in <:expr< $lid:purge_str x$ >> + let e = <:expr< $lid:purge_str x$ >> in <:expr< $anti:e$ >> diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 20cb01b16..0c15950ed 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -34,16 +34,10 @@ let rec iter_name i j base sep = if i >= j then base^(string_of_int i) else (iter_name i (j-1) base sep)^sep^" "^base^(string_of_int j) -(* NB: in ocaml >= 3.10, we could use Printf.ifprintf for printing to - /dev/null, but for being compatible with earlier ocaml and not - relying on system-dependent stuff like open_out "/dev/null", - let's use instead a magical hack *) - (* Standard printer, with a final newline *) let pr s = Printf.printf (s^^"\n") (* Printing to /dev/null *) -let pn = (fun s -> Obj.magic (fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ -> ()) - : ('a, out_channel, unit) format -> 'a) +let pn s = Printf.ifprintf stdout s (* Proof printer : prints iff gen_proof is true *) let pp = if gen_proof then pr else pn (* Printer for admitted parts : prints iff gen_proof is false *) |