Imported Upstream version 8.5~beta1+dfsg

1 files changed, 465 insertions, 222 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index d2eb7d9c..142f3386 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -1,36 +1,96 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open System
 open Flags
 open Names
 open Libnames
-open Nameops
 open States
-open Toplevel
 open Coqinit
 
+let () = at_exit flush_all
+
+let ( / ) = Filename.concat
+
+let fatal_error info anomaly =
+  let msg = info ++ fnl () in
+  pp_with ~pp_tag:Ppstyle.pp_tag !Pp_control.err_ft msg;
+  flush_all ();
+  exit (if anomaly then 129 else 1)
+
 let get_version_date () =
   try
-    let coqlib = Envars.coqlib () in
-    let ch = open_in (Filename.concat coqlib "revision") in
+    let ch = open_in (Envars.coqlib () / "revision") in
     let ver = input_line ch in
     let rev = input_line ch in
-      (ver,rev)
+    let () = close_in ch in
+    (ver,rev)
   with e when Errors.noncritical e ->
     (Coq_config.version,Coq_config.date)
 
 let print_header () =
-  let (ver,rev) = (get_version_date ()) in
-    Printf.printf "Welcome to Coq %s (%s)\n" ver rev;
-    flush stdout
+  let (ver,rev) = get_version_date () in
+  ppnl (str ("Welcome to Coq "^ver^" ("^rev^")"));
+  pp_flush ()
+
+let warning s = msg_warning (strbrk s)
+
+let toploop = ref None
+
+let color : [`ON | `AUTO | `OFF] ref = ref `AUTO
+let set_color = function
+| "on" -> color := `ON
+| "off" -> color := `OFF
+| "auto" -> color := `AUTO
+| _ -> prerr_endline ("Error: on/off/auto expected after option color"); exit 1
+
+let init_color () =
+  let has_color = match !color with
+  | `OFF -> false
+  | `ON -> true
+  | `AUTO ->
+    Terminal.has_style Unix.stdout &&
+    Terminal.has_style Unix.stderr
+  in
+  if has_color then begin
+    let colors = try Some (Sys.getenv "COQ_COLORS") with Not_found -> None in
+    match colors with
+    | None ->
+      (** Default colors *)
+      Ppstyle.init_color_output ()
+    | Some "" ->
+      (** No color output *)
+      ()
+    | Some s ->
+      (** Overwrite all colors *)
+      Ppstyle.clear_styles ();
+      Ppstyle.parse_config s;
+      Ppstyle.init_color_output ()
+  end
+
+let toploop_init = ref begin fun x ->
+  let () = init_color () in
+  let () = CoqworkmgrApi.(init !Flags.async_proofs_worker_priority) in
+  x
+  end
+
+let toploop_run = ref (fun () ->
+  if Dumpglob.dump () then begin
+    if_verbose warning "Dumpglob cannot be used in interactive mode.";
+    Dumpglob.noglob ()
+  end;
+  Coqloop.loop();
+  (* Initialise and launch the Ocaml toplevel *)
+  Coqinit.init_ocaml_path();
+  Mltop.ocaml_toploop())
 
 let output_context = ref false
 
@@ -38,7 +98,8 @@ let memory_stat = ref false
 
 let print_memory_stat () =
   if !memory_stat then
-    Format.printf "total heap size = %d kbytes\n" (heap_size_kb ())
+    ppnl
+      (str "total heap size = " ++ int (CObj.heap_size_kb ()) ++ str " kbytes")
 
 let _ = at_exit print_memory_stat
 
@@ -47,40 +108,40 @@ let set_engagement c = engagement := Some c
 let engage () =
   match !engagement with Some c -> Global.set_engagement c | None -> ()
 
+let type_in_type = ref false
+let set_type_in_type () = type_in_type := true
+let set_hierarchy () = if !type_in_type then Global.set_type_in_type ()
+
 let set_batch_mode () = batch_mode := true
 
-let toplevel_default_name = make_dirpath [id_of_string "Top"]
+let toplevel_default_name = DirPath.make [Id.of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
 let set_toplevel_name dir =
-  if dir = empty_dirpath then error "Need a non empty toplevel module name";
+  if DirPath.is_empty dir then error "Need a non empty toplevel module name";
   toplevel_name := Some dir
 let unset_toplevel_name () = toplevel_name := None
 
 let remove_top_ml () = Mltop.remove ()
 
-let inputstate = ref None
-let set_inputstate s = inputstate:= Some s
-let inputstate () =
-  match !inputstate with
-    | Some "" -> ()
-    | Some s -> intern_state s
-    | None -> intern_state "initial.coq"
+let inputstate = ref ""
+let set_inputstate s =
+  let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in
+  inputstate:=s
+let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate
 
 let outputstate = ref ""
-let set_outputstate s = outputstate:=s
-let outputstate () = if !outputstate <> "" then extern_state !outputstate
+let set_outputstate s =
+  let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in
+  outputstate:=s
+let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate
 
-let set_default_include d = push_include (d,Nameops.default_root_prefix)
-let set_include d p =
+let set_include d p recursive implicit =
   let p = dirpath_of_string p in
-  push_include (d,p)
-let set_rec_include d p =
-  let p = dirpath_of_string p in
-  push_rec_include(d,p)
+  push_include d p recursive implicit
 
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
-  load_vernacular_list := ((make_suffix s ".v"),verb) :: !load_vernacular_list
+  load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
 let load_vernacular () =
   List.iter
     (fun (s,b) ->
@@ -96,29 +157,57 @@ let load_vernac_obj () =
   List.iter (fun f -> Library.require_library_from_file None f None)
     (List.rev !load_vernacular_obj)
 
+let require_prelude () =
+  let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
+  let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in
+  let m =
+    if Sys.file_exists vo then vo else
+    if Sys.file_exists vio then vio else vo in
+  Library.require_library_from_dirpath [Coqlib.prelude_module,m] (Some true)
+
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
 let require () =
+  if !load_init then silently require_prelude ();
   List.iter (fun s -> Library.require_library_from_file None s (Some false))
     (List.rev !require_list)
 
 let compile_list = ref ([] : (bool * string) list)
+
+let glob_opt = ref false
+
 let add_compile verbose s =
   set_batch_mode ();
   Flags.make_silent true;
+  if not !glob_opt then Dumpglob.dump_to_dotglob ();
+  (** make the file name explicit; needed not to break up Coq loadpath stuff. *)
+  let s =
+    let open Filename in
+    if is_implicit s
+    then concat current_dir_name s
+    else s
+  in
   compile_list := (verbose,s) :: !compile_list
+
+let compile_file (v,f) =
+  if Flags.do_beautify () then
+    with_option beautify_file (Vernac.compile v) f
+  else
+    Vernac.compile v f
+
 let compile_files () =
-  let init_state = States.freeze() in
-  let coqdoc_init_state = Dumpglob.coqdoc_freeze () in
-    List.iter
-      (fun (v,f) ->
-	 States.unfreeze init_state;
-	 Dumpglob.coqdoc_unfreeze coqdoc_init_state;
-	 if Flags.do_beautify () then
-	   with_option beautify_file (Vernac.compile v) f
-	 else
-	   Vernac.compile v f)
-      (List.rev !compile_list)
+  match !compile_list with
+    | [] -> ()
+    | [vf] -> compile_file vf (* One compilation : no need to save init state *)
+    | l ->
+      let init_state = States.freeze ~marshallable:`No in
+      let coqdoc_init_state = Lexer.location_table () in
+      List.iter
+        (fun vf ->
+	  States.unfreeze init_state;
+	  Lexer.restore_location_table coqdoc_init_state;
+          compile_file vf)
+        (List.rev l)
 
 (*s options for the virtual machine *)
 
@@ -129,248 +218,402 @@ let set_vm_opt () =
   Vm.set_transp_values (not !boxed_val);
   Vconv.set_use_vm !use_vm
 
+(** Options for proof general *)
+
+let set_emacs () =
+  Flags.print_emacs := true;
+  Pp.make_pp_emacs ();
+  Vernacentries.qed_display_script := false;
+  color := `OFF
+
+(** GC tweaking *)
+
+(** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
+    minor heap is heavily sollicited. Unfortunately, the default size is far too
+    small, so we enlarge it a lot (128 times larger).
+
+    To better handle huge memory consumers, we also augment the default major
+    heap increment and the GC pressure coefficient.
+*)
+
+let init_gc () =
+  let param =
+    try ignore (Sys.getenv "OCAMLRUNPARAM"); true
+    with Not_found -> false
+  in
+  let control = Gc.get () in
+  let tweaked_control = { control with
+    Gc.minor_heap_size = 33554432; (** 4M *)
+(*     Gc.major_heap_increment = 268435456; (** 32M *) *)
+    Gc.space_overhead = 120;
+  } in
+  if param then ()
+  else Gc.set tweaked_control
+
 (*s Parsing of the command line.
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
     between coqtop and coqc. *)
 
 let usage () =
-  if !batch_mode then
-    Usage.print_usage_coqc ()
-  else
-    Usage.print_usage_coqtop () ;
-  flush stderr ;
-  exit 1
+  Envars.set_coqlib Errors.error;
+  init_load_path ();
+  if !batch_mode then Usage.print_usage_coqc ()
+  else begin
+    Mltop.load_ml_objects_raw_rex
+      (Str.regexp (if Mltop.is_native then "^.*top.cmxs$" else "^.*top.cma$"));
+    Usage.print_usage_coqtop ()
+  end
+
+let print_style_tags () =
+  let () = init_color () in
+  let tags = Ppstyle.dump () in
+  let iter (t, st) =
+    let st = match st with Some st -> st | None -> Terminal.make () in
+    let opt =
+      Terminal.eval st ^
+      String.concat "." (Ppstyle.repr t) ^
+      Terminal.reset ^ "\n"
+    in
+    print_string opt
+  in
+  List.iter iter tags;
+  flush_all ()
 
-let warning s = msg_warning (str s)
+let error_missing_arg s =
+  prerr_endline ("Error: extra argument expected after option "^s);
+  prerr_endline "See -help for the syntax of supported options";
+  exit 1
 
-let ide_slave = ref false
 let filter_opts = ref false
+let exitcode () = if !filter_opts then 2 else 0
 
 let verb_compat_ntn = ref false
 let no_compat_ntn = ref false
 
-let parse_args arglist =
-  let glob_opt = ref false in
-  let rec parse = function
-    | [] -> []
-    | "-with-geoproof" :: s :: rem ->
-	if s = "yes" then Coq_config.with_geoproof := true
-	else if s = "no" then Coq_config.with_geoproof := false
-	else usage ();
-	parse rem
-    | "-impredicative-set" :: rem ->
-        set_engagement Declarations.ImpredicativeSet; parse rem
-
-    | ("-I"|"-include") :: d :: "-as" :: p :: rem -> set_include d p; parse rem
-    | ("-I"|"-include") :: d :: "-as" :: [] -> usage ()
-    | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
-    | ("-I"|"-include") :: []       -> usage ()
-
-    | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem
-    | "-R" :: d :: "-as" :: [] -> usage ()
-    | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem
-    | "-R" :: ([] | [_]) -> usage ()
-
-    | "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem
-    | "-top" :: [] -> usage ()
-
-    | "-exclude-dir" :: f :: rem -> exclude_search_in_dirname f; parse rem
-    | "-exclude-dir" :: [] -> usage ()
-
-    | "-notop" :: rem -> unset_toplevel_name (); parse rem
-    | "-q" :: rem -> no_load_rc (); parse rem
-
-    | "-opt" :: rem -> warning "option -opt deprecated, call with .opt suffix\n"; parse rem
-    | "-byte" :: rem -> warning "option -byte deprecated, call with .byte suffix\n"; parse rem
-    | "-full" :: rem -> warning "option -full deprecated\n"; parse rem
-
-    | "-batch" :: rem -> set_batch_mode (); parse rem
-    | "-boot" :: rem -> boot := true; no_load_rc (); parse rem
-    | "-quality" :: rem -> term_quality := true; no_load_rc (); parse rem
-    | "-outputstate" :: s :: rem ->
-      Flags.load_proofs := Flags.Force; set_outputstate s; parse rem
-    | "-outputstate" :: []       -> usage ()
-
-    | "-nois" :: rem -> set_inputstate ""; parse rem
-
-    | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
-    | ("-inputstate"|"-is") :: []       -> usage ()
+let print_where = ref false
+let print_config = ref false
+let print_tags = ref false
 
-    | "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f; parse rem
-    | "-load-ml-object" :: []       -> usage ()
+let get_priority opt s =
+  try Flags.priority_of_string s
+  with Invalid_argument _ ->
+    prerr_endline ("Error: low/high expected after "^opt); exit 1
 
-    | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem
-    | "-load-ml-source" :: []       -> usage ()
+let get_async_proofs_mode opt = function
+  | "off" -> Flags.APoff
+  | "on" -> Flags.APon
+  | "lazy" -> Flags.APonLazy
+  | _ -> prerr_endline ("Error: on/off/lazy expected after "^opt); exit 1
 
-    | ("-load-vernac-source"|"-l") :: f :: rem ->
-	add_load_vernacular false f; parse rem
-    | ("-load-vernac-source"|"-l") :: []       -> usage ()
+let get_cache opt = function
+  | "force" -> Some Flags.Force
+  | _ -> prerr_endline ("Error: force expected after "^opt); exit 1
 
-    | ("-load-vernac-source-verbose"|"-lv") :: f :: rem ->
-	add_load_vernacular true f; parse rem
-    | ("-load-vernac-source-verbose"|"-lv") :: []       -> usage ()
 
-    | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
-    | "-load-vernac-object" :: []       -> usage ()
+let set_worker_id opt s =
+  assert (s <> "master");
+  Flags.async_proofs_worker_id := s
 
-    | "-dump-glob" :: "stdout" :: rem -> Dumpglob.dump_to_stdout (); glob_opt := true; parse rem
-	  (* À ne pas documenter : l'option 'stdout' n'étant
-	     éventuellement utile que pour le debugging... *)
-    | "-dump-glob" :: f :: rem -> Dumpglob.dump_into_file f; glob_opt := true; parse rem
-    | "-dump-glob" :: []       -> usage ()
-    | ("-no-glob" | "-noglob") :: rem -> Dumpglob.noglob (); glob_opt := true; parse rem
+let get_bool opt = function
+  | "yes" -> true
+  | "no" -> false
+  | _ -> prerr_endline ("Error: yes/no expected after option "^opt); exit 1
 
-    | "-require" :: f :: rem -> add_require f; parse rem
-    | "-require" :: []       -> usage ()
+let get_int opt n =
+  try int_of_string n
+  with Failure _ ->
+    prerr_endline ("Error: integer expected after option "^opt); exit 1
 
-    | "-compile" :: f :: rem -> add_compile false f; if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
-    | "-compile" :: []       -> usage ()
+let get_host_port opt s =
+  match CString.split ':' s with
+  | [host; port] -> Some (Spawned.Socket(host, int_of_string port))
+  | ["stdfds"] -> Some Spawned.AnonPipe
+  | _ ->
+     prerr_endline ("Error: host:port or stdfds expected after option "^opt);
+     exit 1
 
-    | "-compile-verbose" :: f :: rem -> add_compile true f;  if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
-    | "-compile-verbose" :: []       -> usage ()
+let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
 
-    | "-force-load-proofs" :: rem -> Flags.load_proofs := Flags.Force; parse rem
-    | "-lazy-load-proofs" :: rem -> Flags.load_proofs := Flags.Lazy; parse rem
-    | "-dont-load-proofs" :: rem -> Flags.load_proofs := Flags.Dont; parse rem
+let vio_tasks = ref []
 
-    | "-beautify" :: rem -> make_beautify true; parse rem
-
-    | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
-    | "-unsafe" :: []       -> usage ()
-
-    | "-debug" :: rem -> set_debug (); parse rem
-
-    | "-compat" :: v :: rem ->
-        Flags.compat_version := get_compat_version v; parse rem
-    | "-compat" :: []       -> usage ()
-
-    | "-verbose-compat-notations" :: rem -> verb_compat_ntn := true; parse rem
-    | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem
-
-    | "-vm" :: rem -> use_vm := true; parse rem
-    | "-emacs" :: rem ->
-	Flags.print_emacs := true; Pp.make_pp_emacs();
-	Vernacentries.qed_display_script := false;
-	parse rem
-    | "-emacs-U" :: rem ->
-	warning "Obsolete option \"-emacs-U\", use -emacs instead.";	
-	parse ("-emacs" :: rem)
-
-    | "-unicode" :: rem -> add_require "Utf8_core"; parse rem
-
-    | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
-    | "-coqlib" :: [] -> usage ()
-
-    | "-where" :: _ -> print_endline (Envars.coqlib ()); exit (if !filter_opts then 2 else 0)
-
-    | ("-config"|"--config") :: _ -> Usage.print_config (); exit (if !filter_opts then 2 else 0)
-
-    | ("-quiet"|"-silent") :: rem -> Flags.make_silent true; parse rem
-
-    | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
-
-    | ("-v"|"--version") :: _ -> Usage.version (if !filter_opts then 2 else 0)
-
-    | "-init-file" :: f :: rem -> set_rcfile f; parse rem
-    | "-init-file" :: []       -> usage ()
-
-    | "-notactics" :: rem ->
-	warning "Obsolete option \"-notactics\".";
-	remove_top_ml (); parse rem
-
-    | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
-
-    | ("-m" | "--memory") :: rem -> memory_stat := true; parse rem
-
-    | "-xml" :: rem -> Flags.xml_export := true; parse rem
-
-    | "-output-context" :: rem -> output_context := true; parse rem
-
-    (* Scanned in Flags. *)
-    | "-v7" :: rem -> error "This version of Coq does not support v7 syntax"
-    | "-v8" :: rem -> parse rem
-
-    | "-no-hash-consing" :: rem -> Flags.hash_cons_proofs := false; parse rem
-
-    | "-ideslave" :: rem -> ide_slave := true; parse rem
+let add_vio_task f =
+  set_batch_mode ();
+  Flags.make_silent true;
+  vio_tasks := f :: !vio_tasks
+
+let check_vio_tasks () =
+  let rc =
+    List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
+      true (List.rev !vio_tasks) in
+  if not rc then exit 1
+
+let vio_files = ref []
+let vio_files_j = ref 0
+let vio_checking = ref false
+let add_vio_file f =
+  set_batch_mode ();
+  Flags.make_silent true;
+  vio_files := f :: !vio_files
+
+let set_vio_checking_j opt j =
+  try vio_files_j := int_of_string j
+  with Failure _ ->
+    prerr_endline ("The first argument of " ^ opt ^ " must the number");
+    prerr_endline "of concurrent workers to be used (a positive integer).";
+    prerr_endline "Makefiles generated by coq_makefile should be called";
+    prerr_endline "setting the J variable like in 'make vio2vo J=3'";
+    exit 1
+
+let is_not_dash_option = function
+  | Some f when String.length f > 0 && f.[0] <> '-' -> true
+  | _ -> false
+
+let schedule_vio_checking () =
+  if !vio_files <> [] && !vio_checking then
+    Vio_checking.schedule_vio_checking !vio_files_j !vio_files
+let schedule_vio_compilation () =
+  if !vio_files <> [] && not !vio_checking then
+    Vio_checking.schedule_vio_compilation !vio_files_j !vio_files
+
+let get_native_name s =
+  (* We ignore even critical errors because this mode has to be super silent *)
+  try
+    String.concat Filename.dir_sep [Filename.dirname s;
+      Nativelib.output_dir; Library.native_name_from_filename s]
+  with _ -> ""
 
-    | "-filteropts" :: rem -> filter_opts := true; parse rem
+let parse_args arglist =
+  let args = ref arglist in
+  let extras = ref [] in
+  let rec parse () = match !args with
+  | [] -> List.rev !extras
+  | opt :: rem ->
+    args := rem;
+    let next () = match !args with
+      | x::rem -> args := rem; x
+      | [] -> error_missing_arg opt
+    in
+    let peek_next () = match !args with
+      | x::_ -> Some x
+      | [] -> None
+    in
+    begin match opt with
+
+    (* Complex options with many args *)
+    |"-I"|"-include" ->
+      begin match rem with
+      | d :: "-as" :: p :: rem -> set_include d p false true; args := rem
+      | d :: "-as" :: [] -> error_missing_arg "-as"
+      | d :: rem -> push_ml_include d; args := rem
+      | [] -> error_missing_arg opt
+      end
+    |"-Q" ->
+      begin match rem with
+      | d :: p :: rem -> set_include d p true false; args := rem
+      | _ -> error_missing_arg opt
+      end
+    |"-R" ->
+      begin match rem with
+      | d :: "-as" :: [] -> error_missing_arg "-as"
+      | d :: "-as" :: p :: rem
+      | d :: p :: rem -> set_include d p true true; args := rem
+      | _ -> error_missing_arg opt
+      end
 
-    | s :: rem ->
-      if !filter_opts then
-       s :: (parse rem)
-      else
-       (prerr_endline ("Don't know what to do with " ^ s); usage ())
+    (* Options with two arg *)
+    |"-check-vio-tasks" ->
+        let tno = get_task_list (next ()) in
+        let tfile = next () in
+        add_vio_task (tno,tfile)
+    |"-schedule-vio-checking" ->
+        vio_checking := true;
+        set_vio_checking_j opt (next ());
+        add_vio_file (next ());
+        while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
+    |"-schedule-vio2vo" ->
+        set_vio_checking_j opt (next ());
+        add_vio_file (next ());
+        while is_not_dash_option (peek_next ()) do add_vio_file (next ()); done
+
+    (* Options with one arg *)
+    |"-coqlib" -> Flags.coqlib_spec:=true; Flags.coqlib:=(next ())
+    |"-async-proofs" ->
+        Flags.async_proofs_mode := get_async_proofs_mode opt (next())
+    |"-async-proofs-j" ->
+        Flags.async_proofs_n_workers := (get_int opt (next ()))
+    |"-async-proofs-cache" ->
+        Flags.async_proofs_cache := get_cache opt (next ())
+    |"-async-proofs-tac-j" ->
+        Flags.async_proofs_n_tacworkers := (get_int opt (next ()))
+    |"-async-proofs-worker-priority" ->
+        Flags.async_proofs_worker_priority := get_priority opt (next ())
+    |"-async-proofs-private-flags" ->
+        Flags.async_proofs_private_flags := Some (next ());
+    |"-worker-id" -> set_worker_id opt (next ())
+    |"-compat" -> Flags.compat_version := get_compat_version (next ())
+    |"-compile" -> add_compile false (next ())
+    |"-compile-verbose" -> add_compile true (next ())
+    |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
+    |"-feedback-glob" -> Dumpglob.feedback_glob ()
+    |"-exclude-dir" -> exclude_search_in_dirname (next ())
+    |"-init-file" -> set_rcfile (next ())
+    |"-inputstate"|"-is" -> set_inputstate (next ())
+    |"-load-ml-object" -> Mltop.dir_ml_load (next ())
+    |"-load-ml-source" -> Mltop.dir_ml_use (next ())
+    |"-load-vernac-object" -> add_vernac_obj (next ())
+    |"-load-vernac-source"|"-l" -> add_load_vernacular false (next ())
+    |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ())
+    |"-outputstate" -> set_outputstate (next ())
+    |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
+    |"-require" -> add_require (next ())
+    |"-top" -> set_toplevel_name (dirpath_of_string (next ()))
+    |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
+    |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
+    |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
+    |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
+    |"-toploop" -> toploop := Some (next ())
+
+    (* Options with zero arg *)
+    |"-async-queries-always-delegate"
+    |"-async-proofs-always-delegate"
+    |"-async-proofs-full" ->
+        Flags.async_proofs_full := true;
+    |"-async-proofs-never-reopen-branch" ->
+        Flags.async_proofs_never_reopen_branch := true;
+    |"-batch" -> set_batch_mode ()
+    |"-beautify" -> make_beautify true
+    |"-boot" -> boot := true; no_load_rc ()
+    |"-bt" -> Backtrace.record_backtrace true
+    |"-color" -> set_color (next ())
+    |"-config"|"--config" -> print_config := true
+    |"-debug" -> set_debug ()
+    |"-emacs" -> set_emacs ()
+    |"-filteropts" -> filter_opts := true
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
+    |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
+    |"-impredicative-set" -> set_engagement Declarations.ImpredicativeSet
+    |"-indices-matter" -> Indtypes.enforce_indices_matter ()
+    |"-just-parsing" -> Vernac.just_parsing := true
+    |"-m"|"--memory" -> memory_stat := true
+    |"-noinit"|"-nois" -> load_init := false
+    |"-no-compat-notations" -> no_compat_ntn := true
+    |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
+    |"-no-native-compiler" -> no_native_compiler := true
+    |"-notop" -> unset_toplevel_name ()
+    |"-output-context" -> output_context := true
+    |"-q" -> no_load_rc ()
+    |"-quiet"|"-silent" -> Flags.make_silent true
+    |"-quick" -> Flags.compilation_mode := BuildVio
+    |"-list-tags" -> print_tags := true
+    |"-time" -> Flags.time := true
+    |"-type-in-type" -> set_type_in_type ()
+    |"-unicode" -> add_require "Utf8_core"
+    |"-v"|"--version" -> Usage.version (exitcode ())
+    |"-verbose-compat-notations" -> verb_compat_ntn := true
+    |"-vm" -> use_vm := true
+    |"-where" -> print_where := true
+
+    (* Deprecated options *)
+    |"-byte" -> warning "option -byte deprecated, call with .byte suffix"
+    |"-opt" -> warning "option -opt deprecated, call with .opt suffix"
+    |"-full" -> warning "option -full deprecated"
+    |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml ()
+    |"-emacs-U" ->
+      warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs ()
+    |"-v7" -> error "This version of Coq does not support v7 syntax"
+    |"-v8" -> warning "Obsolete option \"-v8\"."
+    |"-lazy-load-proofs" -> warning "Obsolete option \"-lazy-load-proofs\"."
+    |"-dont-load-proofs" -> warning "Obsolete option \"-dont-load-proofs\"."
+    |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"."
+    |"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ())
+    |"-quality" -> warning "Obsolete option \"-quality\"."
+    |"-xml" -> warning "Obsolete option \"-xml\"."
+
+    (* Unknown option *)
+    | s -> extras := s :: !extras
+    end;
+    parse ()
   in
   try
-    parse arglist
+    parse ()
   with
-    | UserError(_,s) as e -> begin
-	try
-	  Stream.empty s; exit 1
-	with Stream.Failure ->
-	  msgnl (Errors.print e); exit 1
-      end
-    | any -> begin msgnl (Errors.print any); exit 1 end
+    | UserError(_, s) as e ->
+      if is_empty s then exit 1
+      else fatal_error (Errors.print e) false
+    | any -> fatal_error (Errors.print any) (Errors.is_anomaly any)
 
 let init arglist =
+  init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   Lib.init();
   (* Default Proofb Mode starts with an alternative default. *)
   Goptions.set_string_option_value ["Default";"Proof";"Mode"] "Classic";
   begin
     try
-      let foreign_args = parse_args arglist in
-      if !filter_opts then
-        (print_string (String.concat "\n" foreign_args); exit 0);
-      if !ide_slave then begin
-        Flags.make_silent true;
-        Ide_slave.init_stdout ()
+      let extras = parse_args arglist in
+      (* If we have been spawned by the Spawn module, this has to be done
+       * early since the master waits us to connect back *)
+      Spawned.init_channels ();
+      Envars.set_coqlib Errors.error;
+      if !print_where then (print_endline(Envars.coqlib ()); exit(exitcode ()));
+      if !print_config then (Usage.print_config (); exit (exitcode ()));
+      if !print_tags then (print_style_tags (); exit (exitcode ()));
+      if !filter_opts then (print_string (String.concat "\n" extras); exit 0);
+      init_load_path ();
+      Option.iter Mltop.load_ml_object_raw !toploop;
+      let extras = !toploop_init extras in
+      if not (List.is_empty extras) then begin
+        prerr_endline ("Don't know what to do with "^String.concat " " extras);
+        prerr_endline "See -help for the list of supported options";
+        exit 1
       end;
       if_verbose print_header ();
-      init_load_path ();
       inputstate ();
       Mltop.init_known_plugins ();
       set_vm_opt ();
       engage ();
+      set_hierarchy ();
       (* Be careful to set these variables after the inputstate *)
       Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
       Syntax_def.set_compat_notations (not !no_compat_ntn);
-      if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
-        Option.iter Declaremods.start_library !toplevel_name;
+      if (not !batch_mode || List.is_empty !compile_list)
+         && Global.env_is_initial ()
+      then Option.iter Declaremods.start_library !toplevel_name;
       init_library_roots ();
       load_vernac_obj ();
       require ();
+      Stm.init ();
       load_rcfile();
       load_vernacular ();
       compile_files ();
+      schedule_vio_checking ();
+      schedule_vio_compilation ();
+      check_vio_tasks ();
       outputstate ()
     with any ->
+      let any = Errors.push any in
       flush_all();
-      if not !batch_mode then message "Error during initialization:";
-      msgnl (Toplevel.print_toplevel_error any);
-      exit 1
+      let msg =
+        if !batch_mode then mt ()
+        else str "Error during initialization:" ++ fnl ()
+      in
+      fatal_error (msg ++ Coqloop.print_toplevel_error any) (Errors.is_anomaly (fst any))
   end;
-  if !batch_mode then
-    (flush_all();
-     if !output_context then
-       Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
-     Profile.print_profile ();
-     exit 0);
-  (* We initialize the command history stack with a first entry *)
-  Backtrack.mark_command Vernacexpr.VernacNop
+  if !batch_mode then begin
+    flush_all();
+    if !output_context then
+      Pp.ppnl (with_option raw_print Prettyp.print_full_pure_context ());
+    Profile.print_profile ();
+    exit 0
+  end
 
 let init_toplevel = init
 
 let start () =
-  init_toplevel (List.tl (Array.to_list Sys.argv));
-  if !ide_slave then
-    Ide_slave.loop ()
-  else
-    Toplevel.loop();
-  (* Initialise and launch the Ocaml toplevel *)
-  Coqinit.init_ocaml_path();
-  Mltop.ocaml_toploop();
+  let () = init_toplevel (List.tl (Array.to_list Sys.argv)) in
+  (* In batch mode, Coqtop has already exited at this point. In interactive one,
+     dump glob is nothing but garbage ...  *)
+  !toploop_run ();
   exit 1
 
 (* [Coqtop.start] will be called by the code produced by coqmktop *)