Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 529 insertions, 343 deletions

diff --git a/configure.ml b/configure.ml
index 99f5ae54..5bbf0111 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,19 +11,21 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "8.6"
-let coq_macos_version = "8.6.00" (** "[...] should be a string comprised of
+let coq_version = "8.8.2"
+let coq_macos_version = "8.8.2" (** "[...] should be a string comprised of
 three non-negative, period-separated integers [...]" *)
-let vo_magic = 8600
-let state_magic = 58600
-let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr";
+let vo_magic = 8800
+let state_magic = 58800
+let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqworkmgr";
 "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
 
 let verbose = ref false (* for debugging this script *)
 
 (** * Utility functions *)
-
-let die msg = eprintf "%s\nConfiguration script failed!\n" msg; exit 1
+let cfprintf oc = kfprintf (fun oc -> fprintf oc "\n%!") oc
+let cprintf s = cfprintf stdout s
+let ceprintf s = cfprintf stderr s
+let die msg = ceprintf "%s\nConfiguration script failed!" msg; exit 1
 
 let s2i = int_of_string
 let i2s = string_of_int
@@ -107,7 +109,7 @@ let run ?(fatal=true) ?(err=StdErr) prog args =
       let cmd = String.concat " " (prog::args) in
       let exn = match e with Failure s -> s | _ -> Printexc.to_string e in
       let msg = sprintf "Error while running '%s' (%s)" cmd exn in
-      if fatal then die msg else (printf "W: %s\n" msg; "", [])
+      if fatal then die msg else (cprintf "W: %s" msg; "", [])
 
 let tryrun prog args = run ~fatal:false ~err:DevNull prog args
 
@@ -178,8 +180,22 @@ let which prog =
 let program_in_path prog =
   try let _ = which prog in true with Not_found -> false
 
+(** Choose a command among a list of candidates
+    (command name, mandatory arguments, arguments for this test).
+    Chooses the first one whose execution outputs a non-empty (first) line.
+    Dies with message [msg] if none is found. *)
+
+let select_command msg candidates =
+  let rec search = function
+    | [] -> die msg
+    | (p, x, y) :: tl ->
+      if fst (tryrun p (x @ y)) <> ""
+      then List.fold_left (Printf.sprintf "%s %s") p x
+      else search tl
+  in search candidates
+
 (** As per bug #4828, ocamlfind on Windows/Cygwin barfs if you pass it
-    a quoted path to camlpXo via -pp.  So we only quote camlpXo on not
+    a quoted path to camlp5o via -pp.  So we only quote camlp5o on not
     Windows, and warn on Windows if the path contains spaces *)
 let contains_suspicious_characters str =
   List.fold_left (fun b ch -> String.contains str ch || b) false [' '; '\t']
@@ -189,7 +205,7 @@ let win_aware_quote_executable str =
     sprintf "%S" str
   else
     let _ = if contains_suspicious_characters str then
-      printf "*Warning* The string %S contains suspicious characters; ocamlfind might fail\n" str in
+      cprintf "*Warning* The string %S contains suspicious characters; ocamlfind might fail" str in
     Str.global_replace (Str.regexp "\\\\") "/" str
 
 (** * Date *)
@@ -206,7 +222,7 @@ let get_date () =
   let year = 1900+now.Unix.tm_year in
   let month = months.(now.Unix.tm_mon) in
   sprintf "%s %d" month year,
-  sprintf "%s %d %d %d:%d:%d" (String.sub month 0 3) now.Unix.tm_mday year
+  sprintf "%s %d %d %d:%02d:%02d" (String.sub month 0 3) now.Unix.tm_mday year
     now.Unix.tm_hour now.Unix.tm_min now.Unix.tm_sec
 
 let short_date, full_date = get_date ()
@@ -221,6 +237,101 @@ let _ = if not (dir_exists "bin") then Unix.mkdir "bin" 0o755
 
 type ide = Opt | Byte | No
 
+type preferences = {
+  prefix : string option;
+  local : bool;
+  vmbyteflags : string option;
+  custom : bool option;
+  bindir : string option;
+  libdir : string option;
+  configdir : string option;
+  datadir : string option;
+  mandir : string option;
+  docdir : string option;
+  emacslib : string option;
+  coqdocdir : string option;
+  ocamlfindcmd : string option;
+  lablgtkdir : string option;
+  camlp5dir : string option;
+  arch : string option;
+  natdynlink : bool;
+  coqide : ide option;
+  macintegration : bool;
+  browser : string option;
+  withdoc : bool;
+  byteonly : bool;
+  flambda_flags : string list;
+  debug : bool;
+  profile : bool;
+  bin_annot : bool;
+  annot : bool;
+  bytecodecompiler : bool;
+  nativecompiler : bool;
+  coqwebsite : string;
+  force_caml_version : bool;
+  force_findlib_version : bool;
+  warn_error : bool;
+}
+
+module Profiles = struct
+
+let default = {
+  prefix = None;
+  local = false;
+  vmbyteflags = None;
+  custom = None;
+  bindir = None;
+  libdir = None;
+  configdir = None;
+  datadir = None;
+  mandir = None;
+  docdir = None;
+  emacslib = None;
+  coqdocdir = None;
+  ocamlfindcmd = None;
+  lablgtkdir = None;
+  camlp5dir = None;
+  arch = None;
+  natdynlink = true;
+  coqide = None;
+  macintegration = true;
+  browser = None;
+  withdoc = false;
+  byteonly = false;
+  flambda_flags = [];
+  debug = true;
+  profile = false;
+  bin_annot = false;
+  annot = false;
+  bytecodecompiler = true;
+  nativecompiler = not (os_type_win32 || os_type_cygwin);
+  coqwebsite = "http://coq.inria.fr/";
+  force_caml_version = false;
+  force_findlib_version = false;
+  warn_error = false;
+}
+
+let devel state = { state with
+  local = true;
+  bin_annot = true;
+  annot = true;
+  warn_error = true;
+}
+let devel_doc = "-local -annot -bin-annot -warn-error yes"
+
+let get = function
+  | "devel" -> devel
+  | s -> raise (Arg.Bad ("profile name expected instead of "^s))
+
+let doc =
+  "<profile> Sets a bunch of flags. Supported profiles:
+     devel = " ^ devel_doc
+
+end
+
+let prefs = ref Profiles.default
+
+
 let get_bool = function
   | "true" | "yes" | "y" | "all" -> true
   | "false" | "no" | "n" -> false
@@ -232,123 +343,99 @@ let get_ide = function
   | "no" -> No
   | s -> raise (Arg.Bad ("(opt|byte|no) argument expected instead of "^s))
 
-let arg_bool r = Arg.String (fun s -> r := get_bool s)
-
-let arg_string_option r = Arg.String (fun s -> r := Some s)
-
-module Prefs = struct
-  let prefix = ref (None : string option)
-  let local = ref false
-  let vmbyteflags = ref (None : string option)
-  let custom = ref (None : bool option)
-  let bindir = ref (None : string option)
-  let libdir = ref (None : string option)
-  let configdir = ref (None : string option)
-  let datadir = ref (None : string option)
-  let mandir = ref (None : string option)
-  let docdir = ref (None : string option)
-  let emacslib = ref (None : string option)
-  let coqdocdir = ref (None : string option)
-  let ocamlfindcmd = ref (None : string option)
-  let lablgtkdir = ref (None : string option)
-  let usecamlp5 = ref true
-  let camlp5dir = ref (None : string option)
-  let arch = ref (None : string option)
-  let natdynlink = ref true
-  let coqide = ref (None : ide option)
-  let macintegration = ref true
-  let browser = ref (None : string option)
-  let withdoc = ref false
-  let geoproof = ref false
-  let byteonly = ref false
-  let debug = ref false
-  let profile = ref false
-  let annotate = ref false
-  let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
-  let coqwebsite = ref "http://coq.inria.fr/"
-  let force_caml_version = ref false
-end
+let arg_bool f = Arg.String (fun s -> prefs := f !prefs (get_bool s))
+
+let arg_string f = Arg.String (fun s -> prefs := f !prefs s)
+let arg_string_option f = Arg.String (fun s -> prefs := f !prefs (Some s))
+let arg_string_list c f = Arg.String (fun s -> prefs := f !prefs (string_split c s))
+
+let arg_set f = Arg.Unit (fun () -> prefs := f !prefs true)
+let arg_clear f = Arg.Unit (fun () -> prefs := f !prefs false)
+
+let arg_set_option f = Arg.Unit (fun () -> prefs := f !prefs (Some true))
+let arg_clear_option f = Arg.Unit (fun () -> prefs := f !prefs (Some false))
+
+let arg_ide f = Arg.String (fun s -> prefs := f !prefs (Some (get_ide s)))
+
+let arg_profile = Arg.String (fun s -> prefs := Profiles.get s !prefs)
 
 (* TODO : earlier any option -foo was also available as --foo *)
 
 let args_options = Arg.align [
-  "-prefix", arg_string_option Prefs.prefix,
+  "-prefix", arg_string_option (fun p prefix -> { p with prefix }),
     "<dir> Set installation directory to <dir>";
-  "-local", Arg.Set Prefs.local,
+  "-local", arg_set (fun p local -> { p with local }),
     " Set installation directory to the current source tree";
-  "-vmbyteflags", arg_string_option Prefs.vmbyteflags,
+  "-vmbyteflags", arg_string_option (fun p vmbyteflags -> { p with vmbyteflags }),
     "<flags> Comma-separated link flags for the VM of coqtop.byte";
-  "-custom", Arg.Unit (fun () -> Prefs.custom := Some true),
+  "-custom", arg_set_option (fun p custom -> { p with custom }),
     " Build bytecode executables with -custom (not recommended)";
-  "-no-custom", Arg.Unit (fun () -> Prefs.custom := Some false),
+  "-no-custom", arg_clear_option (fun p custom -> { p with custom }),
     " Do not build with -custom on Windows and MacOS";
-  "-bindir", arg_string_option Prefs.bindir,
+  "-bindir", arg_string_option (fun p bindir -> { p with bindir }),
     "<dir> Where to install bin files";
-  "-libdir", arg_string_option Prefs.libdir,
+  "-libdir", arg_string_option (fun p libdir -> { p with libdir }),
     "<dir> Where to install lib files";
-  "-configdir", arg_string_option Prefs.configdir,
+  "-configdir", arg_string_option (fun p configdir -> { p with configdir }),
     "<dir> Where to install config files";
-  "-datadir", arg_string_option Prefs.datadir,
+  "-datadir", arg_string_option (fun p datadir -> { p with datadir }),
     "<dir> Where to install data files";
-  "-mandir", arg_string_option Prefs.mandir,
+  "-mandir", arg_string_option (fun p mandir -> { p with mandir }),
     "<dir> Where to install man files";
-  "-docdir", arg_string_option Prefs.docdir,
+  "-docdir", arg_string_option (fun p docdir -> { p with docdir }),
     "<dir> Where to install doc files";
-  "-emacslib", arg_string_option Prefs.emacslib,
+  "-emacslib", arg_string_option (fun p emacslib -> { p with emacslib }),
     "<dir> Where to install emacs files";
-  "-emacs", Arg.String (fun s ->
-      printf "Warning: obsolete -emacs option\n";
-      Prefs.emacslib := Some s),
-    "<dir> Obsolete: same as -emacslib";
-  "-coqdocdir", arg_string_option Prefs.coqdocdir,
+  "-coqdocdir", arg_string_option (fun p coqdocdir -> { p with coqdocdir }),
     "<dir> Where to install Coqdoc style files";
-  "-ocamlfind", arg_string_option Prefs.ocamlfindcmd,
+  "-ocamlfind", arg_string_option (fun p ocamlfindcmd -> { p with ocamlfindcmd }),
     "<dir> Specifies the ocamlfind command to use";
-  "-lablgtkdir", arg_string_option Prefs.lablgtkdir,
+  "-lablgtkdir", arg_string_option (fun p lablgtkdir -> { p with lablgtkdir }),
     "<dir> Specifies the path to the Lablgtk library";
-  "-usecamlp5", Arg.Set Prefs.usecamlp5,
-    " Specifies to use camlp5 instead of camlp4";
-  "-usecamlp4", Arg.Clear Prefs.usecamlp5,
-    " Specifies to use camlp4 instead of camlp5";
-  "-camlp5dir",
-    Arg.String (fun s -> Prefs.usecamlp5:=true; Prefs.camlp5dir:=Some s),
+  "-camlp5dir", arg_string_option (fun p camlp5dir -> { p with camlp5dir }),
     "<dir> Specifies where is the Camlp5 library and tells to use it";
-  "-arch", arg_string_option Prefs.arch,
+  "-flambda-opts", arg_string_list ' ' (fun p flambda_flags -> { p with flambda_flags }),
+    "<flags> Specifies additional flags to be passed to the flambda optimizing compiler";
+  "-arch", arg_string_option (fun p arch -> { p with arch }),
     "<arch> Specifies the architecture";
-  "-opt", Arg.Unit (fun () -> printf "Warning: obsolete -opt option\n"),
-    " Obsolete: native OCaml executables detected automatically";
-  "-natdynlink", arg_bool Prefs.natdynlink,
+  "-natdynlink", arg_bool (fun p natdynlink -> { p with natdynlink }),
     "(yes|no) Use dynamic loading of native code or not";
-  "-coqide", Arg.String (fun s -> Prefs.coqide := Some (get_ide s)),
-    "(opt|byte|no) Specifies whether or not to compile Coqide";
-  "-nomacintegration", Arg.Clear Prefs.macintegration,
-    " Do not try to build coqide mac integration";
-  "-browser", arg_string_option Prefs.browser,
+  "-coqide", arg_ide (fun p coqide -> { p with coqide }),
+    "(opt|byte|no) Specifies whether or not to compile CoqIDE";
+  "-nomacintegration", arg_clear (fun p macintegration -> { p with macintegration }),
+    " Do not try to build CoqIDE MacOS integration";
+  "-browser", arg_string_option (fun p browser -> { p with browser }),
     "<command> Use <command> to open URL %s";
-  "-nodoc", Arg.Clear Prefs.withdoc,
-    " Do not compile the documentation";
-  "-with-doc", arg_bool Prefs.withdoc,
+  "-with-doc", arg_bool (fun p withdoc -> { p with withdoc }),
     "(yes|no) Compile the documentation or not";
-  "-with-geoproof", arg_bool Prefs.geoproof,
-    "(yes|no) Use Geoproof binding or not";
-  "-byte-only", Arg.Set Prefs.byteonly,
-    " Compiles only bytecode version of Coq";
-  "-byteonly", Arg.Set Prefs.byteonly,
+  "-byte-only", arg_set (fun p byteonly -> { p with byteonly }),
     " Compiles only bytecode version of Coq";
-  "-debug", Arg.Set Prefs.debug,
-    " Add debugging information in the Coq executables";
-  "-profile", Arg.Set Prefs.profile,
+  "-nodebug", arg_clear (fun p debug -> { p with debug }),
+    " Do not add debugging information in the Coq executables";
+  "-profiling", arg_set (fun p profile -> { p with profile }),
     " Add profiling information in the Coq executables";
-  "-annotate", Arg.Set Prefs.annotate,
-    " Dumps ml annotation files while compiling Coq";
-  "-makecmd", Arg.String (fun _ -> printf "Warning: obsolete -makecmd option\n"),
-    "<command> Obsolete: name of GNU Make command";
-  "-native-compiler", arg_bool Prefs.nativecompiler,
+  "-annotate", Arg.Unit (fun () -> cprintf "*Warning* -annotate is deprecated. Please use -annot or -bin-annot instead."),
+    " Deprecated. Please use -annot or -bin-annot instead";
+  "-annot", arg_set (fun p annot -> { p with annot }),
+    " Dumps ml text annotation files while compiling Coq (e.g. for Tuareg)";
+  "-bin-annot", arg_set (fun p bin_annot -> { p with bin_annot }),
+    " Dumps ml binary annotation files while compiling Coq (e.g. for Merlin)";
+  "-bytecode-compiler", arg_bool (fun p bytecodecompiler -> { p with bytecodecompiler }),
+    "(yes|no) Enable Coq's bytecode reduction machine (VM)";
+  "-native-compiler", arg_bool (fun p nativecompiler -> { p with nativecompiler }),
     "(yes|no) Compilation to native code for conversion and normalization";
-  "-coqwebsite", Arg.Set_string Prefs.coqwebsite,
+  "-coqwebsite", arg_string (fun p coqwebsite -> { p with coqwebsite }),
     " URL of the coq website";
-  "-force-caml-version", Arg.Set Prefs.force_caml_version,
+  "-force-caml-version", arg_set (fun p force_caml_version -> { p with force_caml_version }),
     " Force OCaml version";
+  "-force-findlib-version", arg_set (fun p force_findlib_version -> { p with force_findlib_version }),
+    " Force findlib version";
+  "-warn-error", arg_bool (fun p warn_error -> { p with warn_error }),
+    "(yes|no) Make OCaml warnings into errors (default no)";
+  "-camldir", Arg.String (fun _ -> ()),
+    "<dir> Specifies path to 'ocaml' for running configure script";
+  "-profile", arg_profile,
+    Profiles.doc
 ]
 
 let parse_args () =
@@ -356,7 +443,7 @@ let parse_args () =
     args_options
     (fun s -> raise (Arg.Bad ("Unknown option: "^s)))
     "Available options for configure are:";
-  if !Prefs.local && !Prefs.prefix <> None then
+  if !prefs.local && !prefs.prefix <> None then
     die "Options -prefix and -local are incompatible."
 
 let _ = parse_args ()
@@ -377,12 +464,14 @@ let reset_caml_lex c o = c.lex <- o
 let reset_caml_top c o = c.top <- o
 let reset_caml_find c o = c.find <- o
 
-let coq_debug_flag = if !Prefs.debug then "-g" else ""
-let coq_profile_flag = if !Prefs.profile then "-p" else ""
-let coq_annotate_flag =
-  if !Prefs.annotate
-  then if program_in_path "ocamlmerlin" then "-bin-annot" else "-dtypes"
-  else ""
+let coq_debug_flag = if !prefs.debug then "-g" else ""
+let coq_profile_flag = if !prefs.profile then "-p" else ""
+let coq_annot_flag = if !prefs.annot then "-annot" else ""
+let coq_bin_annot_flag = if !prefs.bin_annot then "-bin-annot" else ""
+
+(* This variable can be overriden only for debug purposes, use with
+   care. *)
+let coq_safe_string = "-safe-string"
 
 let cflags = "-Wall -Wno-unused -g -O2"
 
@@ -396,8 +485,8 @@ let arch_progs =
    ("/usr/ucb/arch", []) ]
 
 let query_arch () =
-  printf "I can not automatically find the name of your architecture.\n";
-  printf "Give me a name, please [win32 for Win95, Win98 or WinNT]: %!";
+  cprintf "I can not automatically find the name of your architecture.";
+  cprintf "Give me a name, please [win32 for Win95, Win98 or WinNT]: %!";
   read_line ()
 
 let rec try_archs = function
@@ -407,7 +496,7 @@ let rec try_archs = function
   | _ :: rest -> try_archs rest
   | [] -> query_arch ()
 
-let arch = match !Prefs.arch with
+let arch = match !prefs.arch with
   | Some a -> a
   | None ->
     let arch,_ = tryrun "uname" ["-s"] in
@@ -416,11 +505,11 @@ let arch = match !Prefs.arch with
     else if arch <> "" then arch
     else try_archs arch_progs
 
-(** NB: [arch_win32] is broader than [os_type_win32], cf. cygwin *)
+(** NB: [arch_is_win32] is broader than [os_type_win32], cf. cygwin *)
 
-let arch_win32 = (arch = "win32")
+let arch_is_win32 = (arch = "win32")
 
-let exe = exe := if arch_win32 then ".exe" else ""; !exe
+let exe = exe := if arch_is_win32 then ".exe" else ""; !exe
 let dll = if os_type_win32 then ".dll" else ".so"
 
 (** * VCS
@@ -435,19 +524,35 @@ let vcs =
   else if dir_exists "{arch}" then "gnuarch"
   else "none"
 
+(** * Git Precommit Hook *)
+let _ =
+  let f = ".git/hooks/pre-commit" in
+  if vcs = "git" && dir_exists ".git/hooks" && not (Sys.file_exists f) then begin
+    cprintf "Creating pre-commit hook in %s" f;
+    let o = open_out f in
+    let pr s = fprintf o s in
+    pr "#!/bin/sh\n";
+    pr "\n";
+    pr "if [ -x dev/tools/pre-commit ]; then\n";
+    pr "    exec dev/tools/pre-commit\n";
+    pr "fi\n";
+    close_out o;
+    Unix.chmod f 0o775
+  end
+
 (** * Browser command *)
 
 let browser =
-  match !Prefs.browser with
+  match !prefs.browser with
   | Some b -> b
-  | None when arch_win32 -> "start %s"
+  | None when arch_is_win32 -> "start %s"
   | None when arch = "Darwin" -> "open %s"
   | _ -> "firefox -remote \"OpenURL(%s,new-tab)\" || firefox %s &"
 
 (** * OCaml programs *)
 
-let camlbin, caml_version, camllib =
-  let () = match !Prefs.ocamlfindcmd with
+let camlbin, caml_version, camllib, findlib_version =
+  let () = match !prefs.ocamlfindcmd with
     | Some cmd -> reset_caml_find camlexec cmd
     | None ->
        try reset_caml_find camlexec (which camlexec.find)
@@ -458,6 +563,7 @@ let camlbin, caml_version, camllib =
   if not (is_executable camlexec.find)
   then die ("Error: cannot find the executable '"^camlexec.find^"'.")
   else
+    let findlib_version, _ = run camlexec.find ["query"; "findlib"; "-format"; "%v"] in
     let caml_version, _ = run camlexec.find ["ocamlc";"-version"] in
     let camllib, _ = run camlexec.find ["printconf";"stdlib"] in
     let camlbin = (* TODO beurk beurk beurk *)
@@ -468,9 +574,9 @@ let camlbin, caml_version, camllib =
     let () =
       if is_executable (camlbin / "ocaml")
       then reset_caml_top camlexec (camlbin / "ocaml") in
-    camlbin, caml_version, camllib
+    camlbin, caml_version, camllib, findlib_version
 
-let camlp4compat = "-loc loc"
+let camlp5compat = "-loc loc"
 
 (** Caml version as a list of string, e.g. ["4";"00";"1"] *)
 
@@ -487,48 +593,104 @@ let caml_version_nums =
          "Is it installed properly?")
 
 let check_caml_version () =
-  if caml_version_nums >= [4;1;0] then
-    if caml_version_nums = [4;2;0] && not !Prefs.force_caml_version then
-      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
-      printf "You have OCaml %s. Good!\n" caml_version
+  if caml_version_nums >= [4;2;3] then
+    cprintf "You have OCaml %s. Good!" 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"
+    let () = cprintf "Your version of OCaml is %s." caml_version in
+    if !prefs.force_caml_version then
+      cprintf "*Warning* Your version of OCaml is outdated."
     else
-      die "You need OCaml 4.01 or later."
+      die "You need OCaml 4.02.3 or later."
 
 let _ = check_caml_version ()
 
-let coq_debug_flag_opt =
-  if caml_version_nums >= [3;10] then coq_debug_flag else ""
+let findlib_version_list = numeric_prefix_list findlib_version
 
-let camltag = match caml_version_list with
-  | x::y::_ -> "OCAML"^x^y
-  | _ -> assert false
+let findlib_version_nums =
+  try
+    if List.length findlib_version_list < 2 then failwith "bad version";
+    List.map s2i findlib_version_list
+  with _ ->
+    die ("I found ocamlfind but cannot read its version number!\n" ^
+         "Is it installed properly?")
 
+let check_findlib_version () =
+  if findlib_version_nums >= [1;4;1] then
+    cprintf "You have OCamlfind %s. Good!" findlib_version
+  else
+    let () = cprintf "Your version of OCamlfind is %s." findlib_version in
+    if !prefs.force_findlib_version then
+      cprintf "*Warning* Your version of OCamlfind is outdated."
+    else
+      die "You need OCamlfind 1.4.1 or later."
 
-(** * CamlpX configuration *)
+let _ = check_findlib_version ()
 
-(* Convention: we use camldir as a prioritary location for camlpX, if given *)
+let camltag = match caml_version_list with
+  | x::y::_ -> "OCAML"^x^y
+  | _ -> assert false
 
-let which_camlpX base =
+(** Explanation of disabled warnings:
+    4: fragile pattern matching: too common in the code and too annoying to avoid in general
+    9: missing fields in a record pattern: too common in the code and not worth the bother
+    27: innocuous unused variable: innocuous
+    41: ambiguous constructor or label: too common
+    42: disambiguated counstructor or label: too common
+    44: "open" shadowing already defined identifier: too common, especially when some are aliases
+    45: "open" shadowing a label or constructor: see 44
+    48: implicit elimination of optional arguments: too common
+    50: unexpected documentation comment: too common and annoying to avoid
+    56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3
+    58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
+    59: "potential assignment to a non-mutable value": See Coq's issue #8043
+*)
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59"
+let coq_warn_error =
+    if !prefs.warn_error
+    then "-warn-error +a"
+         ^ (if caml_version_nums > [4;2;3]
+            then "-56"
+            else "")
+    else ""
+
+(* Flags used to compile Coq and plugins (via coq_makefile) *)
+let caml_flags =
+  Printf.sprintf "-thread -rectypes %s %s %s %s" coq_warnings coq_annot_flag coq_bin_annot_flag coq_safe_string
+
+(* Flags used to compile Coq but _not_ plugins (via coq_makefile) *)
+let coq_caml_flags =
+  coq_warn_error
+
+(** * Camlp5 configuration *)
+
+(* Convention: we use camldir as a prioritary location for camlp5, 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_camlp5 base =
   let file = Filename.concat camlbin base in
   if is_executable file then file else which base
 
 (* TODO: camlp5dir should rather be the *binary* location, just as camldir *)
 (* TODO: remove the late attempts at finding gramlib.cma *)
 
-exception NoCamlp5
-
-let check_camlp5 testcma = match !Prefs.camlp5dir with
+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
@@ -538,52 +700,28 @@ let check_camlp5 testcma = match !Prefs.camlp5dir with
       in die msg
   | None ->
     try
-      let camlp5o = which_camlpX "camlp5o" in
+      let camlp5o = which_camlp5 "camlp5o" in
       let dir,_ = tryrun camlp5o ["-where"] in
       dir, camlp5o
     with Not_found ->
-      let () = printf "No Camlp5 installation found." in
-      let () = printf "Looking for Camlp4 instead...\n" in
-      raise NoCamlp5
+      die "No Camlp5 installation found."
 
 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
+    cprintf "You have Camlp5 %s. Good!" version; version
   | _ -> die "Error: unsupported Camlp5 (version < 6.06 or unrecognized).\n"
 
-let check_caml_version_for_camlp4 () =
-  if caml_version_nums = [4;1;0] && !Prefs.debug && not !Prefs.force_caml_version then
-    die ("Your version of OCaml is detected to be 4.01.0 which fails to compile\n" ^
-         "Coq in -debug mode with Camlp4. Remove -debug option or use a different\n" ^
-         "version of OCaml or use Camlp5, or bypass this test by using option\n" ^
-         "-force-caml-version.\n")
-
-let config_camlpX () =
-  try
-    if not !Prefs.usecamlp5 then raise NoCamlp5;
+let config_camlp5 () =
     let camlp5mod = "gramlib" in
     let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in
     let camlp5_version = check_camlp5_version camlp5o in
-    "camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version
-  with NoCamlp5 ->
-    (* We now try to use Camlp4, either by explicit choice or
-       by lack of proper Camlp5 installation *)
-    let camlp4mod = "camlp4lib" in
-    let camlp4libdir = camllib/"camlp4" in
-    if not (Sys.file_exists (camlp4libdir/camlp4mod^".cma")) then
-      die "No Camlp4 installation found.\n";
-    try
-      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"
+    camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version
 
-let camlpX, camlpXo, camlpXbindir, fullcamlpXlibdir, camlpXmod, camlpX_version = config_camlpX ()
+let camlp5o, camlp5bindir, fullcamlp5libdir,
+    camlp5mod, camlp5_version = config_camlp5 ()
 
 let shorten_camllib s =
   if starts_with s (camllib^"/") then
@@ -591,46 +729,46 @@ let shorten_camllib s =
     "+" ^ String.sub s l (String.length s - l)
   else s
 
-let camlpXlibdir = shorten_camllib fullcamlpXlibdir
+let camlp5libdir = shorten_camllib fullcamlp5libdir
 
 (** * Native compiler *)
 
 let msg_byteonly () =
-  printf "Only the bytecode version of Coq will be available.\n"
+  cprintf "Only the bytecode version of Coq will be available."
 
 let msg_no_ocamlopt () =
-  printf "Cannot find the OCaml native-code compiler.\n"; msg_byteonly ()
+  cprintf "Cannot find the OCaml native-code compiler."; msg_byteonly ()
 
-let msg_no_camlpX_cmxa () =
-  printf "Cannot find the native-code library of %s.\n" camlpX; msg_byteonly ()
+let msg_no_camlp5_cmxa () =
+  cprintf "Cannot find the native-code library of camlp5."; msg_byteonly ()
 
 let msg_no_dynlink_cmxa () =
-  printf "Cannot find native-code dynlink library.\n"; msg_byteonly ();
-  printf "For building a native-code Coq, you may try to first\n";
-  printf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)\n";
-  printf "and then run ./configure -natdynlink no\n"
+  cprintf "Cannot find native-code dynlink library."; msg_byteonly ();
+  cprintf "For building a native-code Coq, you may try to first";
+  cprintf "compile and install a dummy dynlink.cmxa (see dev/dynlink.ml)";
+  cprintf "and then run ./configure -natdynlink no"
 
 let check_native () =
-  let () = if !Prefs.byteonly then raise Not_found in
+  let () = if !prefs.byteonly then raise Not_found in
   let version, _ = tryrun camlexec.find ["opt";"-version"] in
   if version = "" then let () = msg_no_ocamlopt () in raise Not_found
-  else if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa"))
-  then let () = msg_no_camlpX_cmxa () in raise Not_found
+  else if not (Sys.file_exists (fullcamlp5libdir/camlp5mod^".cmxa"))
+  then let () = msg_no_camlp5_cmxa () in raise Not_found
   else if fst (tryrun camlexec.find ["query";"dynlink"]) = ""
   then let () = msg_no_dynlink_cmxa () in raise Not_found
   else
     let () =
       if version <> caml_version then
-	printf
-	  "Warning: Native and bytecode compilers do not have the same version!\n"
-    in printf "You have native-code compilation. Good!\n"
+        cprintf
+          "Warning: Native and bytecode compilers do not have the same version!"
+    in cprintf "You have native-code compilation. Good!"
 
 let best_compiler =
   try check_native (); "opt" with Not_found -> "byte"
 
 (** * Native dynlink *)
 
-let hasnatdynlink = !Prefs.natdynlink && best_compiler = "opt"
+let hasnatdynlink = !prefs.natdynlink && best_compiler = "opt"
 
 let natdynlinkflag =
   if hasnatdynlink then "true" else "false"
@@ -638,18 +776,32 @@ let natdynlinkflag =
 
 (** * OS dependent libraries *)
 
-let osdeplibs = "-cclib -lunix"
-
-let operating_system, osdeplibs =
+let operating_system =
   if starts_with arch "sun4" then
     let os, _ = run "uname" ["-r"] in
     if starts_with os "5" then
-      "Sun Solaris "^os, osdeplibs^" -cclib -lnsl -cclib -lsocket"
+      "Sun Solaris "^os
     else
-      "Sun OS "^os, osdeplibs
+      "Sun OS "^os
   else
-    (try Sys.getenv "OS" with Not_found -> ""), osdeplibs
+    (try Sys.getenv "OS" with Not_found -> "")
+
+(** Num library *)
+
+(* since 4.06, the Num library is no longer distributed with OCaml (replaced
+   by Zarith)
+*)
+
+let check_for_numlib () =
+  if caml_version_nums >= [4;6;0] then
+    let numlib,_ = tryrun camlexec.find ["query";"num"] in
+    match numlib with
+    | ""  ->
+       die "Num library not installed, required for OCaml 4.06 or later"
+    | _   -> cprintf "You have the Num library installed. Good!"
 
+let numlib =
+  check_for_numlib ()
 
 (** * lablgtk2 and CoqIDE *)
 
@@ -663,7 +815,7 @@ let get_source = function
 (** Is some location a suitable LablGtk2 installation ? *)
 
 let check_lablgtkdir ?(fatal=false) src dir =
-  let yell msg = if fatal then die msg else (printf "%s\n" msg; false) in
+  let yell msg = if fatal then die msg else (cprintf "%s" msg; false) in
   let msg = get_source src in
   if not (dir_exists dir) then
     yell (sprintf "No such directory '%s' (%s)." dir msg)
@@ -676,18 +828,18 @@ let check_lablgtkdir ?(fatal=false) src dir =
 (** Detect and/or verify the Lablgtk2 location *)
 
 let get_lablgtkdir () =
-  match !Prefs.lablgtkdir with
+  match !prefs.lablgtkdir with
   | Some dir ->
     let msg = Manual in
     if check_lablgtkdir ~fatal:true msg dir then dir, msg
     else "", msg
   | None ->
     let msg = OCamlFind in
-    let d1,_ = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in
+    let d1,_ = tryrun camlexec.find ["query";"lablgtk2.sourceview2"] in
     if d1 <> "" && check_lablgtkdir msg d1 then d1, msg
     else
       (* In debian wheezy, ocamlfind knows only of lablgtk2 *)
-      let d2,_ = tryrun "ocamlfind" ["query";"lablgtk2"] in
+      let d2,_ = tryrun camlexec.find ["query";"lablgtk2"] in
       if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg
       else
         let msg = Stdlib in
@@ -699,24 +851,22 @@ let get_lablgtkdir () =
 
 let check_lablgtk_version src dir = match src with
 | Manual | Stdlib ->
-  let test accu f =
-    if accu then
-      let test = sprintf "grep -q -w %s %S/glib.mli" f dir in
-      Sys.command test = 0
-    else false
-  in
-  let heuristics = [
-    "convert_with_fallback";
-    "wrap_poll_func"; (** Introduced in lablgtk 2.16 *)
-  ] in
-  let ans = List.fold_left test true heuristics in
-  if ans then printf "Warning: could not check the version of lablgtk2.\n";
-  (ans, "an unknown version")
+  cprintf "Warning: could not check the version of lablgtk2.\nMake sure your version is at least 2.18.3.";
+  (true, "an unknown version")
 | OCamlFind ->
-  let v, _ = tryrun "ocamlfind" ["query"; "-format"; "%v"; "lablgtk2"] in
+  let v, _ = tryrun camlexec.find ["query"; "-format"; "%v"; "lablgtk2"] in
   try
     let vi = List.map s2i (numeric_prefix_list v) in
-    ([2; 16] <= vi, v)
+    if vi < [2; 16; 0] then
+      (false, v)
+    else if vi < [2; 18; 3] then
+      begin
+        (* Version 2.18.3 is known to report incorrectly as 2.18.0, and Launchpad packages report as version 2.16.0 due to a misconfigured META file; see https://bugs.launchpad.net/ubuntu/+source/lablgtk2/+bug/1577236 *)
+        cprintf "Warning: Your installed lablgtk reports as %s.\n It is possible that the installed version is actually more recent\n but reports an incorrect version. If the installed version is\n actually more recent than 2.18.3, that's fine; if it is not,\n CoqIDE will compile but may be very unstable." v;
+        (true, "an unknown version")
+      end
+    else
+      (true, v)
   with _ -> (false, v)
 
 let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native"
@@ -725,11 +875,11 @@ exception Ide of ide
 
 (** If the user asks an impossible coqide, we abort the configuration *)
 
-let set_ide ide msg = match ide, !Prefs.coqide with
+let set_ide ide msg = match ide, !prefs.coqide with
   | No, Some (Byte|Opt)
   | Byte, Some Opt -> die (msg^":\n=> cannot build requested CoqIde")
   | _ ->
-    printf "%s:\n=> %s CoqIde will be built.\n" msg (pr_ide ide);
+    cprintf "%s:\n=> %s CoqIde will be built." msg (pr_ide ide);
     raise (Ide ide)
 
 let lablgtkdir = ref ""
@@ -738,15 +888,15 @@ let lablgtkdir = ref ""
     This function also sets the lablgtkdir reference in case of success. *)
 
 let check_coqide () =
-  if !Prefs.coqide = Some No then set_ide No "CoqIde manually disabled";
+  if !prefs.coqide = Some No then set_ide No "CoqIde manually disabled";
   let dir, via = get_lablgtkdir () in
   if dir = "" then set_ide No "LablGtk2 not found";
   let (ok, version) = check_lablgtk_version via dir in
   let found = sprintf "LablGtk2 found (%s, %s)" (get_source via) version in
-  if not ok then set_ide No (found^", but too old (required >= 2.16, found " ^ version ^ ")");
+  if not ok then set_ide No (found^", but too old (required >= 2.18.3, found " ^ version ^ ")");
   (* We're now sure to produce at least one kind of coqide *)
   lablgtkdir := shorten_camllib dir;
-  if !Prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
+  if !prefs.coqide = Some Byte then set_ide Byte (found^", bytecode requested");
   if best_compiler<>"opt" then set_ide Byte (found^", but no native compiler");
   if not (Sys.file_exists (dir/"gtkThread.cmx")) then
     set_ide Byte (found^", but no native LablGtk2");
@@ -769,8 +919,8 @@ let idearchdef = ref "X11"
 let coqide_flags () =
   if !lablgtkdir <> "" then lablgtkincludes := sprintf "-I %S" !lablgtkdir;
   match coqide, arch with
-    | "opt", "Darwin" when !Prefs.macintegration ->
-      let osxdir,_ = tryrun "ocamlfind" ["query";"lablgtkosx"] in
+    | "opt", "Darwin" when !prefs.macintegration ->
+      let osxdir,_ = tryrun camlexec.find ["query";"lablgtkosx"] in
       if osxdir <> "" then begin
         lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir;
         idearchflags := "lablgtkosx.cma";
@@ -795,7 +945,7 @@ let strip =
   if arch = "Darwin" then
     if hasnatdynlink then "true" else "strip"
   else
-    if !Prefs.profile || !Prefs.debug then "true" else begin
+    if !prefs.profile || !prefs.debug then "true" else begin
     let _, all = run camlexec.find ["ocamlc";"-config"] in
     let strip = String.concat "" (List.map (fun l ->
         match string_split ' ' l with
@@ -806,106 +956,113 @@ let strip =
     if strip = "" then "strip" else strip
     end
 
-(** * md5sum command *)
-
-let md5sum =
-  if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"]
-  then "md5 -q" else "md5sum"
-
 
 (** * Documentation : do we have latex, hevea, ... *)
 
+let check_sphinx_deps () =
+  ignore (run (which "python3") ["doc/tools/coqrst/checkdeps.py"])
+
 let check_doc () =
   let err s =
-    printf "%s was not found; documentation will not be available\n" s;
-    raise Not_found
+    die (sprintf "A documentation build was requested, but %s was not found." s);
   in
-  try
-    if not !Prefs.withdoc then raise Not_found;
-    if not (program_in_path "latex") then err "latex";
-    if not (program_in_path "hevea") then err "hevea";
-    if not (program_in_path "hacha") then err "hacha";
-    if not (program_in_path "fig2dev") then err "fig2dev";
-    if not (program_in_path "convert") then err "convert";
-    true
-  with Not_found -> false
-
-let withdoc = check_doc ()
+  if not (program_in_path "python3") then err "python3";
+  if not (program_in_path "sphinx-build") then err "sphinx-build";
+  check_sphinx_deps ()
 
+let _ = if !prefs.withdoc then check_doc ()
 
 (** * Installation directories : bindir, libdir, mandir, docdir, etc *)
 
 let coqtop = Sys.getcwd ()
 
-let unix = os_type_cygwin || not arch_win32
+let unix = os_type_cygwin || not arch_is_win32
+
+(** Variable name, description, ref in prefs, default dir, prefix-relative *)
 
-(** Variable name, description, ref in Prefs, default dir, prefix-relative *)
+type path_style =
+  | Absolute of string (* Should start with a "/" *)
+  | Relative of string (* Should not start with a "/" *)
 
 let install = [
-  "BINDIR", "the Coq binaries", Prefs.bindir,
-    (if unix then "/usr/local/bin" else "C:/coq/bin"),
-    "/bin";
-  "COQLIBINSTALL", "the Coq library", Prefs.libdir,
-    (if unix then "/usr/local/lib/coq" else "C:/coq/lib"),
-    (if arch_win32 then "" else "/lib/coq");
-  "CONFIGDIR", "the Coqide configuration files", Prefs.configdir,
-    (if unix then "/etc/xdg/coq" else "C:/coq/config"),
-    (if arch_win32 then "/config" else "/etc/xdg/coq");
-  "DATADIR", "the Coqide data files", Prefs.datadir,
-    (if unix then "/usr/local/share/coq" else "C:/coq/share"),
-    "/share/coq";
-  "MANDIR", "the Coq man pages", Prefs.mandir,
-    (if unix then "/usr/local/share/man" else "C:/coq/man"),
-    "/share/man";
-  "DOCDIR", "the Coq documentation", Prefs.docdir,
-    (if unix then "/usr/local/share/doc/coq" else "C:/coq/doc"),
-    "/share/doc/coq";
-  "EMACSLIB", "the Coq Emacs mode", Prefs.emacslib,
-    (if unix then "/usr/local/share/emacs/site-lisp" else "C:/coq/emacs"),
-    (if arch_win32 then "/emacs" else "/share/emacs/site-lisp");
-  "COQDOCDIR", "the Coqdoc LaTeX files", Prefs.coqdocdir,
-    (if unix then "/usr/local/share/texmf/tex/latex/misc" else "C:/coq/latex"),
-    (if arch_win32 then "/latex" else "/share/emacs/site-lisp");
+  "BINDIR", "the Coq binaries", !prefs.bindir,
+    Relative "bin", Relative "bin", Relative "bin";
+  "COQLIBINSTALL", "the Coq library", !prefs.libdir,
+    Relative "lib", Relative "lib/coq", Relative "";
+  "CONFIGDIR", "the Coqide configuration files", !prefs.configdir,
+    Relative "config", Absolute "/etc/xdg/coq", Relative "ide";
+  "DATADIR", "the Coqide data files", !prefs.datadir,
+    Relative "share", Relative "share/coq", Relative "ide";
+  "MANDIR", "the Coq man pages", !prefs.mandir,
+    Relative "man", Relative "share/man", Relative "man";
+  "DOCDIR", "the Coq documentation", !prefs.docdir,
+    Relative "doc", Relative "share/doc/coq", Relative "doc";
+  "EMACSLIB", "the Coq Emacs mode", !prefs.emacslib,
+    Relative "emacs", Relative "share/emacs/site-lisp", Relative "tools";
+  "COQDOCDIR", "the Coqdoc LaTeX files", !prefs.coqdocdir,
+    Relative "latex", Relative "share/texmf/tex/latex/misc", Relative "tools/coqdoc";
  ]
 
-let do_one_instdir (var,msg,r,dflt,suff) =
-  let dir = match !r, !Prefs.prefix with
-    | Some d, _ -> d
-    | _, Some p -> p^suff
-    | _ ->
+let strip_trailing_slash_if_any p =
+  if p.[String.length p - 1] = '/' then String.sub p 0 (String.length p - 1) else p
+
+let use_suffix prefix = function
+  | Relative "" -> prefix
+  | Relative suff -> prefix ^ "/" ^ suff
+  | Absolute path -> path
+
+let relativize = function
+  (* Turn a global layout based on some prefix to a relative layout *)
+  | Relative _ as suffix -> suffix
+  | Absolute path -> Relative (String.sub path 1 (String.length path - 1))
+
+let find_suffix prefix path = match prefix with
+  | None -> Absolute path
+  | Some p ->
+     let p = strip_trailing_slash_if_any p in
+     let lpath = String.length path in
+     let lp = String.length p in
+     if lpath > lp && String.sub path 0 lp = p then
+       Relative (String.sub path (lp+1) (lpath - lp - 1))
+     else
+       Absolute path
+
+let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout,locallayout) =
+  let dir,suffix =
+    if !prefs.local then (use_suffix coqtop locallayout,locallayout)
+    else match uservalue, !prefs.prefix with
+    | Some d, p -> d,find_suffix p d
+    | _, Some p ->
+      let suffix = if arch_is_win32 then selfcontainedlayout else relativize unixlayout in
+      use_suffix p suffix, suffix
+    | _, p ->
+      let suffix = if unix then unixlayout else selfcontainedlayout in
+      let base = if unix then "/usr/local" else "C:/coq" in
+      let dflt = use_suffix base suffix in
       let () = printf "Where should I install %s [%s]? " msg dflt in
       let line = read_line () in
-      if line = "" then dflt else line
-  in (var,msg,dir,dir<>dflt)
+      if line = "" then (dflt,suffix) else (line,find_suffix p line)
+  in (var,msg,dir,suffix)
 
-let do_one_noinst (var,msg,_,_,_) =
-  if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide",true)
-  else (var,msg,"",false)
-
-let install_dirs =
-  let f = if !Prefs.local then do_one_noinst else do_one_instdir in
-  List.map f install
+let install_dirs = List.map do_one_instdir install
 
 let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs
 
-let libdir = let (_,_,d,_) = select "COQLIBINSTALL" in d
-
-let docdir = let (_,_,d,_) = select "DOCDIR" in d
+let coqlib,coqlibsuffix = let (_,_,d,s) = select "COQLIBINSTALL" in d,s
 
-let configdir =
-  let (_,_,d,b) = select "CONFIGDIR" in if b then Some d else None
+let docdir,docdirsuffix = let (_,_,d,s) = select "DOCDIR" in d,s
 
-let datadir =
-  let (_,_,d,b) = select "DATADIR" in if b then Some d else None
+let configdir,configdirsuffix = let (_,_,d,s) = select "CONFIGDIR" in d,s
 
+let datadir,datadirsuffix = let (_,_,d,s) = select "DATADIR" in d,s
 
 (** * OCaml runtime flags *)
 
 (** Do we use -custom (yes by default on Windows and MacOS) *)
 
-let custom_os = arch_win32 || arch = "Darwin"
+let custom_os = arch_is_win32 || arch = "Darwin"
 
-let use_custom = match !Prefs.custom with
+let use_custom = match !prefs.custom with
   | Some b -> b
   | None -> custom_os
 
@@ -915,18 +1072,19 @@ let build_loadpath =
   ref "# you might want to set CAML_LD_LIBRARY_PATH by hand!"
 
 let config_runtime () =
-  match !Prefs.vmbyteflags with
+  match !prefs.vmbyteflags with
   | Some flags -> string_split ',' flags
   | _ when use_custom -> [custom_flag]
-  | _ when !Prefs.local ->
+  | _ when !prefs.local ->
     ["-dllib";"-lcoqrun";"-dllpath";coqtop/"kernel/byterun"]
   | _ ->
     let ld="CAML_LD_LIBRARY_PATH" in
     build_loadpath := sprintf "export %s:='%s/kernel/byterun':$(%s)" ld coqtop ld;
-    ["-dllib";"-lcoqrun";"-dllpath";libdir]
+    ["-dllib";"-lcoqrun";"-dllpath";coqlib/"kernel/byterun"]
 
 let vmbyteflags = config_runtime ()
 
+let esc s = if String.contains s ' ' then "\"" ^ s ^ "\"" else s
 
 (** * Summary of the configuration *)
 
@@ -938,32 +1096,32 @@ let print_summary () =
     pr "  Operating system            : %s\n" operating_system;
   pr "  Coq VM bytecode link flags  : %s\n" (String.concat " " vmbyteflags);
   pr "  Other bytecode link flags   : %s\n" custom_flag;
-  pr "  OS dependent libraries      : %s\n" osdeplibs;
   pr "  OCaml version               : %s\n" caml_version;
-  pr "  OCaml binaries in           : %s\n" camlbin;
-  pr "  OCaml library in            : %s\n" camllib;
-  pr "  %s version              : %s\n"     (String.capitalize camlpX) camlpX_version;
-  pr "  %s binaries in          : %s\n"     (String.capitalize camlpX) camlpXbindir;
-  pr "  %s library in           : %s\n"     (String.capitalize camlpX) camlpXlibdir;
+  pr "  OCaml binaries in           : %s\n" (esc camlbin);
+  pr "  OCaml library in            : %s\n" (esc camllib);
+  pr "  OCaml flambda flags         : %s\n" (String.concat " " !prefs.flambda_flags);
+  pr "  Camlp5 version              : %s\n" camlp5_version;
+  pr "  Camlp5 binaries in          : %s\n" (esc camlp5bindir);
+  pr "  Camlp5 library in           : %s\n" (esc camlp5libdir);
   if best_compiler = "opt" then
     pr "  Native dynamic link support : %B\n" hasnatdynlink;
   if coqide <> "no" then
-    pr "  Lablgtk2 library in         : %s\n" !lablgtkdir;
+    pr "  Lablgtk2 library in         : %s\n" (esc !lablgtkdir);
   if !idearchdef = "QUARTZ" then
     pr "  Mac OS integration is on\n";
   pr "  CoqIde                      : %s\n" coqide;
   pr "  Documentation               : %s\n"
-    (if withdoc then "All" else "None");
+    (if !prefs.withdoc then "All" else "None");
   pr "  Web browser                 : %s\n" browser;
-  pr "  Coq web site                : %s\n\n" !Prefs.coqwebsite;
-  if not !Prefs.nativecompiler then
-    pr "  Native compiler for conversion and normalization disabled\n\n";
-  if !Prefs.local then
+  pr "  Coq web site                : %s\n" !prefs.coqwebsite;
+  pr "  Bytecode VM enabled         : %B\n" !prefs.bytecodecompiler;
+  pr "  Native Compiler enabled     : %B\n\n" !prefs.nativecompiler;
+  if !prefs.local then
     pr "  Local build, no installation...\n"
   else
     (pr "  Paths for true installation:\n";
      List.iter
-       (fun (_,msg,dir,_) -> pr "  - %s will be copied in %s\n" msg dir)
+       (fun (_,msg,dir,_) -> pr "  - %s will be copied in %s\n" msg (esc dir))
        install_dirs);
   pr "\n";
   pr "If anything is wrong above, please restart './configure'.\n\n";
@@ -977,21 +1135,20 @@ let _ = print_summary ()
 
 let write_dbg_wrapper f =
   safe_remove f;
-  let o = open_out f in
+  let o = open_out_bin f in  (* _bin to avoid adding \r on Cygwin/Windows *)
   let pr s = fprintf o s in
   pr "#!/bin/sh\n\n";
   pr "###### ocamldebug-coq : a wrapper around ocamldebug for Coq ######\n\n";
   pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure #\n\n";
   pr "export COQTOP=%S\n" coqtop;
   pr "OCAMLDEBUG=%S\n" (camlbin^"/ocamldebug");
-  pr "CAMLP4LIB=%S\n\n" camlpXlibdir;
+  pr "CAMLP5LIB=%S\n\n" camlp5libdir;
   pr ". $COQTOP/dev/ocamldebug-coq.run\n";
   close_out o;
   Unix.chmod f 0o555
 
 let _ = write_dbg_wrapper "dev/ocamldebug-coq"
 
-
 (** * Build the config/coq_config.ml file *)
 
 let write_configml f =
@@ -1001,54 +1158,71 @@ let write_configml f =
   let pr_s = pr "let %s = %S\n" in
   let pr_b = pr "let %s = %B\n" in
   let pr_i = pr "let %s = %d\n" in
-  let pr_o s o = pr "let %s = %s\n" s
-    (match o with None -> "None" | Some d -> sprintf "Some %S" d)
-  in
+  let pr_p s o = pr "let %s = %S\n" s
+    (match o with Relative s -> s | Absolute s -> s) in
+  let pr_l  n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map (fun s -> "\"" ^ s ^ "\"") l)) in
+  let pr_li n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map string_of_int l)) in
   pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n";
   pr "(* Exact command that generated this file: *)\n";
   pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv));
-  pr_b "local" !Prefs.local;
+  pr_b "local" !prefs.local;
   pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n";
-  pr_o "coqlib" (if !Prefs.local then None else Some libdir);
-  pr_o "configdir" configdir;
-  pr_o "datadir" datadir;
+  pr_s "coqlib" coqlib;
+  pr_s "configdir" configdir;
+  pr_s "datadir" datadir;
   pr_s "docdir" docdir;
+  pr_p "coqlibsuffix" coqlibsuffix;
+  pr_p "configdirsuffix" configdirsuffix;
+  pr_p "datadirsuffix" datadirsuffix;
+  pr_p "docdirsuffix" docdirsuffix;
   pr_s "ocaml" camlexec.top;
   pr_s "ocamlfind" camlexec.find;
   pr_s "ocamllex" camlexec.lex;
   pr_s "camlbin" camlbin;
   pr_s "camllib" camllib;
-  pr_s "camlp4" camlpX;
-  pr_s "camlp4o" camlpXo;
-  pr_s "camlp4bin" camlpXbindir;
-  pr_s "camlp4lib" camlpXlibdir;
-  pr_s "camlp4compat" camlp4compat;
+  pr_s "camlp5o" camlp5o;
+  pr_s "camlp5bin" camlp5bindir;
+  pr_s "camlp5lib" camlp5libdir;
+  pr_s "camlp5compat" camlp5compat;
   pr_s "cflags" cflags;
+  pr_s "caml_flags" caml_flags;
   pr_s "best" best_compiler;
-  pr_s "osdeplibs" osdeplibs;
   pr_s "version" coq_version;
   pr_s "caml_version" caml_version;
+  pr_li "caml_version_nums" caml_version_nums;
   pr_s "date" short_date;
   pr_s "compile_date" full_date;
   pr_s "arch" arch;
-  pr_b "arch_is_win32" arch_win32;
+  pr_b "arch_is_win32" arch_is_win32;
   pr_s "exec_extension" exe;
   pr_s "coqideincl" !lablgtkincludes;
   pr_s "has_coqide" coqide;
   pr "let gtk_platform = `%s\n" !idearchdef;
   pr_b "has_natdynlink" hasnatdynlink;
   pr_s "natdynlinkflag" natdynlinkflag;
+  pr_l "flambda_flags" !prefs.flambda_flags;
   pr_i "vo_magic_number" vo_magic;
   pr_i "state_magic_number" state_magic;
-  pr "let with_geoproof = ref %B\n" !Prefs.geoproof;
   pr_s "browser" browser;
-  pr_s "wwwcoq" !Prefs.coqwebsite;
-  pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/");
-  pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/");
-  pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/");
+  pr_s "wwwcoq" !prefs.coqwebsite;
+  pr_s "wwwbugtracker" (!prefs.coqwebsite ^ "bugs/");
+  pr_s "wwwrefman" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/refman/");
+  pr_s "wwwstdlib" (!prefs.coqwebsite ^ "distrib/V" ^ coq_version ^ "/stdlib/");
   pr_s "localwwwrefman"  ("file:/" ^ docdir ^ "/html/refman");
-  pr_b "no_native_compiler" (not !Prefs.nativecompiler);
+  pr_b "bytecode_compiler" !prefs.bytecodecompiler;
+  pr_b "native_compiler" !prefs.nativecompiler;
+
+  let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library";
+                        "engine"; "pretyping"; "interp"; "parsing"; "proofs";
+                        "tactics"; "toplevel"; "printing"; "intf";
+                        "grammar"; "ide"; "stm"; "vernac" ] in
+  let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ "  \"" ^ core_src_subdir ^ "\";\n")
+                                    ""
+                                    core_src_dirs in
+
+  pr "\nlet core_src_dirs = [\n%s]\n" core_src_dirs;
   pr "\nlet plugins_dirs = [\n";
+
   let plugins = Sys.readdir "plugins" in
   Array.sort compare plugins;
   Array.iter
@@ -1057,6 +1231,9 @@ let write_configml f =
       if Sys.is_directory f' && f.[0] <> '.' then pr "  %S;\n" f')
     plugins;
   pr "]\n";
+
+  pr "\nlet all_src_dirs = core_src_dirs @ plugins_dirs\n";
+
   close_out o;
   Unix.chmod f 0o444
 
@@ -1090,9 +1267,10 @@ let write_makefile f =
   pr "#Variable used to detect whether ./configure has run successfully.\n";
   pr "COQ_CONFIGURED=yes\n\n";
   pr "# Local use (no installation)\n";
-  pr "LOCAL=%B\n\n" !Prefs.local;
+  pr "LOCAL=%B\n\n" !prefs.local;
   pr "# Bytecode link flags : should we use -custom or not ?\n";
   pr "CUSTOM=%s\n" custom_flag;
+  pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags);
   pr "%s\n\n" !build_loadpath;
   pr "# Paths for true installation\n";
   List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
@@ -1114,22 +1292,23 @@ let write_makefile f =
   pr "CAMLHLIB=%S\n\n" camllib;
   pr "# Caml link command and Caml make top command\n";
   pr "# Caml flags\n";
-  pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag;
+  pr "CAMLFLAGS=%s %s\n" caml_flags coq_caml_flags;
   pr "# User compilation flag\n";
   pr "USERFLAGS=\n\n";
+  (* XXX make this configurable *)
+  pr "FLAMBDA_FLAGS=%s\n" (String.concat " " !prefs.flambda_flags);
   pr "# Flags for GCC\n";
   pr "CFLAGS=%s\n\n" cflags;
   pr "# Compilation debug flags\n";
   pr "CAMLDEBUG=%s\n" coq_debug_flag;
-  pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag_opt;
+  pr "CAMLDEBUGOPT=%s\n\n" coq_debug_flag;
   pr "# Compilation profile flag\n";
   pr "CAMLTIMEPROF=%s\n\n" coq_profile_flag;
-  pr "# Camlp4 : flavor, binaries, libraries ...\n";
-  pr "# NB : avoid using CAMLP4LIB (conflict under Windows)\n";
-  pr "CAMLP4=%s\n" camlpX;
-  pr "CAMLP4O=%s\n" (win_aware_quote_executable camlpXo);
-  pr "CAMLP4COMPAT=%s\n" camlp4compat;
-  pr "MYCAMLP4LIB=%S\n\n" camlpXlibdir;
+  pr "# Camlp5 : flavor, binaries, libraries ...\n";
+  pr "# NB : avoid using CAMLP5LIB (conflict under Windows)\n";
+  pr "CAMLP5O=%s\n" (win_aware_quote_executable camlp5o);
+  pr "CAMLP5COMPAT=%s\n" camlp5compat;
+  pr "MYCAMLP5LIB=%S\n\n" camlp5libdir;
   pr "# Your architecture\n";
   pr "# Can be obtain by UNIX command arch\n";
   pr "ARCH=%s\n" arch;
@@ -1137,7 +1316,6 @@ let write_makefile f =
   pr "# Supplementary libs for some systems, currently:\n";
   pr "#  . Sun Solaris: -cclib -lunix -cclib -lnsl -cclib -lsocket\n";
   pr "#  . others     : -cclib -lunix\n";
-  pr "OSDEPLIBS=%s\n\n" osdeplibs;
   pr "# executable files extension, currently:\n";
   pr "#  Unix systems:\n";
   pr "#  Win32 systems : .exe\n";
@@ -1149,8 +1327,6 @@ let write_makefile f =
   pr "# Unix systems and profiling: true\n";
   pr "# Unix systems and no profiling: strip\n";
   pr "STRIP=%s\n\n" strip;
-  pr "#the command md5sum\n";
-  pr "MD5SUM=%s\n\n" md5sum;
   pr "# LablGTK\n";
   pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes;
   pr "# CoqIde (no/byte/opt)\n";
@@ -1163,9 +1339,9 @@ let write_makefile f =
   pr "# Defining REVISION\n";
   pr "CHECKEDOUT=%s\n\n" vcs;
   pr "# Option to control compilation and installation of the documentation\n";
-  pr "WITHDOC=%s\n\n" (if withdoc then "all" else "no");
+  pr "WITHDOC=%s\n\n" (if !prefs.withdoc then "all" else "no");
   pr "# Option to produce precompiled files for native_compute\n";
-  pr "NATIVECOMPUTE=%s\n" (if !Prefs.nativecompiler then "-native-compiler" else "");
+  pr "NATIVECOMPUTE=%s\n" (if !prefs.nativecompiler then "-native-compiler" else "");
   close_out o;
   Unix.chmod f 0o444
 
@@ -1197,3 +1373,13 @@ let write_macos_metadata exec =
 
 let () = if arch = "Darwin" then
 List.iter write_macos_metadata distributed_exec
+
+let write_configpy f =
+  safe_remove f;
+  let o = open_out f in
+  let pr s = fprintf o s in
+  let pr_s = pr "%s = '%s'\n" in
+  pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure\n";
+  pr_s "version" coq_version
+
+let _ = write_configpy "config/coq_config.py"