Coqmktop without Sys.command, changes in ./configure -*byteflags options

NB: Please re-run ./configure after pulling this commit

 For launching ocamlc/ocamlopt, coqmktop doesn't use Sys.command anymore,
 but rather CUnix.sys_command, which is based on Unix.create_process.
 This way, we do not need to bother with the underlying shell
 (/bin/sh or cmd.exe) and the way arguments are to be quoted :-).
 Btw, many cleanups of coqmktop.

 Only difficulty: the -coqrunbyteflags of ./configure is a "meta-option"
 that collect as a string several sub-options to be given by coqmktop to ocamlc.
 For instance ./configure -coqrunbyteflags "-dllib -lcoqrun". We need now to
 parse all these sub-options. To ease that, I've made the following changes
 to the ./configure options:

 * The -coqrunbyteflags and its blank-separated argument isn't accepted
   anymore, and is replaced by a new option -vmbyteflags which expects
   a comma-separated argument. For instance:

   ./configure -vmbyteflags "-dllib,-lcoqrun"

   Btw, on this example, the double-quotes aren't mandatory anymore :-)

 * The -coqtoolsbyteflags isn't accepted anymore. To the best of my
   knowledge, nobody ever used it directly (it was internally triggered
   as a byproduct of the -custom option). The only interest I can think of
   for this option was to cancel the default use of ocamlc custom-linking
   on Win32 and MacOS. For that, ./configure now provides a -no-custom option.

7 files changed, 227 insertions, 215 deletions

diff --git a/CHANGES b/CHANGES
index 6ad0f74be..5a63df21f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -105,6 +105,10 @@ Internal Infrastructure
   an executable compiled with the best OCaml compiler available.
   The bytecode program coqtop.byte is still produced. Same for other
   utilities.
+- Some options of the ./configure script slightly changed:
+  * The -coqrunbyteflags and its blank-separated argument is replaced
+    by option -vmbyteflags which expects a comma-separated argument.
+  * The -coqtoolsbyteflags option is discontinued, see -no-custom instead.
  
 Changes from V8.4beta2 to V8.4
 ==============================
diff --git a/INSTALL b/INSTALL
index a868f8fc8..ca8d705c5 100644
--- a/INSTALL
+++ b/INSTALL
@@ -315,7 +315,7 @@ DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
        the directory of the standard library of OCaml;
      - recompile your bytecode executables after reconfiguring the location of
        of the shared library:
-         ./configure -coqrunbyteflags "-dllib -lcoqrun -dllpath <path>" ...
+         ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
        where <path> is the directory where the dllcoqrun.so is installed;
      - (not recommended) compile bytecode executables with a custom OCaml
        runtime by using:
diff --git a/Makefile.build b/Makefile.build
index 2a78a9494..d98dc30f5 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -113,7 +113,7 @@ DEPFLAGS= $(LOCALINCLUDES)
 define bestocaml
 $(if $(OPT),\
 $(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -o $@ $(1) $(addsuffix .cmxa,$(2)) $^ && $(STRIP) $@,\
-$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(COQTOOLSBYTEFLAGS) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
+$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(CUSTOM) -o $@ $(1) $(addsuffix .cma,$(2)) $^)
 endef
 
 CAMLP4DEPS=$(shell LC_ALL=C sed -n -e 's@^(\*.*camlp4deps: "\(.*\)".*@\1@p' $(1) \#))
@@ -247,7 +247,7 @@ endif
 
 $(CHICKENBYTE): checker/check.cma checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) -thread $(COQTOOLSBYTEFLAGS) -o $@ $(SYSCMA) $^
+	$(HIDE)$(OCAMLC) $(CHKLIBS) $(BYTEFLAGS) $(CUSTOM) -thread -o $@ $(SYSCMA) $^
 
 # coqmktop
 $(COQMKTOP): $(patsubst %.cma,%$(BESTLIB),$(COQMKTOPCMO:.cmo=$(BESTOBJ)))
@@ -636,7 +636,7 @@ install-library:
 	$(MKDIR) $(FULLCOQLIB)
 	$(INSTALLSH) $(FULLCOQLIB) $(LIBFILES) $(PLUGINS)
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
-ifneq ($(COQRUNBYTEFLAGS),"-custom")
+ifndef CUSTOM
 	$(INSTALLLIB) $(DLLCOQRUN) $(FULLCOQLIB)
 endif
 ifeq ($(BEST),opt)
diff --git a/config/coq_config.mli b/config/coq_config.mli
index 94d0b6c93..23f7c0eb6 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -38,7 +38,7 @@ val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
 val arch_is_win32 : bool
 val osdeplibs : string  (* OS dependant link options for ocamlc *)
-val coqrunbyteflags : string (* -custom/-dllib -lcoqrun *)
+val vmbyteflags : string list (* -custom/-dllib -lcoqrun *)
 
 
 (* val defined : string list  (* options for lib/ocamlpp *) *)
diff --git a/configure.ml b/configure.ml
index e64c04254..79087a405 100644
--- a/configure.ml
+++ b/configure.ml
@@ -208,9 +208,8 @@ 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 coqrunbyteflags = ref (None : string option)
-  let coqtoolsbyteflags = ref (None : string option)
-  let custom = 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)
@@ -248,12 +247,12 @@ let args_options = Arg.align [
     "<dir> Set installation directory to <dir>";
   "-local", Arg.Set Prefs.local,
     " Set installation directory to the current source tree";
-  "-coqrunbyteflags", arg_string_option Prefs.coqrunbyteflags,
-    "<flags> Set link flags for VM-dependent bytecode (coqtop)";
-  "-coqtoolsbyteflags", arg_string_option Prefs.coqtoolsbyteflags,
-    "<flags> Set link flags for VM-independant bytecode (coqdep,coqdoc,...)";
-  "-custom", Arg.Set Prefs.custom,
-    " Generate all bytecode executables with -custom (not recommended)";
+  "-vmbyteflags", arg_string_option Prefs.vmbyteflags,
+    "<flags> Comma-separated link flags for the VM of coqtop.byte";
+  "-custom", Arg.Unit (fun () -> Prefs.custom := Some true),
+    " Build bytecode executables with -custom (not recommended)";
+  "-no-custom", Arg.Unit (fun () -> Prefs.custom := Some false),
+    " Do not build with -custom on Windows and MacOS";
   "-bindir", arg_string_option Prefs.bindir,
     "<dir> Where to install bin files";
   "-libdir", arg_string_option Prefs.libdir,
@@ -284,7 +283,7 @@ let args_options = Arg.align [
     " Specifies to use camlp4 instead of camlp5";
   "-camlp5dir",
     Arg.String (fun s -> Prefs.usecamlp5:=true; Prefs.camlp5dir:=Some s),
-    "<dir> Specifies where to look for the Camlp5 library and tells to use it";
+    "<dir> Specifies where is the Camlp5 library and tells to use it";
   "-arch", arg_string_option Prefs.arch,
     "<arch> Specifies the architecture";
   "-opt", Arg.Set Prefs.opt,
@@ -316,7 +315,7 @@ let args_options = Arg.align [
   "-makecmd", Arg.Set_string Prefs.makecmd,
     "<command> Name of GNU Make command";
   "-no-native-compiler", Arg.Clear Prefs.nativecompiler,
-    " Disables compilation to native code for conversion and normalization";
+    " No compilation to native code for conversion and normalization";
   "-coqwebsite", Arg.Set_string Prefs.coqwebsite,
     " URL of the coq website";
   "-force-caml-version", arg_bool Prefs.force_caml_version,
@@ -855,32 +854,31 @@ let datadir =
 
 (** * OCaml runtime flags *)
 
-(** Determine if we enable -custom by default (Windows and MacOS) *)
+(** Do we use -custom (yes by default on Windows and MacOS) *)
+
 let custom_os = arch_win32 || arch = "Darwin"
 
+let use_custom = match !Prefs.custom with
+  | Some b -> b
+  | None -> custom_os
+
+let custom_flag = if use_custom then "-custom" else ""
+
 let build_loadpath =
   ref "# you might want to set CAML_LD_LIBRARY_PATH by hand!"
 
 let config_runtime () =
-  match !Prefs.coqrunbyteflags with
-  | Some flags -> flags
-  | _ when !Prefs.custom || custom_os -> "-custom"
+  match !Prefs.vmbyteflags with
+  | Some flags -> string_split ',' flags
+  | _ when use_custom -> [custom_flag]
   | _ when !Prefs.local ->
-    sprintf "-dllib -lcoqrun -dllpath '%s/kernel/byterun'" coqtop
+    ["-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;
-    sprintf "-dllib -lcoqrun -dllpath '%s'" libdir
-
-let coqrunbyteflags = config_runtime ()
-
-let config_tools_runtime () =
-  match !Prefs.coqtoolsbyteflags with
-  | Some flags -> flags
-  | _ when !Prefs.custom || custom_os -> "-custom"
-  | _ -> ""
+    ["-dllib";"-lcoqrun";"-dllpath";libdir]
 
-let coqtoolsbyteflags = config_tools_runtime ()
+let vmbyteflags = config_runtime ()
 
 
 (** * Summary of the configuration *)
@@ -888,27 +886,27 @@ let coqtoolsbyteflags = config_tools_runtime ()
 let print_summary () =
   let pr s = printf s in
   pr "\n";
-  pr "  Architecture                      : %s\n" arch;
+  pr "  Architecture                : %s\n" arch;
   if operating_system <> "" then
-    pr "  Operating system                  : %s\n" operating_system;
-  pr "  Coq VM bytecode link flags        : %s\n" coqrunbyteflags;
-  pr "  Coq tools bytecode link flags     : %s\n" coqtoolsbyteflags;
-  pr "  OS dependent libraries            : %s\n" osdeplibs;
-  pr "  Objective-Caml/Camlp4 version     : %s\n" caml_version;
-  pr "  Objective-Caml/Camlp4 binaries in : %s\n" camlbin;
-  pr "  Objective-Caml library in         : %s\n" camllib;
-  pr "  Camlp4 library in                 : %s\n" camlp4lib;
+    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/Camlp4 version        : %s\n" caml_version;
+  pr "  OCaml/Camlp4 binaries in    : %s\n" camlbin;
+  pr "  OCaml library in            : %s\n" camllib;
+  pr "  Camlp4 library in           : %s\n" camlp4lib;
   if best_compiler = "opt" then
-    pr "  Native dynamic link support       : %B\n" hasnatdynlink;
+    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" !lablgtkdir;
   if !idearchdef = "QUARTZ" then
     pr "  Mac OS integration is on\n";
-  pr "  CoqIde                            : %s\n" coqide;
-  pr "  Documentation                     : %s\n"
+  pr "  CoqIde                      : %s\n" coqide;
+  pr "  Documentation               : %s\n"
     (if withdoc then "All" else "None");
-  pr "  Web browser                       : %s\n" browser;
-  pr "  Coq web site                      : %s\n\n" !Prefs.coqwebsite;
+  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
@@ -961,7 +959,7 @@ let write_configml f =
   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_s "coqrunbyteflags" coqrunbyteflags;
+  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;
@@ -1045,9 +1043,8 @@ let write_makefile f =
   pr "COQ_CONFIGURED=yes\n\n";
   pr "# Local use (no installation)\n";
   pr "LOCAL=%B\n\n" !Prefs.local;
-  pr "# Bytecode link flags for VM (\"-custom\" or \"-dllib -lcoqrun\")\n";
-  pr "COQRUNBYTEFLAGS=%s\n" coqrunbyteflags;
-  pr "COQTOOLSBYTEFLAGS=%s\n" coqtoolsbyteflags;
+  pr "# Bytecode link flags : should we use -custom or not ?\n";
+  pr "CUSTOM=%s\n" custom_flag;
   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;
diff --git a/myocamlbuild.ml b/myocamlbuild.ml
index 5669dccab..6d3a24306 100644
--- a/myocamlbuild.ml
+++ b/myocamlbuild.ml
@@ -259,9 +259,9 @@ let extra_rules () = begin
        let lines = List.map (fun s -> s^"\n") lines in
        let line0 = "\n(* Adapted variables for ocamlbuild *)\n" in
        (* TODO : line2 isn't completely accurate with respect to ./configure:
-	  the case of -local -coqrunbyteflags foo isn't supported *)
+	  the case of -local -vmbyteflags foo isn't supported *)
        let line1 =
-	 "let coqrunbyteflags = \"-dllib -lcoqrun\"\n"
+	 "let vmbyteflags = [\"-dllib\";\"-lcoqrun\"]\n"
        in
        Echo (lines @ (if local then [line0;line1] else []),
 	     "coq_config.ml"));
@@ -316,7 +316,7 @@ let extra_rules () = begin
   flag ["compile"; "c"] cflags;
   dep ["ocaml"; "use_libcoqrun"; "compile"] [libcoqrun];
   dep ["ocaml"; "use_libcoqrun"; "link"; "native"] [libcoqrun];
-  flag ["ocaml"; "use_libcoqrun"; "link"; "byte"] (Sh Coq_config.coqrunbyteflags);
+  flag ["ocaml"; "use_libcoqrun"; "link"; "byte"] (Sh Coq_config.vmbyteflags);
 
   (* we need to use a different ocamlc. For now we copy the rule *)
   if w32 then
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index b9b67f3e4..95baa8085 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -6,121 +6,145 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* coqmktop is a script to link Coq, analogous to ocamlmktop.
+(** {1 Coqmktop} *)
+
+(** coqmktop is a script to link Coq, analogous to ocamlmktop.
    The command line contains options specific to coqmktop, options for the
    Ocaml linker and files to link (in addition to the default Coq files). *)
 
-let (/) = Filename.concat
+(** {6 Utilities} *)
 
-let safe_sys_command =
-  if Sys.os_type = "Win32" then
-    fun cmd -> Sys.command ("\""^cmd^"\"")
-  else Sys.command
+(** Split a string at each blank
+*)
+let split_list =
+  let spaces = Str.regexp "[ \t\n]+" in
+  fun str -> Str.split spaces str
 
-(* Objects to link *)
+let (/) = Filename.concat
 
-(* NB: dynlink is now always linked, it is used for loading plugins
-   and compiled vm code (see native-compiler). We now reject platforms
-   with ocamlopt but no dynlink.cmxa during ./configure, and give
-   instructions there about how to build a dummy dynlink.cmxa,
-   cf. dev/dynlink.ml. *)
+(** Which user files do we support (and propagate to ocamlopt) ?
+*)
+let supported_suffix f = match CUnix.get_extension f with
+  | ".ml" | ".cmx" | ".cmo" | ".cmxa" | ".cma" | ".c" -> true
+  | _ -> false
 
-(* 1. Core objects *)
-let ocamlobjs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"]
-let camlp4objs =
-  if Coq_config.camlp4 = "camlp5" then ["gramlib.cma"] else ["camlp4lib.cma"]
-let libobjs = ocamlobjs @ camlp4objs
+(** From bytecode extension to native
+*)
+let native_suffix f = match CUnix.get_extension f with
+  | ".cmo" -> (Filename.chop_suffix f ".cmo") ^ ".cmx"
+  | ".cma" -> (Filename.chop_suffix f ".cma") ^ ".cmxa"
+  | ".a" -> f
+  | _ -> failwith ("File "^f^" has not extension .cmo, .cma or .a")
 
-let spaces = Str.regexp "[ \t\n]+"
-let split_list l = Str.split spaces l
+(** Transforms a file name in the corresponding Caml module name.
+*)
+let module_of_file name =
+  String.capitalize
+    (try Filename.chop_extension name with Invalid_argument _ -> name)
 
-let copts     = split_list Tolink.copts
-let core_objs = split_list Tolink.core_objs
-let core_libs = split_list Tolink.core_libs
+(** Run a command [prog] with arguments [args].
+    We do not use [Sys.command] anymore, see comment in [CUnix.sys_command].
+*)
+let run_command prog args =
+  match CUnix.sys_command prog args with
+  | Unix.WEXITED 127 -> failwith ("no such command "^prog)
+  | Unix.WEXITED n -> n
+  | Unix.WSIGNALED n -> failwith (prog^" killed by signal "^string_of_int n)
+  | Unix.WSTOPPED n -> failwith (prog^" stopped by signal "^string_of_int n)
 
-(* 3. Toplevel objects *)
-let camlp4topobjs =
-  if Coq_config.camlp4 = "camlp5" then
-    ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
-  else
-    [ "Camlp4Top.cmo";
-      "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
-      "Camlp4Parsers/Camlp4OCamlParser.cmo";
-      "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
-let topobjs = camlp4topobjs
 
-let gramobjs = []
-let notopobjs = gramobjs
 
-(* 4. High-level tactics objects *)
+(** {6 Coqmktop options} *)
 
-(* environment *)
 let opt        = ref false
-let full       = ref false
 let top        = ref false
 let echo       = ref false
 let no_start   = ref false
 
 let is_ocaml4 = Coq_config.caml_version.[0] <> '3'
+let is_camlp5 = Coq_config.camlp4 = "camlp5"
 
-(* Since the .cma are given with their relative paths (e.g. "lib/clib.cma"),
-   we only need to include directories mentionned in the temp main ml file
-   below (for accessing the corresponding .cmi). *)
-
-let src_dirs =
-  [ []; ["lib"]; ["toplevel"]; ["kernel/byterun"]  ]
-
-let includes () =
-  let coqlib = if !Flags.boot then "." else Envars.coqlib () in
-  let mkdir d = "\"" ^ List.fold_left (/) coqlib d ^ "\"" in
-  (List.fold_right (fun d l -> "-I" :: mkdir d :: l) src_dirs [])
-  @ ["-I"; "\"" ^ Envars.camlp4lib () ^ "\""]
-  @ (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
-
-(* Transform bytecode object file names in native object file names *)
-let native_suffix f =
-  if Filename.check_suffix f ".cmo" then
-    (Filename.chop_suffix f ".cmo") ^ ".cmx"
-  else if Filename.check_suffix f ".cma" then
-    (Filename.chop_suffix f ".cma") ^ ".cmxa"
-  else
-    if Filename.check_suffix f ".a" then f
-    else
-      failwith ("File "^f^" has not extension .cmo, .cma or .a")
 
-(* Transforms a file name in the corresponding Caml module name. *)
-let rem_ext_regexpr = Str.regexp "\\(.*\\)\\.\\(cm..?\\|ml\\)"
+(** {6 Includes options} *)
 
-let module_of_file name =
-  let s = Str.replace_first rem_ext_regexpr "\\1" (Filename.basename name) in
-  String.capitalize s
+(** Since the Coq core .cma are given with their relative paths
+    (e.g. "lib/clib.cma"), we only need to include directories mentionned in
+    the temp main ml file below (for accessing the corresponding .cmi). *)
 
-(* Build the list of files to link and the list of modules names *)
-let files_to_link userfiles =
-  let toplevel_objs =
-    if !top then topobjs else if !opt then notopobjs else [] in
-  let objs = libobjs @ core_objs @ toplevel_objs in
-  let modules = List.map module_of_file (objs @ userfiles)
-  in
-  let libs = libobjs @ core_libs @ toplevel_objs in
-  let libstolink =
-    (if !opt then List.map native_suffix libs else libs) @ userfiles
-  in
-  (modules, libstolink)
+let std_includes basedir =
+  let rebase d = match basedir with None -> d | Some base -> base / d in
+  ["-I"; rebase ".";
+   "-I"; rebase "lib";
+   "-I"; rebase "toplevel";
+   "-I"; rebase "kernel/byterun";
+   "-I"; Envars.camlp4lib () ] @
+  (if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
 
-(* Gives the list of all the directories under [dir]. *)
-let all_subdirs dir =
-  let l = ref [] in
-  let add f = l := f :: !l in
+(** For the -R option, visit all directories under [dir] and add
+    corresponding -I to the [opts] option list (in reversed order) *)
+let incl_all_subdirs dir opts =
+  let l = ref opts in
+  let add f = l := f :: "-I" :: !l in
   let rec traverse dir =
     if Sys.file_exists dir && Sys.is_directory dir then
       let () = add dir in
-      let subdirs = try Sys.readdir dir with _ -> [||] in
+      let subdirs = try Sys.readdir dir with any -> [||] in
       Array.iter (fun f -> traverse (dir/f)) subdirs
   in
-  traverse dir; List.rev !l
+  traverse dir; !l
+
+
+(** {6 Objects to link} *)
+
+(** NB: dynlink is now always linked, it is used for loading plugins
+    and compiled vm code (see native-compiler). We now reject platforms
+    with ocamlopt but no dynlink.cmxa during ./configure, and give
+    instructions there about how to build a dummy dynlink.cmxa,
+    cf. dev/dynlink.ml. *)
+
+(** OCaml + CamlpX libraries *)
+
+let ocaml_libs = ["str.cma";"unix.cma";"nums.cma";"dynlink.cma";"threads.cma"]
+let camlp4_libs = if is_camlp5 then ["gramlib.cma"] else ["camlp4lib.cma"]
+let libobjs = ocaml_libs @ camlp4_libs
+
+(** Toplevel objects *)
+
+let ocaml_topobjs =
+  if is_ocaml4 then
+    ["ocamlcommon.cma";"ocamlbytecomp.cma";"ocamltoplevel.cma"]
+  else
+    ["toplevellib.cma"]
+
+let camlp4_topobjs =
+  if is_camlp5 then
+    ["camlp5_top.cma"; "pa_o.cmo"; "pa_extend.cmo"]
+  else
+    [ "Camlp4Top.cmo";
+      "Camlp4Parsers/Camlp4OCamlRevisedParser.cmo";
+      "Camlp4Parsers/Camlp4OCamlParser.cmo";
+      "Camlp4Parsers/Camlp4GrammarParser.cmo" ]
+
+let topobjs = ocaml_topobjs @ camlp4_topobjs
+
+(** Coq Core objects *)
+
+let copts = (split_list Coq_config.osdeplibs) @ (split_list Tolink.copts)
+let core_objs = split_list Tolink.core_objs
+let core_libs = split_list Tolink.core_libs
+
+(** Build the list of files to link and the list of modules names
+*)
+let files_to_link userfiles =
+  let top = if !top then topobjs else [] in
+  let modules = List.map module_of_file (top @ core_objs @ userfiles) in
+  let objs = libobjs @ top @ core_libs in
+  let objs' = (if !opt then List.map native_suffix objs else objs) @ userfiles
+  in (modules, objs')
+
+
+(** {6 Parsing of the command-line} *)
 
-(* usage *)
 let usage () =
   prerr_endline "Usage: coqmktop <options> <ocaml options> files\
 \nFlags are:\
@@ -130,63 +154,56 @@ let usage () =
 \n  -o exec-file   Specify the name of the resulting toplevel\
 \n  -boot          Run in boot mode\
 \n  -echo          Print calls to external commands\
-\n  -full          Link high level tactics\
 \n  -opt           Compile in native code\
 \n  -top           Build Coq on a OCaml toplevel (incompatible with -opt)\
 \n  -R dir         Add recursively dir to OCaml search path\
 \n";
   exit 1
 
-(* parsing of the command line *)
 let parse_args () =
   let rec parse (op,fl) = function
     | [] -> List.rev op, List.rev fl
+
+    (* Directories *)
     | "-coqlib" :: d :: rem ->
 	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
-    | "-coqlib" :: _        -> usage ()
     | "-camlbin" :: d :: rem ->
 	Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
-    | "-camlbin" :: _        -> usage ()
     | "-camlp4bin" :: d :: rem ->
 	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
-    | "-camlp4bin" :: _        -> usage ()
+    | "-R" :: d :: rem -> parse (incl_all_subdirs d op,fl) rem
+    | ("-coqlib"|"-camlbin"|"-camlp4bin"|"-R") :: [] -> usage ()
+
+    (* Boolean options of coqmktop *)
     | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
     | "-opt" :: rem -> opt := true ; parse (op,fl) rem
-    | "-full" :: rem -> full := true ; parse (op,fl) rem
     | "-top" :: rem -> top := true ; parse (op,fl) rem
-    | "-v8" :: rem ->
-	Printf.eprintf "warning: option -v8 deprecated";
-	parse (op,fl) rem
+    | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem
     | "-echo" :: rem -> echo := true ; parse (op,fl) rem
+    | ("-v8"|"-full" as o) :: rem ->
+	Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem
+
+    (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *)
+    | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
+        parse (o::op,fl) rem
     | ("-cclib"|"-ccopt"|"-I"|"-o"|"-w" as o) :: rem' ->
 	begin
 	  match rem' with
 	    | a :: rem -> parse (a::o::op,fl) rem
 	    | []       -> usage ()
 	end
-    | "-R" :: a :: rem ->
-        parse ((List.rev(List.flatten (List.map (fun d -> ["-I";d])
-					 (all_subdirs a))))@op,fl) rem
-    | "-R" :: [] -> usage ()
-    | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
-        parse (o::op,fl) rem
-    | ("-h"|"--help") :: _ -> usage ()
-    | ("-no-start") :: rem -> no_start:=true; parse (op, fl) rem
-    | f :: rem ->
-	if Filename.check_suffix f ".ml"
-          || Filename.check_suffix f ".cmx"
-	  || Filename.check_suffix f ".cmo"
-	  || Filename.check_suffix f ".cmxa"
-	  || Filename.check_suffix f ".cma"
-	  || Filename.check_suffix f ".c" then
-	    parse (op,f::fl) rem
-	else begin
-	  prerr_endline ("Don't know what to do with " ^ f);
-	  exit 1
-	end
+
+    | ("-h"|"-help"|"--help") :: _ -> usage ()
+    | f :: rem when supported_suffix f -> parse (op,f::fl) rem
+    | f :: _ -> prerr_endline ("Don't know what to do with " ^ f); exit 1
   in
-  parse ([Coq_config.osdeplibs],[]) (List.tl (Array.to_list Sys.argv))
+  parse ([],[]) (List.tl (Array.to_list Sys.argv))
 
+
+(** {6 Temporary main file} *)
+
+(** remove the temporary main file
+*)
 let clean file =
   let rm f = if Sys.file_exists f then Sys.remove f in
   let basename = Filename.chop_suffix file ".ml" in
@@ -198,7 +215,8 @@ let clean file =
     rm (basename ^ ".cmx")
   end
 
-(* Initializes the kind of loading in the main program *)
+(** Initializes the kind of loading in the main program
+*)
 let declare_loading_string () =
   if not !top then
     "Mltop.remove ();;"
@@ -216,13 +234,15 @@ let declare_loading_string () =
 \n     let ppf = Format.std_formatter;;\
 \n     Mltop.set_top\
 \n       {Mltop.load_obj=\
-\n         (fun f -> if not (Topdirs.load_file ppf f) then Errors.error (\"Could not load plugin \"^f));\
+\n         (fun f -> if not (Topdirs.load_file ppf f)\
+\n                   then Errors.error (\"Could not load plugin \"^f));\
 \n        Mltop.use_file=Topdirs.dir_use ppf;\
 \n        Mltop.add_dir=Topdirs.dir_directory;\
 \n        Mltop.ml_loop=(fun () -> Toploop.loop ppf) };;\
 \n"
 
-(* create a temporary main file to link *)
+(** create a temporary main file to link
+*)
 let create_tmp_main_file modules =
   let main_name,oc = Filename.open_temp_file "coqmain" ".ml" in
   try
@@ -233,63 +253,54 @@ let create_tmp_main_file modules =
     (* Initializes the kind of loading *)
     output_string oc (declare_loading_string());
     (* Start the toplevel loop *)
-    if not !no_start then
-    output_string oc "Coqtop.start();;\n";
+    if not !no_start then output_string oc "Coqtop.start();;\n";
     close_out oc;
     main_name
   with reraise ->
     clean main_name; raise reraise
 
-(* main part *)
+
+(** {6 Main } *)
+
 let main () =
   let (options, userfiles) = parse_args () in
+  (* Directories: *)
   let () = Envars.set_coqlib ~fail:Errors.error in
-  (* which ocaml command to invoke *)
   let camlbin = Envars.camlbin () in
-  let prog =
-    if !opt then begin
-      (* native code *)
-      if !top then failwith "no custom toplevel in native code !";
-      let ocamloptexec = Filename.quote (camlbin/"ocamlopt") in
-        ocamloptexec^" -linkall"
-    end else
-      (* bytecode (we shunt ocamlmktop script which fails on win32) *)
-      let ocamlmktoplib = if is_ocaml4
-	then " ocamlcommon.cma ocamlbytecomp.cma ocamltoplevel.cma"
-	else " toplevellib.cma" in
-      let ocamlcexec = Filename.quote (camlbin/"ocamlc") in
-      let ocamlccustom = Printf.sprintf "%s %s -linkall "
-        ocamlcexec Coq_config.coqrunbyteflags in
-      (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
-  in
-  (* files to link *)
+  let basedir = if !Flags.boot then None else Some (Envars.coqlib ()) in
+  (* Which ocaml compiler to invoke *)
+  let prog = camlbin/(if !opt then "ocamlopt" else "ocamlc") in
+  (* Which arguments ? *)
+  if !opt && !top then failwith "no custom toplevel in native code !";
+  let flags = if !opt then [] else Coq_config.vmbyteflags in
+  let topstart = if !top then [ "topstart.cmo" ] else [] in
   let (modules, tolink) = files_to_link userfiles in
-  (* the list of the loaded modules *)
   let main_file = create_tmp_main_file modules in
   try
+    (* - We add topstart.cmo explicitly because we shunted ocamlmktop wrapper.
+       - With the coq .cma, we MUST use the -linkall option. *)
     let args =
-      options @ (includes ()) @ copts @ tolink @ [ Filename.quote main_file ]
+      "-linkall" :: "-rectypes" :: flags @ copts @ options @
+      (std_includes basedir) @ tolink @ [ main_file ] @ topstart
     in
-    (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
-    let args = if !top then args @ [ "topstart.cmo" ] else args in
-      (* Now, with the .cma, we MUST use the -linkall option *)
-    let command = String.concat " " (prog::"-rectypes"::args) in
-      if !echo then
-	begin
-	  print_endline command;
-	  print_endline
-	    ("(command length is " ^
-	       (string_of_int (String.length command)) ^ " characters)");
-	  flush Pervasives.stdout
-	end;
-      let retcode = safe_sys_command command in
-	clean main_file;
-	(* command gives the exit code in HSB, and signal in LSB !!! *)
-	if retcode > 255 then retcode lsr 8 else retcode
-  with reraise ->
-    clean main_file; raise reraise
+    if !echo then begin
+      let command = String.concat " " (prog::args) in
+      print_endline command;
+      print_endline
+	("(command length is " ^
+	    (string_of_int (String.length command)) ^ " characters)");
+      flush Pervasives.stdout
+    end;
+    let exitcode = run_command prog args in
+    clean main_file;
+    exitcode
+  with reraise -> clean main_file; raise reraise
 
-let retcode =
-  try Printexc.print main () with any -> 1
+let pr_exn = function
+  | Failure msg -> msg
+  | Unix.Unix_error (err,fn,arg) -> fn^" "^arg^" : "^Unix.error_message err
+  | any -> Printexc.to_string any
 
-let _ = exit retcode
+let _ =
+  try exit (main ())
+  with any -> Printf.eprintf "Error: %s\n" (pr_exn any); exit 1