From 50266aab0b9d9ba3bede37429bcdc5c2bfdc1159 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 17 Apr 2016 21:55:18 +0200 Subject: Updating configure.ml wrt Coq not compilable with OCaml 4.01.0 in debug mode. --- configure.ml | 3 +++ 1 file changed, 3 insertions(+) (limited to 'configure.ml') diff --git a/configure.ml b/configure.ml index 48bcf34e1..6291de03c 100644 --- a/configure.ml +++ b/configure.ml @@ -520,6 +520,9 @@ let check_caml_version () = die ("Your version of OCaml is 4.02.0 which suffers from a bug inducing\n" ^ "very slow compilation times. If you still want to use it, use \n" ^ "option -force-caml-version.\n") + else if caml_version_nums = [4;1;0] && !Prefs.debug then + die ("Your version of OCaml is 4.01.0 which fails to compile Coq in " ^ + "-debug mode.\nRemove -debug option or use a different version of OCaml.\n") else printf "You have OCaml %s. Good!\n" caml_version else -- cgit v1.2.3 From b038ff00e3d1873bed580c13df1b18ce0510abb2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 19 Apr 2016 09:37:55 +0200 Subject: Fixing 50266aab on incompatibility of OCaml 4.01.0 with option -debug. This was only when compiling with Camlp4 and it was producing an assertion failure in asmcomp/emitaux.ml at line 226, reported as OCaml's bug #6243. Note: The issue of a problematic compilation with 4.01.0 was raised at last WG. --- configure.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) (limited to 'configure.ml') diff --git a/configure.ml b/configure.ml index 6291de03c..83005f0c5 100644 --- a/configure.ml +++ b/configure.ml @@ -520,9 +520,6 @@ let check_caml_version () = die ("Your version of OCaml is 4.02.0 which suffers from a bug inducing\n" ^ "very slow compilation times. If you still want to use it, use \n" ^ "option -force-caml-version.\n") - else if caml_version_nums = [4;1;0] && !Prefs.debug then - die ("Your version of OCaml is 4.01.0 which fails to compile Coq in " ^ - "-debug mode.\nRemove -debug option or use a different version of OCaml.\n") else printf "You have OCaml %s. Good!\n" caml_version else @@ -600,6 +597,12 @@ let check_camlp5_version () = | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n" +let check_caml_version_for_camlp4 () = + if caml_version_nums = [4;1;0] && !Prefs.debug then + die ("Your version of OCaml is 4.01.0 which fails to compile Coq in -debug\n" ^ + "mode with Camlp4. Remove -debug option or use a different version of OCaml\n" ^ + "or use Camlp5.\n") + let config_camlpX () = try if not !Prefs.usecamlp5 then raise NoCamlp5; @@ -618,6 +621,7 @@ let config_camlpX () = let camlp4orf = which_camlpX "camlp4orf" in let version_line, _ = run ~err:StdOut camlp4orf ["-v"] in let camlp4_version = List.nth (string_split ' ' version_line) 2 in + check_caml_version_for_camlp4 (); "camlp4", camlp4orf, Filename.dirname camlp4orf, camlp4libdir, camlp4mod, camlp4_version with _ -> die "No Camlp4 installation found.\n" -- cgit v1.2.3