[stm] [flags] Move document mode flags to the STM.

We move toplevel/STM flags from `Flags` to their proper components;
this ensures that low-level code doesn't depend on them, which was
incorrect and source of many problems wrt the interfaces.

Lower-level components should not be aware whether they are running in
batch or interactive mode, but instead provide a functional interface.

In particular:

== Added flags ==

- `Safe_typing.allow_delayed_constants`
  Allow delayed constants in the kernel.

- `Flags.record_aux_file`
  Output `Proof using` information from the kernel.

- `System.trust_file_cache`
  Assume that the file system won't change during our run.

== Deleted flags ==

- `Flags.compilation_mode`
- `Flags.batch_mode`

Additionally, we modify the STM entry point and `coqtop` to account
for the needed state. Note that testing may be necessary and the
number of combinations possible exceeds what the test-suite / regular
use does.

The next step is to fix the initialization problems [c.f. Bugzilla],
which will require a larger rework of the STM interface.

15 files changed, 255 insertions, 154 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ad622b07d..fd024b215 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -683,12 +683,15 @@ let build_module_body params restype senv =
     with one extra component and some updated fields
     (constraints, required, etc) *)
 
+let allow_delayed_constants = ref false
+
 let propagate_senv newdef newenv newresolver senv oldsenv =
   let now_cst, later_cst = List.partition Future.is_val senv.future_cst in
   (* This asserts that after Paral-ITP, standard vo compilation is behaving
    * exctly as before: the same universe constraints are added to modules *)
-  if !Flags.compilation_mode = Flags.BuildVo &&
-     !Flags.async_proofs_mode = Flags.APoff then assert(later_cst = []);
+  if not !allow_delayed_constants && later_cst <> [] then
+    CErrors.anomaly ~label:"safe_typing"
+      Pp.(str "True Future.t were created for opaque constants even if -async-proofs is off");
   { oldsenv with
     env = newenv;
     modresolver = newresolver;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 752fdd793..f0f273f35 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -158,6 +158,10 @@ val add_module_parameter :
   MBId.t -> Entries.module_struct_entry -> Declarations.inline ->
     Mod_subst.delta_resolver safe_transformer
 
+(** Traditional mode: check at end of module that no future was
+    created. *)
+val allow_delayed_constants : bool ref
+
 (** The optional result type is given without its functorial part *)
 
 val end_module :
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3f42c348f..0c0b910e1 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -428,13 +428,12 @@ let build_constant_declaration kn env result =
             let expr =
               !suggest_proof_using (Constant.to_string kn)
                 env vars ids_typ context_ids in
-            if !Flags.compilation_mode = Flags.BuildVo then
-              record_aux env ids_typ vars expr;
+            if !Flags.record_aux_file then record_aux env ids_typ vars expr;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
-        if !Flags.compilation_mode = Flags.BuildVo then
+        if !Flags.record_aux_file then
           record_aux env Id.Set.empty Id.Set.empty "";
         [], def (* Empty section context: no need to check *)
     | Some declared ->
@@ -614,7 +613,7 @@ let translate_local_def mb env id centry =
   let open Cooking in
   let decl = infer_declaration ~trust:mb env None (DefinitionEntry centry) in
   let typ = decl.cook_type in
-  if Option.is_empty decl.cook_context && !Flags.compilation_mode = Flags.BuildVo then begin
+  if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
     match decl.cook_body with
     | Undef _ -> ()
     | Def _ -> ()
diff --git a/lib/flags.ml b/lib/flags.ml
index d4be81c61..a178eb755 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -43,11 +43,8 @@ let with_extra_values o l f x =
 
 let boot = ref false
 let load_init = ref true
-let batch_mode = ref false
 
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-let compilation_mode = ref BuildVo
-let compilation_output_name = ref None
+let record_aux_file = ref false
 
 let test_mode = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 3024c6039..8ec2a8073 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -13,12 +13,9 @@
 val boot : bool ref
 val load_init : bool ref
 
-(* Will affect STM caching *)
-val batch_mode : bool ref
-
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-val compilation_mode : compilation_mode ref
-val compilation_output_name : string option ref
+(** Set by coqtop to tell the kernel to output to the aux file; will
+    be eventually removed by cleanups such as PR#1103 *)
+val record_aux_file : bool ref
 
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
diff --git a/lib/system.ml b/lib/system.ml
index 0b64b237d..4b5066ef4 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -54,6 +54,8 @@ let make_dir_table dir =
   let filter_dotfiles s f = if f.[0] = '.' then s else StrSet.add f s in
   Array.fold_left filter_dotfiles StrSet.empty (Sys.readdir dir)
 
+let trust_file_cache = ref true
+
 let exists_in_dir_respecting_case dir bf =
   let cache_dir dir =
     let contents = make_dir_table dir in
@@ -62,10 +64,10 @@ let exists_in_dir_respecting_case dir bf =
   let contents, fresh =
     try
       (* in batch mode, assume the directory content is still fresh *)
-      StrMap.find dir !dirmap, !Flags.batch_mode
+      StrMap.find dir !dirmap, !trust_file_cache
     with Not_found ->
       (* in batch mode, we are not yet sure the directory exists *)
-      if !Flags.batch_mode && not (exists_dir dir) then StrSet.empty, true
+      if !trust_file_cache && not (exists_dir dir) then StrSet.empty, true
       else cache_dir dir, true in
   StrSet.mem bf contents ||
     not fresh &&
@@ -80,7 +82,7 @@ let file_exists_respecting_case path f =
     let df = Filename.dirname f in
     (String.equal df "." || aux df)
     && exists_in_dir_respecting_case (Filename.concat path df) bf
-  in (!Flags.batch_mode || Sys.file_exists (Filename.concat path f)) && aux f
+  in (!trust_file_cache || Sys.file_exists (Filename.concat path f)) && aux f
 
 let rec search paths test =
   match paths with
diff --git a/lib/system.mli b/lib/system.mli
index 7281de97c..aa964abeb 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -54,6 +54,12 @@ val where_in_path_rex :
 val find_file_in_path :
   ?warn:bool -> CUnix.load_path -> string -> CUnix.physical_path * string
 
+val trust_file_cache : bool ref
+(** [trust_file_cache] indicates whether we trust the underlying
+    mapped file-system not to change along the execution of Coq. This
+    assumption greatly speds up file search, but it is often
+    inconvenient in interactive mode *)
+
 val file_exists_respecting_case : string -> string -> bool
 
 (** {6 I/O functions } *)
diff --git a/library/library.ml b/library/library.ml
index 1da2c591d..e2832ecdc 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -683,7 +683,8 @@ let error_recursively_dependent_library dir =
 let save_library_to ?todo dir f otab =
   let except = match todo with
     | None ->
-        assert(!Flags.compilation_mode = Flags.BuildVo);
+        (* XXX *)
+        (* assert(!Flags.compilation_mode = Flags.BuildVo); *)
         assert(Filename.check_suffix f ".vo");
         Future.UUIDSet.empty
     | Some (l,_) ->
diff --git a/stm/stm.ml b/stm/stm.ml
index 984a87429..2c5e9ed81 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -64,11 +64,6 @@ let call_process_error_once =
 
 end
 
-(* During interactive use we cache more states so that Undoing is fast *)
-let interactive () =
-  if !Flags.ide_slave || not !Flags.batch_mode then `Yes
-  else `No
-
 let async_proofs_workers_extra_env = ref [||]
 
 type aast = {
@@ -253,6 +248,12 @@ end (* }}} *)
 (*************************** THE DOCUMENT *************************************)
 (******************************************************************************)
 
+(* The main document type associated to a VCS *)
+type stm_doc_type =
+  | VoDoc       of Names.DirPath.t
+  | VioDoc      of Names.DirPath.t
+  | Interactive of Names.DirPath.t
+
 (* Imperative wrap around VCS to obtain _the_ VCS that is the
  * representation of the document Coq is currently processing *)
 module VCS : sig
@@ -269,7 +270,10 @@ module VCS : sig
 
   type vcs = (branch_type, transaction, vcs state_info, box) Vcs_.t
 
-  val init : id -> unit
+  val init : stm_doc_type -> id -> unit
+  (* val get_type : unit -> stm_doc_type *)
+  val is_interactive : unit -> [`Yes | `No | `Shallow]
+  val is_vio_doc : unit -> bool
 
   val current_branch : unit -> Branch.t
   val checkout : Branch.t -> unit
@@ -451,10 +455,25 @@ end = struct (* {{{ *)
   type vcs = (branch_type, transaction, vcs state_info, box) t
   let vcs : vcs ref = ref (empty Stateid.dummy)
 
-  let init id =
+  let doc_type = ref (Interactive (Names.DirPath.make []))
+
+  let init dt id =
+    doc_type := dt;
     vcs := empty id;
     vcs := set_info !vcs id (default_info ())
 
+  (* let get_type () = !doc_type *)
+
+  let is_interactive () =
+    match !doc_type with
+    | Interactive _ -> `Yes
+    | _ -> `No
+
+  let is_vio_doc () =
+    match !doc_type with
+    | VioDoc _ -> true
+    | _ -> false
+
   let current_branch () = current_branch !vcs
 
   let checkout head = vcs := checkout !vcs head
@@ -765,7 +784,7 @@ end = struct (* {{{ *)
     | { state = Error ie } -> cur_id := id; Exninfo.iraise ie 
     | _ ->
         (* coqc has a 1 slot cache and only for valid states *)
-        if interactive () = `No && Stateid.equal id !cur_id then ()
+        if VCS.is_interactive () = `No && Stateid.equal id !cur_id then ()
         else anomaly Pp.(str "installing a non cached state.")
 
   let get_cached id =
@@ -1054,7 +1073,7 @@ end = struct (* {{{ *)
              " the \"-async-proofs-cache force\" option to Coq."))
 
   let undo_vernac_classifier v =
-    if !Flags.batch_mode && !Flags.async_proofs_cache <> Some Flags.Force
+    if VCS.is_interactive () = `No && !Flags.async_proofs_cache <> Some Flags.Force
     then undo_costly_in_batch_mode v;
     try
       match v with
@@ -1106,7 +1125,7 @@ end = struct (* {{{ *)
           VtBack (true, oid), VtLater
       | VernacBacktrack (id,_,_)
       | VernacBackTo id ->
-          VtBack (not !Flags.batch_mode, Stateid.of_int id), VtNow
+          VtBack (VCS.is_interactive () = `Yes, Stateid.of_int id), VtNow
       | _ -> VtUnknown, VtNow
     with
     | Not_found ->
@@ -1364,7 +1383,7 @@ end = struct (* {{{ *)
   let build_proof_here ?loc ~drop_pt (id,valid) eop =
     Future.create (State.exn_on id ~valid) (fun () ->
       let wall_clock1 = Unix.gettimeofday () in
-      if !Flags.batch_mode then Reach.known_state ~cache:`No eop
+      if VCS.is_interactive () = `No then Reach.known_state ~cache:`No eop
       else Reach.known_state ~cache:`Shallow eop;
       let wall_clock2 = Unix.gettimeofday () in
       Aux_file.record_in_aux_at ?loc "proof_build_time"
@@ -1501,7 +1520,6 @@ end = struct (* {{{ *)
   module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask)
   
   let queue = ref None
-
   let init () =
     if Flags.async_proofs_is_master () then
       queue := Some (TaskQueue.create !Flags.async_proofs_n_workers)
@@ -1637,7 +1655,7 @@ end = struct (* {{{ *)
     let id, valid as t_exn_info = exn_info in
     let cancel_switch = ref false in
     if TaskQueue.n_workers (Option.get !queue) = 0 then
-      if !Flags.compilation_mode = Flags.BuildVio then begin
+      if VCS.is_vio_doc () then begin
         let f,assign =
          Future.create_delegate ~blocking:true ~name:pname (State.exn_on id ~valid) in
         let t_uuid = Future.uuid f in
@@ -1962,14 +1980,14 @@ let pstate = summary_pstate
 let async_policy () =
   let open Flags in
   if is_universe_polymorphism () then false
-  else if interactive () = `Yes then
+  else if VCS.is_interactive () = `Yes then
     (async_proofs_is_master () || !async_proofs_mode = APonLazy)
   else
-    (!compilation_mode = BuildVio || !async_proofs_mode <> APoff)
+    (VCS.is_vio_doc () || !async_proofs_mode <> APoff)
 
 let delegate name =
      get_hint_bp_time name >= !Flags.async_proofs_delegation_threshold
-  || !Flags.compilation_mode = Flags.BuildVio
+  || VCS.is_vio_doc ()
   || !Flags.async_proofs_full
  
 let warn_deprecated_nested_proofs =
@@ -2030,7 +2048,7 @@ let collect_proof keep cur hd brkind id =
         `ASync (parent last,accn,name,delegate name)
     | `Fork((_, hd', GuaranteesOpacity, ids), _) when
        has_proof_no_using last && not (State.is_cached_and_valid (parent last)) &&
-       !Flags.compilation_mode = Flags.BuildVio ->
+       VCS.is_vio_doc () ->
         assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
         (try
           let name, hint = name ids, get_hint_ctx loc  in
@@ -2339,9 +2357,20 @@ end (* }}} *)
 (********************************* STM API ************************************)
 (******************************************************************************)
 
-let init () =
-  VCS.init Stateid.initial;
+type stm_init_options = {
+  doc_type     : stm_doc_type;
+(*
+  fb_handler   : Feedback.feedback -> unit;
+  iload_path   : (string list * string * bool) list;
+  require_libs : (Names.DirPath.t * string * bool option) list;
+  implicit_std : bool;
+*)
+}
+
+let init { doc_type } =
+  VCS.init doc_type Stateid.initial;
   set_undo_classifier Backtrack.undo_vernac_classifier;
+  (* we declare the library here XXX: *)
   State.define ~cache:`Yes (fun () -> ()) Stateid.initial;
   Backtrack.record ();
   Slaves.init ();
@@ -2362,7 +2391,7 @@ let init () =
 let observe id =
   let vcs = VCS.backup () in
   try
-    Reach.known_state ~cache:(interactive ()) id;
+    Reach.known_state ~cache:(VCS.is_interactive ()) id;
     VCS.print ()
   with e ->
     let e = CErrors.push e in
@@ -2518,7 +2547,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
           stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
-          Reach.known_state ~cache:(interactive ()) id; `Ok
+          Reach.known_state ~cache:(VCS.is_interactive ()) id; `Ok
       | VtBack (false, id), VtLater ->
           anomaly(str"classifier: VtBack + VtLater must imply part_of_script.")
 
@@ -2536,7 +2565,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
           let id = VCS.new_node ~id:newtip () in
           let queue =
             if !Flags.async_proofs_full then `QueryQueue (ref false)
-            else if Flags.(!compilation_mode = BuildVio) &&
+            else if VCS.is_vio_doc () &&
                     VCS.((get_branch head).kind = `Master) &&
                     may_pierce_opaque x
                  then `SkipQueue
@@ -2626,7 +2655,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
           let step () =
             VCS.checkout VCS.Branch.master;
             let mid = VCS.get_branch_pos VCS.Branch.master in
-            Reach.known_state ~cache:(interactive ()) mid;
+            Reach.known_state ~cache:(VCS.is_interactive ()) mid;
             stm_vernac_interp id x;
             (* Vernac x may or may not start a proof *)
             if not in_proof && Proof_global.there_are_pending_proofs () then
@@ -2834,7 +2863,7 @@ let edit_at id =
       VCS.edit_branch (`Edit (mode, qed_id, master_id, keep, old_branch));
     VCS.delete_boxes_of id;
     cancel_switch := true;
-    Reach.known_state ~cache:(interactive ()) id;
+    Reach.known_state ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `Focus { stop = qed_id; start = master_id; tip } in
   let no_edit = function
@@ -2857,7 +2886,7 @@ let edit_at id =
     VCS.gc ();
     VCS.print ();
     if not !Flags.async_proofs_full then
-      Reach.known_state ~cache:(interactive ()) id;
+      Reach.known_state ~cache:(VCS.is_interactive ()) id;
     VCS.checkout_shallowest_proof_branch ();
     `NewTip in
   try
@@ -2886,7 +2915,7 @@ let edit_at id =
       | true, None, _ ->
           if on_cur_branch id then begin
             VCS.reset_branch (VCS.current_branch ()) id;
-            Reach.known_state ~cache:(interactive ()) id;
+            Reach.known_state ~cache:(VCS.is_interactive ()) id;
             VCS.checkout_shallowest_proof_branch ();
             `NewTip
           end else if is_ancestor_of_cur_branch id then begin
diff --git a/stm/stm.mli b/stm/stm.mli
index 3f01fca01..ea8aecaed 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -10,6 +10,26 @@ open Names
 
 (** state-transaction-machine interface *)
 
+(** The STM doc type determines some properties such as what
+    uncompleted proofs are allowed and recording of aux files. *)
+type stm_doc_type =
+  | VoDoc       of DirPath.t
+  | VioDoc      of DirPath.t
+  | Interactive of DirPath.t
+
+(* Main initalization routine *)
+type stm_init_options = {
+  doc_type     : stm_doc_type;
+(*
+  fb_handler   : Feedback.feedback -> unit;
+  iload_path   : (string list * string * bool) list;
+  require_libs : (Names.DirPath.t * string * bool option) list;
+  implicit_std : bool;
+*)
+}
+
+val init : stm_init_options -> unit
+
 (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
    state [sid] Returns [End_of_input] if the stream ends *)
 val parse_sentence : Stateid.t -> Pcoq.Gram.coq_parsable ->
@@ -83,9 +103,6 @@ val finish_tasks : string ->
 (* Id of the tip of the current branch *)
 val get_current_state : unit -> Stateid.t
 
-(* Misc *)
-val init : unit -> unit
-
 (* This returns the node at that position *)
 val get_ast : Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 1d5406770..8f676c656 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -32,7 +32,7 @@ let load_rcfile sid =
     try
       if !rcfile_specified then
         if CUnix.file_readable_p !rcfile then
-          Vernac.load_vernac false sid !rcfile
+          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid !rcfile
         else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
       else
 	try
@@ -43,7 +43,7 @@ let load_rcfile sid =
 	    Envars.home ~warn / "."^rcdefaultname^"."^Coq_config.version;
 	    Envars.home ~warn / "."^rcdefaultname
 	  ] in
-          Vernac.load_vernac false sid inferedrc
+          Vernac.load_vernac ~verbosely:false ~interactive:false ~check:true sid inferedrc
 	with Not_found -> sid
 	(*
 	Flags.if_verbose
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c159a1c6a..0624c9bed 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -9,7 +9,6 @@
 open Pp
 open CErrors
 open Libnames
-open Coqinit
 
 let () = at_exit flush_all
 
@@ -121,6 +120,14 @@ let print_memory_stat () =
 
 let _ = at_exit print_memory_stat
 
+(******************************************************************************)
+(* Deprecated                                                                 *)
+(******************************************************************************)
+let _remove_top_ml () = Mltop.remove ()
+
+(******************************************************************************)
+(* Engagement                                                                 *)
+(******************************************************************************)
 let impredicative_set = ref Declarations.PredicativeSet
 let set_impredicative_set c = impredicative_set := Declarations.ImpredicativeSet
 let set_type_in_type () =
@@ -129,14 +136,18 @@ let set_type_in_type () =
 let engage () =
   Global.set_engagement !impredicative_set
 
-let set_batch_mode () = Flags.batch_mode := true
-
+(******************************************************************************)
+(* Interactive toplevel name                                                  *)
+(******************************************************************************)
 let toplevel_default_name = Names.(DirPath.make [Id.of_string "Top"])
 let toplevel_name = ref toplevel_default_name
 let set_toplevel_name dir =
   if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name");
   toplevel_name := dir
 
+(******************************************************************************)
+(* Input/Output State                                                         *)
+(******************************************************************************)
 let warn_deprecated_inputstate =
   CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated"
          (fun () -> strbrk "The inputstate option is deprecated and discouraged.")
@@ -164,21 +175,22 @@ let outputstate () =
     let fname = CUnix.make_suffix !outputstate ".coq" in
     States.extern_state fname
 
-let set_include d p implicit =
-  let p = dirpath_of_string p in
-  push_include d p implicit
-
+(******************************************************************************)
+(* Interactive Load File Simulation                                           *)
+(******************************************************************************)
 let load_vernacular_list = ref ([] : (string * bool) list)
+
 let add_load_vernacular verb s =
   load_vernacular_list := ((CUnix.make_suffix s ".v"),verb) :: !load_vernacular_list
+
 let load_vernacular sid =
   List.fold_left
-    (fun sid (s,v) ->
-      let s = Loadpath.locate_file s in
+    (fun sid (f_in, verbosely) ->
+      let s = Loadpath.locate_file f_in in
       if !Flags.beautify then
-	Flags.(with_option beautify_file (Vernac.load_vernac v sid) s)
+	Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid) f_in
       else
-	Vernac.load_vernac v sid s)
+	Vernac.load_vernac ~verbosely ~interactive:false ~check:true sid s)
     sid (List.rev !load_vernacular_list)
 
 let load_vernacular_obj = ref ([] : string list)
@@ -187,6 +199,13 @@ let load_vernac_obj () =
   let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in
   Vernacentries.vernac_require None None (List.rev_map map !load_vernacular_obj)
 
+(******************************************************************************)
+(* Required Modules                                                           *)
+(******************************************************************************)
+let set_include d p implicit =
+  let p = dirpath_of_string p in
+  Coqinit.push_include d p implicit
+
 let require_prelude () =
   let vo = Envars.coqlib () / "theories/Init/Prelude.vo" in
   let vio = Envars.coqlib () / "theories/Init/Prelude.vio" in
@@ -209,10 +228,23 @@ let add_compat_require v =
   | Flags.V8_7 -> add_require "Coq.Compat.Coq87"
   | Flags.VOld | Flags.Current -> ()
 
-let compile_list = ref ([] : (bool * string) list)
+(******************************************************************************)
+(* File Compilation                                                           *)
+(******************************************************************************)
 
 let glob_opt = ref false
 
+let compile_list = ref ([] : (bool * string) list)
+let _compilation_list : Stm.stm_doc_type list ref = ref []
+
+let compilation_mode = ref Vernac.BuildVo
+let compilation_output_name = ref None
+
+let batch_mode = ref false
+let set_batch_mode () =
+  System.trust_file_cache := false;
+  batch_mode := true
+
 let add_compile verbose s =
   set_batch_mode ();
   Flags.quiet := true;
@@ -226,21 +258,66 @@ let add_compile verbose s =
   in
   compile_list := (verbose,s) :: !compile_list
 
-let compile_file (v,f) =
+let compile_file mode (verbosely,f_in) =
   if !Flags.beautify then
-    Flags.(with_option beautify_file (Vernac.compile v) f)
+    Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~f_in ~f_out:None) f_in
   else
-    Vernac.compile v f
+    Vernac.compile ~verbosely ~mode ~f_in ~f_out:None
 
 let compile_files () =
   if !compile_list == [] then ()
   else
     let init_state = States.freeze ~marshallable:`No in
+    let mode = !compilation_mode in
     List.iter (fun vf ->
         States.unfreeze init_state;
-        compile_file vf)
+        compile_file mode vf)
       (List.rev !compile_list)
 
+(******************************************************************************)
+(* VIO Dispatching                                                            *)
+(******************************************************************************)
+
+let vio_tasks = ref []
+let add_vio_task f =
+  set_batch_mode ();
+  Flags.quiet := 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
+
+(* vio files *)
+let vio_files = ref []
+let vio_files_j = ref 0
+let vio_checking = ref false
+let add_vio_file f =
+  set_batch_mode ();
+  Flags.quiet := 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 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
+
+(******************************************************************************)
+(* UI Options                                                                 *)
+(******************************************************************************)
 (** Options for proof general *)
 
 let set_emacs () =
@@ -296,14 +373,15 @@ let usage_no_coqlib = CWarnings.create ~name:"usage-no-coqlib" ~category:"filesy
     (fun () -> Pp.str "cannot guess a path for Coq libraries; dynaminally loaded flags will not be mentioned")
 
 exception NoCoqLib
-let usage () =
+
+let usage batch =
   begin
   try
   Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib);
-  init_load_path ();
+  Coqinit.init_load_path ();
   with NoCoqLib -> usage_no_coqlib ()
   end;
-  if !Flags.batch_mode then Usage.print_usage_coqc ()
+  if batch 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$"));
@@ -389,47 +467,10 @@ let get_error_resilience opt = function
 
 let get_task_list s = List.map int_of_string (Str.split (Str.regexp ",") s)
 
-let vio_tasks = ref []
-
-let add_vio_task f =
-  set_batch_mode ();
-  Flags.quiet := 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.quiet := 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
@@ -464,7 +505,7 @@ let parse_args arglist =
     (* Complex options with many args *)
     |"-I"|"-include" ->
       begin match rem with
-      | d :: rem -> push_ml_include d; args := rem
+      | d :: rem -> Coqinit.push_ml_include d; args := rem
       | [] -> error_missing_arg opt
       end
     |"-Q" ->
@@ -522,7 +563,7 @@ let parse_args arglist =
     |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
     |"-feedback-glob" -> Dumpglob.feedback_glob ()
     |"-exclude-dir" -> System.exclude_directory (next ())
-    |"-init-file" -> set_rcfile (next ())
+    |"-init-file" -> Coqinit.set_rcfile (next ())
     |"-inputstate"|"-is" -> set_inputstate (next ())
     |"-load-ml-object" -> Mltop.dir_ml_load (next ())
     |"-load-ml-source" -> Mltop.dir_ml_use (next ())
@@ -537,7 +578,9 @@ let parse_args arglist =
     |"-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 := Flags.Vio2Vo
+    |"-vio2vo" ->
+      add_compile false (next ());
+      compilation_mode := Vernac.Vio2Vo
     |"-toploop" -> set_toploop (next ())
     |"-w" | "-W" ->
       let w = next () in
@@ -545,7 +588,7 @@ let parse_args arglist =
       else
         let w = CWarnings.get_flags () ^ "," ^ w in
         CWarnings.set_flags (CWarnings.normalize_flags_string w)
-    |"-o" -> Flags.compilation_output_name := Some (next())
+    |"-o" -> compilation_output_name := Some (next())
 
     (* Options with zero arg *)
     |"-async-queries-always-delegate"
@@ -557,15 +600,15 @@ let parse_args arglist =
     |"-batch" -> set_batch_mode ()
     |"-test-mode" -> Flags.test_mode := true
     |"-beautify" -> Flags.beautify := true
-    |"-boot" -> Flags.boot := true; no_load_rc ()
+    |"-boot" -> Flags.boot := true; Coqinit.no_load_rc ()
     |"-bt" -> Backtrace.record_backtrace true
     |"-color" -> set_color (next ())
     |"-config"|"--config" -> print_config := true
-    |"-debug" -> set_debug ()
+    |"-debug" -> Coqinit.set_debug ()
     |"-stm-debug" -> Flags.stm_debug := true
     |"-emacs" -> set_emacs ()
     |"-filteropts" -> filter_opts := true
-    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
+    |"-h"|"-H"|"-?"|"-help"|"--help" -> usage !batch_mode
     |"-ideslave" -> set_ideslave ()
     |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
@@ -578,9 +621,11 @@ let parse_args arglist =
       else Flags.native_compiler := true
     |"-output-context" -> output_context := true
     |"-profile-ltac" -> Flags.profile_ltac := true
-    |"-q" -> no_load_rc ()
+    |"-q" -> Coqinit.no_load_rc ()
     |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
-    |"-quick" -> Flags.compilation_mode := Flags.BuildVio
+    |"-quick" ->
+      Safe_typing.allow_delayed_constants := true;
+      compilation_mode := Vernac.BuildVio
     |"-list-tags" -> print_tags := true
     |"-time" -> Flags.time := true
     |"-type-in-type" -> set_type_in_type ()
@@ -615,7 +660,7 @@ let init_toplevel arglist =
       if !print_config then (Envars.print_config stdout Coq_config.all_src_dirs; 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 ();
+      Coqinit.init_load_path ();
       Option.iter Mltop.load_ml_object_raw !toploop;
       let extras = !toploop_init extras in
       if not (CList.is_empty extras) then begin
@@ -627,19 +672,19 @@ let init_toplevel arglist =
       inputstate ();
       Mltop.init_known_plugins ();
       engage ();
-      if (not !Flags.batch_mode || CList.is_empty !compile_list)
+      if (not !batch_mode || CList.is_empty !compile_list)
          && Global.env_is_initial ()
       then Declaremods.start_library !toplevel_name;
       load_vernac_obj ();
       require ();
-      (* XXX: This is incorrect in batch mode, as we will initialize
-         the STM before having done Declaremods.start_library, thus
-         state 1 is invalid. This bug was present in 8.5/8.6. *)
-      Stm.init ();
-      let sid  = load_rcfile (Stm.get_current_state ()) in
+      Stm.(init { doc_type = Interactive Names.DirPath.empty });
+      let sid  = Coqinit.load_rcfile (Stm.get_current_state ()) in
       (* XXX: We ignore this for now, but should be threaded to the toplevels *)
       let _sid = load_vernacular sid in
       compile_files ();
+      (* All these tasks use coqtop as a driver to invoke more coqtop,
+       * they should be really orthogonal to coqtop.
+       *)
       schedule_vio_checking ();
       schedule_vio_compilation ();
       check_vio_tasks ();
@@ -647,13 +692,13 @@ let init_toplevel arglist =
     with any ->
       flush_all();
       let extra =
-        if !Flags.batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
+        if !batch_mode && not Stateid.(equal (Stm.get_current_state ()) dummy)
         then None
         else Some (str "Error during initialization: ")
       in
       fatal_error ?extra any
   end;
-  if !Flags.batch_mode then begin
+  if !batch_mode then begin
     flush_all();
     if !output_context then
       Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 892d64d91..ac2be7e16 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -15,7 +15,6 @@ val init_toplevel : string list -> unit
 
 val start : unit -> unit
 
-
 (* For other toploops *)
 val toploop_init : (string list -> string list) ref
 val toploop_run : (unit -> unit) ref
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1b020bc87..cb89dc8ff 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -113,13 +113,13 @@ let vernac_error msg =
 (*     Stm.End_of_input -> true *)
 (*   | _ -> false *)
 
-let rec interp_vernac sid (loc,com) =
+let rec interp_vernac ~check ~interactive sid (loc,com) =
   let interp = function
     | VernacLoad (verbosely, fname) ->
 	let fname = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) fname in
         let fname = CUnix.make_suffix fname ".v" in
         let f = Loadpath.locate_file fname in
-        load_vernac verbosely sid f
+        load_vernac ~verbosely ~check ~interactive sid f
     | v ->
 
       (* XXX: We need to run this before add as the classification is
@@ -142,17 +142,16 @@ let rec interp_vernac sid (loc,com) =
       (* Main STM interaction *)
       if ntip <> `NewTip then
         anomaly (str "vernac.ml: We got an unfocus operation on the toplevel!");
+
       (* Due to bug #5363 we cannot use observe here as we should,
          it otherwise reveals bugs *)
       (* Stm.observe nsid; *)
-
-      let check_proof = Flags.(!compilation_mode = BuildVo || not !batch_mode) in
-      if check_proof then Stm.finish ();
+      if check then Stm.finish ();
 
       (* We could use a more refined criteria that depends on the
          vernac. For now we imitate the old approach and rely on the
          classification. *)
-      let print_goals = not !Flags.batch_mode && not !Flags.quiet &&
+      let print_goals = interactive && not !Flags.quiet &&
                         is_proof_step && Proof_global.there_are_pending_proofs () in
 
       if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ());
@@ -167,7 +166,7 @@ let rec interp_vernac sid (loc,com) =
     with reraise ->
       (* XXX: In non-interactive mode edit_at seems to do very weird
          things, so we better avoid it while we investigate *)
-      if not !Flags.batch_mode then ignore(Stm.edit_at sid);
+      if interactive then ignore(Stm.edit_at sid);
       let (reraise, info) = CErrors.push reraise in
       let info = begin
         match Loc.get_loc info with
@@ -176,7 +175,7 @@ let rec interp_vernac sid (loc,com) =
       end in iraise (reraise, info)
 
 (* Load a vernac file. CErrors are annotated with file and location *)
-and load_vernac verbosely sid file =
+and load_vernac ~verbosely ~check ~interactive sid file =
   let ft_beautify, close_beautify =
     if !Flags.beautify_file then
       let chan_beautify = open_out (file^beautify_suffix) in
@@ -217,7 +216,7 @@ and load_vernac verbosely sid file =
       Option.iter (vernac_echo ?loc) in_echo;
 
       checknav_simple (loc, ast);
-      let nsid = Flags.silently (interp_vernac !rsid) (loc, ast) in
+      let nsid = Flags.silently (interp_vernac ~check ~interactive !rsid) (loc, ast) in
       rsid := nsid
     done;
     !rsid
@@ -245,7 +244,7 @@ and load_vernac verbosely sid file =
 
 let process_expr sid loc_ast =
   checknav_deep loc_ast;
-  interp_vernac sid loc_ast
+  interp_vernac ~interactive:true ~check:true sid loc_ast
 
 let warn_file_no_extension =
   CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
@@ -282,8 +281,10 @@ let ensure_exists f =
   if not (Sys.file_exists f) then
     vernac_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
 
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+
 (* Compile a vernac file *)
-let compile verbosely f =
+let compile ~verbosely ~mode ~f_in ~f_out=
   let check_pending_proofs () =
     let pfs = Proof_global.get_all_proof_names () in
     if not (List.is_empty pfs) then
@@ -293,12 +294,12 @@ let compile verbosely f =
                         |> prlist_with_sep pr_comma Names.Id.print)
                     ++ str ".")
   in
-  match !Flags.compilation_mode with
-  | Flags.BuildVo ->
-      let long_f_dot_v = ensure_v f in
+  match mode with
+  | BuildVo ->
+      let long_f_dot_v = ensure_v f_in in
       ensure_exists long_f_dot_v;
       let long_f_dot_vo =
-        match !Flags.compilation_output_name with
+        match f_out with
         | None -> long_f_dot_v ^ "o"
         | Some f -> ensure_vo long_f_dot_v f in
       let ldir = Flags.verbosely Library.start_library long_f_dot_vo in
@@ -309,7 +310,7 @@ let compile verbosely f =
       Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo;
       Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
       let wall_clock1 = Unix.gettimeofday () in
-      let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in
+      let _ = load_vernac ~verbosely ~check:true ~interactive:false (Stm.get_current_state ()) long_f_dot_v in
       Stm.join ();
       let wall_clock2 = Unix.gettimeofday () in
       check_pending_proofs ();
@@ -318,32 +319,31 @@ let compile verbosely f =
         (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
       Aux_file.stop_aux_file ();
       Dumpglob.end_dump_glob ()
-  | Flags.BuildVio ->
-      let long_f_dot_v = ensure_v f in
+  | BuildVio ->
+      let long_f_dot_v = ensure_v f_in in
       ensure_exists long_f_dot_v;
       let long_f_dot_vio =
-        match !Flags.compilation_output_name with
+        match f_out with
         | None -> long_f_dot_v ^ "io"
         | Some f -> ensure_vio long_f_dot_v f in
       let ldir = Flags.verbosely Library.start_library long_f_dot_vio in
       Dumpglob.noglob ();
       Stm.set_compilation_hints long_f_dot_vio;
-      let _ = load_vernac verbosely (Stm.get_current_state ()) long_f_dot_v in
+      let _ = load_vernac ~verbosely ~check:false ~interactive:false (Stm.get_current_state ()) long_f_dot_v in
       Stm.finish ();
       check_pending_proofs ();
       Stm.snapshot_vio ldir long_f_dot_vio;
       Stm.reset_task_queue ()
-  | Flags.Vio2Vo ->
+  | Vio2Vo ->
       let open Filename in
-      let open Library in
       Dumpglob.noglob ();
-      let f = if check_suffix f ".vio" then chop_extension f else f in
-      let lfdv, sum, lib, univs, disch, tasks, proofs = load_library_todo f in
+      let f = if check_suffix f_in ".vio" then chop_extension f_in else f_in in
+      let lfdv, sum, lib, univs, disch, tasks, proofs = Library.load_library_todo f in
       Stm.set_compilation_hints lfdv;
       let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
       Library.save_library_raw lfdv sum lib univs proofs
 
-let compile v f =
+let compile ~verbosely ~mode ~f_in ~f_out =
   ignore(CoqworkmgrApi.get 1);
-  compile v f;
+  compile ~verbosely ~mode ~f_in ~f_out;
   CoqworkmgrApi.giveback 1
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index bccf560e1..410dcf0d4 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -17,7 +17,9 @@ val process_expr : Stateid.t -> Vernacexpr.vernac_expr Loc.located -> Stateid.t
 (** [load_vernac echo sid file] Loads [file] on top of [sid], will
     echo the commands if [echo] is set. Callers are expected to handle
     and print errors in form of exceptions. *)
-val load_vernac : bool -> Stateid.t -> string -> Stateid.t
+val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stateid.t -> string -> Stateid.t
+
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
 
 (** Compile a vernac file, (f is assumed without .v suffix) *)
-val compile : bool -> string -> unit
+val compile : verbosely:bool -> mode:compilation_mode -> f_in:string -> f_out:string option -> unit