Merge branch 'v8.6'

1 files changed, 19 insertions, 5 deletions

diff --git a/configure.ml b/configure.ml
index f75bbb538..48e167c99 100644
--- a/configure.ml
+++ b/configure.ml
@@ -12,10 +12,10 @@
 open Printf
 
 let coq_version = "trunk"
-let coq_macos_version = "8.4.90" (** "[...] should be a string comprised of
+let coq_macos_version = "8.6.90" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
-let vo_magic = 8591
-let state_magic = 58591
+let vo_magic = 8691
+let state_magic = 58691
 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
 "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
 
@@ -509,6 +509,20 @@ let camltag = match caml_version_list with
 (** * CamlpX configuration *)
 
 (* Convention: we use camldir as a prioritary location for camlpX, if given *)
+(* i.e., in the case of camlp5, we search for a copy of camlp5o which *)
+(* answers the right camlp5 lib dir *)
+
+let strip_slash dir =
+  let n = String.length dir in
+  if n>0 && dir.[n - 1] = '/' then String.sub dir 0 (n-1) else dir
+
+let which_camlp5o_for camlp5lib =
+  let camlp5o = Filename.concat camlbin "camlp5o" in
+  let camlp5lib = strip_slash camlp5lib in
+  if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else
+  let camlp5o = which "camlp5o" in
+  if fst (tryrun camlp5o ["-where"]) = camlp5lib then camlp5o else
+  die ("Error: cannot find Camlp5 binaries corresponding to Camlp5 library " ^ camlp5lib)
 
 let which_camlpX base =
   let file = Filename.concat camlbin base in
@@ -523,7 +537,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
   | Some dir ->
     if Sys.file_exists (dir/testcma) then
       let camlp5o =
-        try which_camlpX "camlp5o"
+        try which_camlp5o_for dir
         with Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" in
       dir, camlp5o
     else
@@ -544,7 +558,7 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
 let check_camlp5_version camlp5o =
   let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
   let version = List.nth (string_split ' ' version_line) 2 in
-  match string_split '.' version with
+  match numeric_prefix_list version with
   | major::minor::_ when s2i major > 6 || (s2i major, s2i minor) >= (6,6) ->
     printf "You have Camlp5 %s. Good!\n" version; version
   | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n"