Imported Upstream version 8.6upstream/8.6

1 files changed, 163 insertions, 204 deletions

diff --git a/configure.ml b/configure.ml
index 7ab19709..99f5ae54 100644
--- a/configure.ml
+++ b/configure.ml
@@ -11,11 +11,11 @@
 #load "str.cma"
 open Printf
 
-let coq_version = "8.5"
-let coq_macos_version = "8.5.0" (** "[...] should be a string comprised of
-three non-negative, period-separed integers [...]" *)
-let vo_magic = 8500
-let state_magic = 58500
+let coq_version = "8.6"
+let coq_macos_version = "8.6.00" (** "[...] 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";
 "coqdoc";"coq_makefile";"coq-tex";"gallina";"coqwc";"csdpcert";"coqdep"]
 
@@ -178,6 +178,19 @@ let which prog =
 let program_in_path prog =
   try let _ = which prog in true with Not_found -> false
 
+(** 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
+    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']
+
+let win_aware_quote_executable str =
+  if not (os_type_win32 || os_type_cygwin) then
+    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
+    Str.global_replace (Str.regexp "\\\\") "/" str
 
 (** * Date *)
 
@@ -236,7 +249,7 @@ module Prefs = struct
   let docdir = ref (None : string option)
   let emacslib = ref (None : string option)
   let coqdocdir = ref (None : string option)
-  let camldir = 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)
@@ -251,7 +264,6 @@ module Prefs = struct
   let debug = ref false
   let profile = ref false
   let annotate = ref false
-  let makecmd = ref "make"
   let nativecompiler = ref (not (os_type_win32 || os_type_cygwin))
   let coqwebsite = ref "http://coq.inria.fr/"
   let force_caml_version = ref false
@@ -290,8 +302,8 @@ let args_options = Arg.align [
     "<dir> Obsolete: same as -emacslib";
   "-coqdocdir", arg_string_option Prefs.coqdocdir,
     "<dir> Where to install Coqdoc style files";
-  "-camldir", arg_string_option Prefs.camldir,
-    "<dir> Specifies the path to the OCaml binaries";
+  "-ocamlfind", arg_string_option Prefs.ocamlfindcmd,
+    "<dir> Specifies the ocamlfind command to use";
   "-lablgtkdir", arg_string_option Prefs.lablgtkdir,
     "<dir> Specifies the path to the Lablgtk library";
   "-usecamlp5", Arg.Set Prefs.usecamlp5,
@@ -329,14 +341,14 @@ let args_options = Arg.align [
     " Add profiling information in the Coq executables";
   "-annotate", Arg.Set Prefs.annotate,
     " Dumps ml annotation files while compiling Coq";
-  "-makecmd", Arg.Set_string Prefs.makecmd,
-    "<command> Name of GNU Make command";
+  "-makecmd", Arg.String (fun _ -> printf "Warning: obsolete -makecmd option\n"),
+    "<command> Obsolete: name of GNU Make command";
   "-native-compiler", arg_bool Prefs.nativecompiler,
     "(yes|no) Compilation to native code for conversion and normalization";
   "-coqwebsite", Arg.Set_string Prefs.coqwebsite,
     " URL of the coq website";
   "-force-caml-version", Arg.Set Prefs.force_caml_version,
-    "Force OCaml version";
+    " Force OCaml version";
 ]
 
 let parse_args () =
@@ -352,42 +364,18 @@ let _ = parse_args ()
 (** Default OCaml binaries *)
 
 type camlexec =
- { mutable byte : string;
-   mutable opt : string;
+ { mutable find : string;
    mutable top : string;
-   mutable mklib : string;
-   mutable dep : string;
-   mutable doc : string;
-   mutable lex : string;
-   mutable yacc : string }
-
-(* TODO: autodetect .opt binaries ? *)
+   mutable lex : string; }
 
 let camlexec =
-  { byte = "ocamlc";
-    opt = "ocamlopt";
+  { find = "ocamlfind";
     top = "ocaml";
-    mklib = "ocamlmklib";
-    dep = "ocamldep";
-    doc = "ocamldoc";
-    lex = "ocamllex";
-    yacc = "ocamlyacc" }
-
-let reset_caml_byte c o = c.byte <- o
-let reset_caml_opt c o = c.opt <- o
-let reset_caml_doc c o = c.doc <- o
+    lex = "ocamllex"; }
+
 let reset_caml_lex c o = c.lex <- o
-let reset_caml_dep c o = c.dep <- o
-
-let rebase_camlexec dir c =
-  c.byte <- Filename.concat dir c.byte;
-  c.opt <- Filename.concat dir c.opt;
-  c.top <- Filename.concat dir c.top;
-  c.mklib <- Filename.concat dir c.mklib;
-  c.dep <- Filename.concat dir c.dep;
-  c.doc <- Filename.concat dir c.doc;
-  c.lex <- Filename.concat dir c.lex;
-  c.yacc <- Filename.concat dir c.yacc
+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 ""
@@ -442,23 +430,11 @@ let dll = if os_type_win32 then ".dll" else ".so"
 
 let vcs =
   let git_dir = try Sys.getenv "GIT_DIR" with Not_found -> ".git" in
-  if dir_exists git_dir then "git"
+  if Sys.file_exists git_dir then "git"
   else if Sys.file_exists ".svn/entries" then "svn"
   else if dir_exists "{arch}" then "gnuarch"
   else "none"
 
-(** * The make command *)
-
-let make =
-  try
-    let version_line, _ = run !Prefs.makecmd ["-v"] in
-    let version = List.nth (string_split ' ' version_line) 2 in
-    match string_split '.' version with
-    | major::minor::_ when (s2i major, s2i minor) >= (3,81) ->
-      printf "You have GNU Make %s. Good!\n" version
-    | _ -> failwith "bad version"
-  with _ -> die "Error: Cannot find GNU Make >= 3.81."
-
 (** * Browser command *)
 
 let browser =
@@ -471,32 +447,28 @@ let browser =
 (** * OCaml programs *)
 
 let camlbin, caml_version, camllib =
-  let camlbin, camlc = match !Prefs.camldir with
-  | Some dir ->
-    rebase_camlexec dir camlexec;
-    Filename.dirname camlexec.byte, camlexec.byte
-  | None ->
-    try let camlc = which camlexec.byte in
-        let dir = Filename.dirname camlc in
-        if not arch_win32 then rebase_camlexec dir camlexec; (* win32: TOCHECK *)
-        dir, camlc
-    with Not_found ->
-      die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.byte ^
-           "Please adjust your path or use the -camldir option of ./configure")
+  let () = match !Prefs.ocamlfindcmd with
+    | Some cmd -> reset_caml_find camlexec cmd
+    | None ->
+       try reset_caml_find camlexec (which camlexec.find)
+       with Not_found ->
+	 die (sprintf "Error: cannot find '%s' in your path!\n" camlexec.find ^
+		"Please adjust your path or use the -ocamlfind option of ./configure")
   in
-  let camlcopt = camlc ^ ".opt" in
-  let camlc =
-    if is_executable camlcopt then begin
-      reset_caml_byte camlexec (camlexec.byte ^ ".opt");
-      camlcopt
-    end
-    else if is_executable camlc then
-      camlc
-    else
-      die ("Error: cannot find the executable '"^camlc^"'.") in
-  let caml_version, _ = run camlc ["-version"] in
-  let camllib, _ = run camlc ["-where"] in
-  camlbin, caml_version, camllib
+  if not (is_executable camlexec.find)
+  then die ("Error: cannot find the executable '"^camlexec.find^"'.")
+  else
+    let caml_version, _ = run camlexec.find ["ocamlc";"-version"] in
+    let camllib, _ = run camlexec.find ["printconf";"stdlib"] in
+    let camlbin = (* TODO beurk beurk beurk *)
+      Filename.dirname (Filename.dirname camllib) / "bin/" in
+    let () =
+      if is_executable (camlbin / "ocamllex")
+      then reset_caml_lex camlexec (camlbin / "ocamllex") in
+    let () =
+      if is_executable (camlbin / "ocaml")
+      then reset_caml_top camlexec (camlbin / "ocaml") in
+    camlbin, caml_version, camllib
 
 let camlp4compat = "-loc loc"
 
@@ -515,7 +487,7 @@ let caml_version_nums =
          "Is it installed properly?")
 
 let check_caml_version () =
-  if caml_version_nums >= [3;12;1] then
+  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" ^
@@ -527,7 +499,7 @@ let check_caml_version () =
     if !Prefs.force_caml_version then
       printf "*Warning* Your version of OCaml is outdated.\n"
     else
-      die "You need OCaml 3.12.1 or later."
+      die "You need OCaml 4.01 or later."
 
 let _ = check_caml_version ()
 
@@ -544,12 +516,8 @@ let camltag = match caml_version_list with
 (* Convention: we use camldir as a prioritary location for camlpX, if given *)
 
 let which_camlpX base =
-  match !Prefs.camldir with
-  | Some dir ->
-    let file = Filename.concat dir base in
-    if is_executable file then file else which base
-  | None ->
-    which 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 *)
@@ -558,51 +526,47 @@ exception NoCamlp5
 
 let check_camlp5 testcma = match !Prefs.camlp5dir with
   | Some dir ->
-    if Sys.file_exists (dir/testcma) then dir
+    if Sys.file_exists (dir/testcma) then
+      let camlp5o =
+        try which_camlpX "camlp5o"
+        with Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" in
+      dir, camlp5o
     else
       let msg =
         sprintf "Cannot find camlp5 libraries in '%s' (%s not found)."
           dir testcma
       in die msg
   | None ->
-    let dir,_ = tryrun "camlp5" ["-where"] in
-    let dir2 =
-      if Sys.file_exists (camllib/"camlp5"/testcma) then
-        camllib/"camlp5"
-      else if Sys.file_exists (camllib/"site-lib"/"camlp5"/testcma) then
-        camllib/"site-lib"/"camlp5"
-      else ""
-    in
-    (* if the two values are different then camlp5 has been relocated
-     * and will not be able to find its own files, so we prefer the
-     * path where the files actually do exist *)
-    if dir2 = "" then
-      if dir = "" then
-        let () = printf "No Camlp5 installation found." in
-        let () = printf "Looking for Camlp4 instead...\n" in
-        raise NoCamlp5
-      else dir
-    else dir2
-
-let check_camlp5_version () =
-  try
-    let camlp5o = which_camlpX "camlp5o" in
-    let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
-    let version = List.nth (string_split ' ' version_line) 2 in
-    match string_split '.' version with
-    | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) ->
-      printf "You have Camlp5 %s. Good!\n" version; camlp5o, version
-    | _ -> failwith "bad version"
-  with
-  | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n"
-  | _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
+    try
+      let camlp5o = which_camlpX "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
+
+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
+  | 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"
+
+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 camlp5mod = "gramlib" in
-    let camlp5libdir = check_camlp5 (camlp5mod^".cma") in
-    let camlp5o, camlp5_version = check_camlp5_version () 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
@@ -615,6 +579,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"
 
@@ -646,60 +611,29 @@ let msg_no_dynlink_cmxa () =
   printf "and then run ./configure -natdynlink no\n"
 
 let check_native () =
-  if !Prefs.byteonly then raise Not_found;
-  let camloptopt = camlexec.opt ^ ".opt" in
-  if (is_executable camloptopt || program_in_path camloptopt) then
-    reset_caml_opt camlexec camloptopt
-  else if not (is_executable camlexec.opt || program_in_path camlexec.opt) then
-    (msg_no_ocamlopt (); raise Not_found);
-  if not (Sys.file_exists (fullcamlpXlibdir/camlpXmod^".cmxa")) then
-    (msg_no_camlpX_cmxa (); raise Not_found);
-  if not (Sys.file_exists (camllib/"dynlink.cmxa")) then
-    (msg_no_dynlink_cmxa (); raise Not_found);
-  let version, _ = run camlexec.opt ["-version"] in
-  if version <> caml_version then
-    printf
-      "Warning: Native and bytecode compilers do not have the same version!\n";
-  printf "You have native-code compilation. Good!\n"
+  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 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"
 
 let best_compiler =
   try check_native (); "opt" with Not_found -> "byte"
 
-let _ =
-  let camllexopt = camlexec.lex ^ ".opt" in
-  if is_executable camllexopt || program_in_path camllexopt then
-    reset_caml_lex camlexec camllexopt
-
-let _ =
-  let camldepopt = camlexec.dep ^ ".opt" in
-  if is_executable camldepopt || program_in_path camldepopt then
-    reset_caml_dep camlexec camldepopt
-
-let _ =
-  let camldocopt = camlexec.doc ^ ".opt" in
-  if is_executable camldocopt || program_in_path camldocopt then
-    reset_caml_doc camlexec camldocopt
-
 (** * Native dynlink *)
 
 let hasnatdynlink = !Prefs.natdynlink && best_compiler = "opt"
 
-(** OCaml 3.11.0 dynlink is buggy on MacOS 10.5, and possibly
-    also on 10.6.(0|1|2) for x86_64 and 10.6.x on x86_32 *)
-
-let needs_MacOS_fix () =
-  match hasnatdynlink, arch, caml_version_nums with
-  | true, "Darwin", 3::11::_ ->
-    (match string_split '.' (fst(run "uname" ["-r"])) with
-    | "9"::_ -> true
-    | "10"::("0"|"1"|"2")::_ -> true
-    | "10"::_ when Sys.word_size = 32 -> true
-    | _ -> false)
-  | _ -> false
-
 let natdynlinkflag =
-  if needs_MacOS_fix () then "os5fixme" else
-    if hasnatdynlink then "true" else "false"
+  if hasnatdynlink then "true" else "false"
 
 
 (** * OS dependent libraries *)
@@ -719,10 +653,18 @@ let operating_system, osdeplibs =
 
 (** * lablgtk2 and CoqIDE *)
 
+type source = Manual | OCamlFind | Stdlib
+
+let get_source = function
+| Manual -> "manually provided"
+| OCamlFind -> "via ocamlfind"
+| Stdlib -> "in OCaml library"
+
 (** Is some location a suitable LablGtk2 installation ? *)
 
-let check_lablgtkdir ?(fatal=false) msg dir =
+let check_lablgtkdir ?(fatal=false) src dir =
   let yell msg = if fatal then die msg else (printf "%s\n" msg; false) in
+  let msg = get_source src in
   if not (dir_exists dir) then
     yell (sprintf "No such directory '%s' (%s)." dir msg)
   else if not (Sys.file_exists (dir/"gSourceView2.cmi")) then
@@ -736,11 +678,11 @@ let check_lablgtkdir ?(fatal=false) msg dir =
 let get_lablgtkdir () =
   match !Prefs.lablgtkdir with
   | Some dir ->
-    let msg = "manually provided" in
+    let msg = Manual in
     if check_lablgtkdir ~fatal:true msg dir then dir, msg
-    else "", ""
+    else "", msg
   | None ->
-    let msg = "via ocamlfind" in
+    let msg = OCamlFind in
     let d1,_ = tryrun "ocamlfind" ["query";"lablgtk2.sourceview2"] in
     if d1 <> "" && check_lablgtkdir msg d1 then d1, msg
     else
@@ -748,10 +690,34 @@ let get_lablgtkdir () =
       let d2,_ = tryrun "ocamlfind" ["query";"lablgtk2"] in
       if d2 <> "" && d2 <> d1 && check_lablgtkdir msg d2 then d2, msg
       else
-        let msg = "in OCaml library" in
+        let msg = Stdlib in
         let d3 = camllib^"/lablgtk2" in
         if check_lablgtkdir msg d3 then d3, msg
-        else "", ""
+        else "", msg
+
+(** Detect and/or verify the Lablgtk2 version *)
+
+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")
+| OCamlFind ->
+  let v, _ = tryrun "ocamlfind" ["query"; "-format"; "%v"; "lablgtk2"] in
+  try
+    let vi = List.map s2i (numeric_prefix_list v) in
+    ([2; 16] <= vi, v)
+  with _ -> (false, v)
 
 let pr_ide = function No -> "no" | Byte -> "only bytecode" | Opt -> "native"
 
@@ -775,9 +741,9 @@ let check_coqide () =
   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 found = sprintf "LablGtk2 found (%s)" via in
-  let test = sprintf "grep -q -w convert_with_fallback %S/glib.mli" dir in
-  if Sys.command test <> 0 then set_ide No (found^" but too old");
+  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 ^ ")");
   (* 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");
@@ -830,20 +796,21 @@ let strip =
     if hasnatdynlink then "true" else "strip"
   else
     if !Prefs.profile || !Prefs.debug then "true" else begin
-    let _, all = run camlexec.byte ["-config"] in
+    let _, all = run camlexec.find ["ocamlc";"-config"] in
     let strip = String.concat "" (List.map (fun l ->
         match string_split ' ' l with
         | "ranlib:" :: cc :: _ -> (* on windows, we greb the right strip *)
              Str.replace_first (Str.regexp "ranlib") "strip" cc
         | _ -> ""
       ) all) in
-    if strip = "" then "stip" else strip
+    if strip = "" then "strip" else strip
     end
 
 (** * md5sum command *)
 
 let md5sum =
-  if arch = "Darwin" then "md5 -q" else "md5sum"
+  if List.mem arch ["Darwin"; "FreeBSD"; "OpenBSD"]
+  then "md5 -q" else "md5sum"
 
 
 (** * Documentation : do we have latex, hevea, ... *)
@@ -968,7 +935,7 @@ let print_summary () =
   pr "\n";
   pr "  Architecture                : %s\n" arch;
   if operating_system <> "" then
-    pr "  Operating system          : %s\n" operating_system;
+    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;
@@ -1025,7 +992,7 @@ let write_dbg_wrapper f =
 let _ = write_dbg_wrapper "dev/ocamldebug-coq"
 
 
-(** * Build the config/coq_config.ml file (+ link to myocamlbuild_config.ml) *)
+(** * Build the config/coq_config.ml file *)
 
 let write_configml f =
   safe_remove f;
@@ -1047,12 +1014,7 @@ let write_configml f =
   pr_o "datadir" datadir;
   pr_s "docdir" docdir;
   pr_s "ocaml" camlexec.top;
-  pr_s "ocamlc" camlexec.byte;
-  pr_s "ocamlopt" camlexec.opt;
-  pr_s "ocamlmklib" camlexec.mklib;
-  pr_s "ocamldep" camlexec.dep;
-  pr_s "ocamldoc" camlexec.doc;
-  pr_s "ocamlyacc" camlexec.yacc;
+  pr_s "ocamlfind" camlexec.find;
   pr_s "ocamllex" camlexec.lex;
   pr_s "camlbin" camlbin;
   pr_s "camllib" camllib;
@@ -1081,6 +1043,7 @@ let write_configml f =
   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 "localwwwrefman"  ("file:/" ^ docdir ^ "/html/refman");
@@ -1097,15 +1060,18 @@ let write_configml f =
   close_out o;
   Unix.chmod f 0o444
 
-let write_configml_my f f' =
-  write_configml f;
-  if os_type_win32 then
-    write_configml f'
-  else
-    (safe_remove f'; Unix.symlink f f')
+let _ = write_configml "config/coq_config.ml"
 
-let _ = write_configml_my "config/coq_config.ml" "myocamlbuild_config.ml"
+(** * Symlinks or copies for the checker *)
 
+let _ =
+  let prog, args, prf =
+    if arch = "win32" then "cp", [], ""
+    else "ln", ["-s"], "../" in
+  List.iter (fun file ->
+    ignore(run "rm" ["-f"; "checker/"^file]);
+    ignore(run ~fatal:true prog (args @ [prf^"kernel/"^file;"checker/"^file])))
+  [ "esubst.ml"; "esubst.mli"; "names.ml"; "names.mli" ]
 
 (** * Build the config/Makefile file *)
 
@@ -1136,13 +1102,8 @@ let write_makefile f =
   pr "VERSION4MACOS=%s\n\n" coq_macos_version;
   pr "# Objective-Caml compile command\n";
   pr "OCAML=%S\n" camlexec.top;
-  pr "OCAMLC=%S\n" camlexec.byte;
-  pr "OCAMLMKLIB=%S\n" camlexec.mklib;
-  pr "OCAMLOPT=%S\n" camlexec.opt;
-  pr "OCAMLDEP=%S\n" camlexec.dep;
-  pr "OCAMLDOC=%S\n" camlexec.doc;
+  pr "OCAMLFIND=%S\n" camlexec.find;
   pr "OCAMLLEX=%S\n" camlexec.lex;
-  pr "OCAMLYACC=%S\n\n" camlexec.yacc;
   pr "# The best compiler: native (=opt) or bytecode (=byte)\n";
   pr "BEST=%s\n\n" best_compiler;
   pr "# Ocaml version number\n";
@@ -1152,8 +1113,6 @@ let write_makefile f =
   pr "# Ocaml .h directory\n";
   pr "CAMLHLIB=%S\n\n" camllib;
   pr "# Caml link command and Caml make top command\n";
-  pr "CAMLLINK=%S\n" camlexec.byte;
-  pr "CAMLOPTLINK=%S\n\n" camlexec.opt;
   pr "# Caml flags\n";
   pr "CAMLFLAGS=-rectypes %s\n" coq_annotate_flag;
   pr "# User compilation flag\n";
@@ -1168,7 +1127,7 @@ let write_makefile f =
   pr "# Camlp4 : flavor, binaries, libraries ...\n";
   pr "# NB : avoid using CAMLP4LIB (conflict under Windows)\n";
   pr "CAMLP4=%s\n" camlpX;
-  pr "CAMLP4O=%S\n" camlpXo;
+  pr "CAMLP4O=%s\n" (win_aware_quote_executable camlpXo);
   pr "CAMLP4COMPAT=%s\n" camlp4compat;
   pr "MYCAMLP4LIB=%S\n\n" camlpXlibdir;
   pr "# Your architecture\n";