[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)

We move delicate library/module instillation code to the STM so the
API guarantees that the first state snapshot is correct. That was not
the case in the past, which meant that the STM cache was unsound in
batch mode, however we never used its contents due to not backtracking
to the first state.

This provides quite an improvement in the API, however more work is
needed until the codepath is fully polished.

This is a critical step towards handling the STM functionally.

10 files changed, 298 insertions, 213 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index a178eb755..a53a866ab 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -42,7 +42,6 @@ let with_extra_values o l f x =
     Exninfo.iraise reraise
 
 let boot = ref false
-let load_init = ref true
 
 let record_aux_file = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 8ec2a8073..5233e72a2 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -11,7 +11,6 @@
 (** Command-line flags  *)
 
 val boot : bool ref
-val load_init : bool ref
 
 (** Set by coqtop to tell the kernel to output to the aux file; will
     be eventually removed by cleanups such as PR#1103 *)
diff --git a/stm/stm.ml b/stm/stm.ml
index 220ed9be4..770ccf22d 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -250,8 +250,8 @@ end (* }}} *)
 
 (* The main document type associated to a VCS *)
 type stm_doc_type =
-  | VoDoc       of Names.DirPath.t
-  | VioDoc      of Names.DirPath.t
+  | VoDoc       of string
+  | VioDoc      of string
   | Interactive of Names.DirPath.t
 
 (* Dummy until we land the functional interp patch + fixed start_library *)
@@ -276,6 +276,9 @@ module VCS : sig
 
   val init : stm_doc_type -> id -> doc
   (* val get_type : unit -> stm_doc_type *)
+  val set_ldir : Names.DirPath.t -> unit
+  val get_ldir : unit -> Names.DirPath.t
+
   val is_interactive : unit -> [`Yes | `No | `Shallow]
   val is_vio_doc : unit -> bool
 
@@ -460,6 +463,7 @@ end = struct (* {{{ *)
   let vcs : vcs ref = ref (empty Stateid.dummy)
 
   let doc_type = ref (Interactive (Names.DirPath.make []))
+  let ldir = ref Names.DirPath.empty
 
   let init dt id =
     doc_type := dt;
@@ -467,6 +471,10 @@ end = struct (* {{{ *)
     vcs := set_info !vcs id (default_info ());
     dummy_doc
 
+  let set_ldir ld =
+    ldir := ld
+
+  let get_ldir () = !ldir
   (* let get_type () = !doc_type *)
 
   let is_interactive () =
@@ -697,7 +705,7 @@ let state_of_id ~doc id =
 
 (****** A cache: fills in the nodes of the VCS document with their value ******)
 module State : sig
-  
+
   (** The function is from unit, so it uses the current state to define
       a new one.  I.e. one may been to install the right state before
       defining a new one.
@@ -713,7 +721,6 @@ module State : sig
   val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
   val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
 
-
   val exn_on : Stateid.t -> valid:Stateid.t -> Exninfo.iexn -> Exninfo.iexn
   (* to send states across worker/master *)
   type frozen_state
@@ -727,9 +734,15 @@ module State : sig
   val proof_part_of_frozen : frozen_state -> proof_part
   val assign : Stateid.t -> partial_state -> unit
 
+  (* Handlers for initial state, prior to document creation. *)
+  val register_root_state : unit -> unit
+  val restore_root_state : unit -> unit
+
   (* Only for internal use to catch problems in parse_sentence, should
      be removed in the state handling refactoring.  *)
   val cur_id : Stateid.t ref
+
+
 end = struct (* {{{ *)
 
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
@@ -879,6 +892,15 @@ end = struct (* {{{ *)
       Hooks.(call unreachable_state id ie);
       Exninfo.iraise ie
 
+  let init_state = ref None
+
+  let register_root_state () =
+    init_state := Some (freeze_global_state `No)
+
+  let restore_root_state () =
+    cur_id := Stateid.dummy;
+    unfreeze_global_state Option.(get !init_state)
+
 end (* }}} *)
 
 (* indentation code for Show Script, initially contributed
@@ -2365,19 +2387,55 @@ end (* }}} *)
 
 type stm_init_options = {
   doc_type     : stm_doc_type;
+  require_libs : (string * string option * bool option) list;
 (*
   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 } =
+(*
+let doc_type_module_name (std : stm_doc_type) =
+  match std with
+  | VoDoc mn | VioDoc mn | Vio2Vo mn -> mn
+  | Interactive mn -> Names.DirPath.to_string mn
+*)
+
+let init_core () =
+  State.register_root_state ()
+
+let new_doc { doc_type ; require_libs } =
+  let load_objs libs =
+    let rq_file (dir, from, exp) =
+      let mp = Libnames.(Qualid (Loc.tag @@ qualid_of_string dir)) in
+      let mfrom = Option.map (fun fr -> Libnames.(Qualid (Loc.tag @@ qualid_of_string fr))) from in
+      Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
+    List.(iter rq_file (rev libs))
+  in
+
+  (* We must reset the whole state before creating a document! *)
+  State.restore_root_state ();
+
   let doc = VCS.init doc_type Stateid.initial in
   set_undo_classifier Backtrack.undo_vernac_classifier;
-  (* we declare the library here XXX: *)
-  State.define ~cache:`Yes (fun () -> ()) Stateid.initial;
+
+  begin match doc_type with
+  | Interactive ln ->
+    Declaremods.start_library ln
+  | VoDoc ln ->
+    let ldir = Flags.verbosely Library.start_library ln in
+    VCS.set_ldir ldir;
+    set_compilation_hints ln
+  | VioDoc ln ->
+    let ldir = Flags.verbosely Library.start_library ln in
+    VCS.set_ldir ldir;
+    set_compilation_hints ln
+  end;
+  load_objs require_libs;
+
+  (* We record the state here! *)
+  State.define ~cache:`Yes ~redefine:true (fun () -> ()) Stateid.initial;
   Backtrack.record ();
   Slaves.init ();
   if Flags.async_proofs_is_master () then begin
@@ -2393,7 +2451,7 @@ let init { doc_type } =
         (Str.split_delim (Str.regexp ";") (Str.replace_first env_opt "" env))
     with Not_found -> () end;
   end;
-  doc
+  doc, VCS.cur_tip ()
 
 let observe ~doc id =
   let vcs = VCS.backup () in
@@ -2456,6 +2514,7 @@ let check_task name (tasks,rcbackup) i =
     rc
   with e when CErrors.noncritical e -> VCS.restore vcs; false
 let info_tasks (tasks,_) = Slaves.info_tasks tasks
+
 let finish_tasks name u d p (t,rcbackup as tasks) =
   RemoteCounter.restore rcbackup;
   let finish_task u (_,_,i) =
@@ -2953,6 +3012,7 @@ let edit_at ~doc id =
         Exninfo.iraise (e, info)
 
 let get_current_state ~doc = VCS.cur_tip ()
+let get_ldir ~doc = VCS.get_ldir ()
 
 let get_doc did = dummy_doc
 
diff --git a/stm/stm.mli b/stm/stm.mli
index 47963e5d8..c65cf6a9a 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -13,17 +13,17 @@ open Names
 (** 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
+  | VoDoc       of string
+  | VioDoc      of string
   | Interactive of DirPath.t
 
 (* Main initalization routine *)
 type stm_init_options = {
   doc_type     : stm_doc_type;
+  require_libs : (string * string option * bool option) list;
 (*
   fb_handler   : Feedback.feedback -> unit;
   iload_path   : (string list * string * bool) list;
-  require_libs : (Names.DirPath.t * string * bool option) list;
   implicit_std : bool;
 *)
 }
@@ -31,7 +31,10 @@ type stm_init_options = {
 (** The type of a STM document *)
 type doc
 
-val init : stm_init_options -> doc
+val init_core : unit -> unit
+
+(* Starts a new document *)
+val new_doc  : stm_init_options -> doc * Stateid.t
 
 (* [parse_sentence sid pa] Reads a sentence from [pa] with parsing
    state [sid] Returns [End_of_input] if the stream ends *)
@@ -105,6 +108,7 @@ val finish_tasks : string ->
 
 (* Id of the tip of the current branch *)
 val get_current_state : doc:doc -> Stateid.t
+val get_ldir : doc:doc -> Names.DirPath.t
 
 (* This returns the node at that position *)
 val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_expr Loc.located) option
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index bf22c16cd..c80899288 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -59,9 +59,9 @@ let load_rcfile doc sid =
      doc, sid)
 
 (* Recursively puts dir in the LoadPath if -nois was not passed *)
-let add_stdlib_path ~unix_path ~coq_root ~with_ml =
+let add_stdlib_path ~load_init ~unix_path ~coq_root ~with_ml =
   let add_ml = if with_ml then Mltop.AddRecML else Mltop.AddNoML in
-  Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:(!Flags.load_init)
+  Mltop.add_rec_path add_ml ~unix_path ~coq_root ~implicit:load_init
 
 let add_userlib_path ~unix_path =
   Mltop.add_rec_path Mltop.AddRecML ~unix_path
@@ -75,7 +75,7 @@ let ml_includes = ref []
 let push_ml_include s = ml_includes := s :: !ml_includes
 
 (* Initializes the LoadPath *)
-let init_load_path () =
+let init_load_path ~load_init =
   let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in
@@ -93,9 +93,9 @@ let init_load_path () =
     if System.exists_dir (coqlib/"toploop") then
       Mltop.add_ml_dir (coqlib/"toploop");
     (* then standard library *)
-    add_stdlib_path ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
+    add_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_root ~with_ml:false;
     (* then plugins *)
-    add_stdlib_path ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true;
+    add_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_root ~with_ml:true;
     (* then user-contrib *)
     if Sys.file_exists user_contrib then
       add_userlib_path ~unix_path:user_contrib;
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 2c275a00d..60ed698b8 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -20,6 +20,6 @@ val push_include : string -> Names.DirPath.t -> bool -> unit
 
 val push_ml_include : string -> unit
 
-val init_load_path : unit -> unit
+val init_load_path : load_init:bool -> unit
 
 val init_ocaml_path : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 9b58c9a65..e9fdaac5b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -188,11 +188,9 @@ let load_vernacular doc sid =
 	Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s)
     (doc, sid) (List.rev !load_vernacular_list)
 
-let load_vernacular_obj = ref ([] : string list)
-let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
-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)
+let load_init_vernaculars doc sid =
+  let doc, sid = Coqinit.load_rcfile doc sid in
+  load_vernacular doc sid
 
 (******************************************************************************)
 (* Required Modules                                                           *)
@@ -201,26 +199,23 @@ 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
-  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)
+(* None = No Import; Some false = Import; Some true = Export *)
+let require_list = ref ([] : (string * string option * bool option) list)
 let add_require s = require_list := s :: !require_list
-let require () =
-  let () = if !Flags.load_init then Flags.silently require_prelude () in
-  let map dir = Qualid (Loc.tag @@ qualid_of_string dir) in
-  Vernacentries.vernac_require None (Some false) (List.rev_map map !require_list)
+
+let load_init = ref true
+
+(* From Coq Require Import Prelude. *)
+let prelude_data = "Prelude", Some "Coq", Some true
+
+let require_libs () =
+  if !load_init then prelude_data :: !require_list else !require_list
 
 let add_compat_require v =
   match v with
-  | Flags.V8_5 -> add_require "Coq.Compat.Coq85"
-  | Flags.V8_6 -> add_require "Coq.Compat.Coq86"
-  | Flags.V8_7 -> add_require "Coq.Compat.Coq87"
+  | Flags.V8_5 -> add_require ("Coq.Compat.Coq85", None, Some false)
+  | Flags.V8_6 -> add_require ("Coq.Compat.Coq86", None, Some false)
+  | Flags.V8_7 -> add_require ("Coq.Compat.Coq87", None, Some false)
   | Flags.VOld | Flags.Current -> ()
 
 (******************************************************************************)
@@ -230,9 +225,9 @@ let add_compat_require v =
 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
+type compilation_mode = BuildVo | BuildVio | Vio2Vo
+let compilation_mode = ref BuildVo
 let compilation_output_name = ref None
 
 let batch_mode = ref false
@@ -253,21 +248,140 @@ let add_compile verbose s =
   in
   compile_list := (verbose,s) :: !compile_list
 
-let compile_file mode doc (verbosely,f_in) =
+let warn_file_no_extension =
+  CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
+         (fun (f,ext) ->
+          str "File \"" ++ str f ++
+            strbrk "\" has been implicitly expanded to \"" ++
+            str f ++ str ext ++ str "\"")
+
+let ensure_ext ext f =
+  if Filename.check_suffix f ext then f
+  else begin
+    warn_file_no_extension (f,ext);
+    f ^ ext
+  end
+
+let chop_extension f =
+  try Filename.chop_extension f with _ -> f
+
+let compile_error msg =
+  Topfmt.std_logger Feedback.Error msg;
+  flush_all ();
+  exit 1
+
+let ensure_bname src tgt =
+  let src, tgt = Filename.basename src, Filename.basename tgt in
+  let src, tgt = chop_extension src, chop_extension tgt in
+  if src <> tgt then
+    compile_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
+                   str "Source: " ++ str src                                                ++ fnl () ++
+                   str "Target: " ++ str tgt)
+
+let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
+
+let ensure_v v = ensure ".v" v v
+let ensure_vo v vo = ensure ".vo" v vo
+let ensure_vio v vio = ensure ".vio" v vio
+
+let ensure_exists f =
+  if not (Sys.file_exists f) then
+    compile_error (hov 0 (str "Can't find file" ++ spc () ++ str f))
+
+(* Compile a vernac file *)
+let compile ~verbosely ~f_in ~f_out =
+  let check_pending_proofs () =
+    let pfs = Proof_global.get_all_proof_names () in
+    if not (CList.is_empty pfs) then
+      compile_error (str "There are pending proofs: "
+                    ++ (pfs
+                        |> List.rev
+                        |> prlist_with_sep pr_comma Names.Id.print)
+                    ++ str ".")
+  in
+  match !compilation_mode with
+  | BuildVo ->
+      Flags.record_aux_file := true;
+      let long_f_dot_v = ensure_v f_in in
+      ensure_exists long_f_dot_v;
+      let long_f_dot_vo =
+        match f_out with
+        | None -> long_f_dot_v ^ "o"
+        | Some f -> ensure_vo long_f_dot_v f in
+
+      let doc, sid = Stm.(new_doc
+          { doc_type = VoDoc long_f_dot_vo;
+            require_libs = require_libs ()
+          }) in
+
+      let doc, sid = load_init_vernaculars doc sid in
+      let ldir = Stm.get_ldir ~doc in
+      Aux_file.(start_aux_file
+        ~aux_file:(aux_file_name_for long_f_dot_vo)
+        ~v_file:long_f_dot_v);
+      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 doc, _ = Vernac.load_vernac ~verbosely ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+      let _doc = Stm.join ~doc in
+      let wall_clock2 = Unix.gettimeofday () in
+      check_pending_proofs ();
+      Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
+      Aux_file.record_in_aux_at "vo_compile_time"
+        (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
+      Aux_file.stop_aux_file ();
+      Dumpglob.end_dump_glob ()
+  | BuildVio ->
+
+      Flags.record_aux_file := false;
+      Dumpglob.noglob ();
+
+      let long_f_dot_v = ensure_v f_in in
+      ensure_exists long_f_dot_v;
+
+      let long_f_dot_vio =
+        match f_out with
+        | None -> long_f_dot_v ^ "io"
+        | Some f -> ensure_vio long_f_dot_v f in
+
+      let doc, sid = Stm.(new_doc
+          { doc_type = VioDoc long_f_dot_vio;
+            require_libs = require_libs ()
+          }) in
+
+      let doc, sid = load_init_vernaculars doc sid in
+
+      let ldir = Stm.get_ldir ~doc in
+      let doc, _ = Vernac.load_vernac ~verbosely ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
+      let doc = Stm.finish ~doc in
+      check_pending_proofs ();
+      let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
+      Stm.reset_task_queue ()
+
+  | Vio2Vo ->
+      let open Filename in
+      Flags.record_aux_file := false;
+      Dumpglob.noglob ();
+      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
+      let univs, proofs = Stm.finish_tasks lfdv univs disch proofs tasks in
+      Library.save_library_raw lfdv sum lib univs proofs
+
+let compile ~verbosely ~f_in ~f_out =
+  ignore(CoqworkmgrApi.get 1);
+  compile ~verbosely ~f_in ~f_out;
+  CoqworkmgrApi.giveback 1
+
+let compile_file (verbosely,f_in) =
   if !Flags.beautify then
-    Flags.with_option Flags.beautify_file (fun f_in -> Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None) f_in
+    Flags.with_option Flags.beautify_file
+      (fun f_in -> compile ~verbosely ~f_in ~f_out:None) f_in
   else
-    Vernac.compile ~verbosely ~mode ~doc ~f_in ~f_out:None
+    compile ~verbosely ~f_in ~f_out:None
 
 let compile_files doc =
   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 mode doc vf)
-      (List.rev !compile_list)
+  else List.iter compile_file (List.rev !compile_list)
 
 (******************************************************************************)
 (* VIO Dispatching                                                            *)
@@ -279,7 +393,7 @@ let add_vio_task f =
   Flags.quiet := true;
   vio_tasks := f :: !vio_tasks
 
-let check_vio_tasks doc =
+let check_vio_tasks () =
   let rc =
     List.fold_left (fun acc t -> Vio_checking.check_vio t && acc)
       true (List.rev !vio_tasks) in
@@ -303,7 +417,7 @@ let set_vio_checking_j opt j =
     prerr_endline "setting the J variable like in 'make vio2vo J=3'";
     exit 1
 
-let schedule_vio_checking doc =
+let schedule_vio_checking () =
   if !vio_files <> [] && !vio_checking then
     Vio_checking.schedule_vio_checking !vio_files_j !vio_files
 
@@ -374,7 +488,7 @@ let usage batch =
   begin
   try
   Envars.set_coqlib ~fail:(fun x -> raise NoCoqLib);
-  Coqinit.init_load_path ();
+  Coqinit.init_load_path ~load_init:!load_init;
   with NoCoqLib -> usage_no_coqlib ()
   end;
   if batch then Usage.print_usage_coqc ()
@@ -563,20 +677,20 @@ let parse_args arglist =
     |"-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-object" -> add_require (next (), None, None)
     |"-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
     |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ())
-    |"-require" -> add_require (next ())
+    |"-require" -> add_require (next (), None, Some false)
     |"-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 ());
-      compilation_mode := Vernac.Vio2Vo
+      compilation_mode := Vio2Vo
     |"-toploop" -> set_toploop (next ())
     |"-w" | "-W" ->
       let w = next () in
@@ -609,7 +723,7 @@ let parse_args arglist =
     |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
     |"-m"|"--memory" -> memory_stat := true
-    |"-noinit"|"-nois" -> Flags.load_init := false
+    |"-noinit"|"-nois" -> load_init := false
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
     |"-native-compiler" ->
       if Coq_config.no_native_compiler then
@@ -621,11 +735,11 @@ let parse_args arglist =
     |"-quiet"|"-silent" -> Flags.quiet := true; Flags.make_warn false
     |"-quick" ->
       Safe_typing.allow_delayed_constants := true;
-      compilation_mode := Vernac.BuildVio
+      compilation_mode := BuildVio
     |"-list-tags" -> print_tags := true
     |"-time" -> Flags.time := true
     |"-type-in-type" -> set_type_in_type ()
-    |"-unicode" -> add_require "Utf8_core"
+    |"-unicode" -> add_require ("Utf8_core", None, Some false)
     |"-v"|"--version" -> Usage.version (exitcode ())
     |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ())
     |"-where" -> print_where := true
@@ -640,12 +754,18 @@ let parse_args arglist =
   with any -> fatal_error any
 
 let init_toplevel arglist =
+  (* Coq's init process, phase 1:
+     - OCaml parameters, and basic structures and IO
+   *)
   Profile.init_profile ();
   init_gc ();
   Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *)
   let init_feeder = Feedback.add_feeder coqtop_init_feed in
   Lib.init();
-  let doc = begin
+  (* Coq's init process, phase 2:
+     - Basic Coq environment, load-path, plugins.
+   *)
+  let res = begin
     try
       let extras = parse_args arglist in
       (* If we have been spawned by the Spawn module, this has to be done
@@ -656,7 +776,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);
-      Coqinit.init_load_path ();
+      Coqinit.init_load_path ~load_init:!load_init;
       Option.iter Mltop.load_ml_object_raw !toploop;
       let extras = !toploop_init extras in
       if not (CList.is_empty extras) then begin
@@ -665,52 +785,67 @@ let init_toplevel arglist =
         exit 1
       end;
       Flags.if_verbose print_header ();
-      inputstate ();
       Mltop.init_known_plugins ();
       engage ();
+
+      (* Allow the user to load an arbitrary state here *)
+      inputstate ();
+
+      (* This state will be shared by all the documents *)
+      Stm.init_core ();
+
+      (* Coq init process, phase 3: Stm initialization, backtracking state.
+
+         It is essential that the module system is in a consistent
+         state before we take the first snapshot. This was not
+         guaranteed in the past. In particular, we want to be sure we
+         have called start_library before loading the prelude and rest
+         of required files.
+
+         We split the codepath here depending whether coqtop is called
+         in interactive mode or not.  *)
+
       if (not !batch_mode || CList.is_empty !compile_list)
-         && Global.env_is_initial ()
-      then Declaremods.start_library !toplevel_name;
-      load_vernac_obj ();
-      require ();
-      let doc = Stm.(init { doc_type = Interactive Names.DirPath.empty }) in
-      let doc, sid = Coqinit.load_rcfile doc (Stm.get_current_state ~doc) in
-      (* XXX: We ignore this for now, but should be threaded to the toplevels *)
-      let doc, _sid = load_vernacular doc sid in
-      compile_files doc;
-      (* All these tasks use coqtop as a driver to invoke more coqtop,
-       * they should be really orthogonal to coqtop.
-       *)
-      schedule_vio_checking doc;
-      schedule_vio_compilation ();
-      check_vio_tasks doc;
-      outputstate ();
-      doc
+      (* Interactive *)
+      then begin
+        try
+          let doc, sid = Stm.(new_doc
+                                { doc_type = Interactive !toplevel_name;
+                                  require_libs = require_libs ()
+                                }) in
+          Some (load_init_vernaculars doc sid)
+        with any -> flush_all(); fatal_error any
+      (* Non interactive *)
+      end else begin
+        try
+          compile_files ();
+          schedule_vio_checking ();
+          schedule_vio_compilation ();
+          check_vio_tasks ();
+          (* Allow the user to output an arbitrary state *)
+          outputstate ();
+          None
+        with any -> flush_all(); fatal_error any
+      end;
     with any ->
       flush_all();
-      let extra = None
-        (* XXX: Must refine once Stm.init takes care of the start_library & friends *)
-        (* if !batch_mode && not Stateid.(equal (Stm.get_current_state ~doc) dummy) *)
-        (* then None *)
-        (* else Some (str "Error during initialization: ") *)
-      in
+      let extra = Some (str "Error during initialization: ") in
       fatal_error ?extra any
   end in
-  if !batch_mode then begin
+  Feedback.del_feeder init_feeder;
+  res
+
+let start () =
+  match init_toplevel (List.tl (Array.to_list Sys.argv)) with
+  (* Batch mode *)
+  | Some (doc, sid) when not !batch_mode ->
+    !toploop_run doc;
+    exit 1
+  | _ ->
     flush_all();
     if !output_context then
       Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
     Profile.print_profile ();
     exit 0
-  end;
-  Feedback.del_feeder init_feeder;
-  doc
-
-let start () =
-  let doc = 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 doc;
-  exit 1
 
 (* [Coqtop.start] will be called by the code produced by coqmktop *)
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 4c26a6ebc..1c7c3f944 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -11,7 +11,7 @@
    state, load the files given on the command line, load the resource file,
    produce the output state if any, and finally will launch [Coqloop.loop]. *)
 
-val init_toplevel : string list -> Stm.doc
+val init_toplevel : string list -> (Stm.doc * Stateid.t) option
 
 val start : unit -> unit
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 1e09a1c0d..d736975d3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -103,11 +103,6 @@ let pr_open_cur_subgoals () =
   try Printer.pr_open_subgoals ()
   with Proof_global.NoCurrentProof -> Pp.str ""
 
-let vernac_error msg =
-  Topfmt.std_logger Feedback.Error msg;
-  flush_all ();
-  exit 1
-
 (* Reenable when we get back to feedback printing *)
 (* let is_end_of_input any = match any with *)
 (*     Stm.End_of_input -> true *)
@@ -247,105 +242,3 @@ and load_vernac ~verbosely ~check ~interactive doc sid file =
 let process_expr doc sid loc_ast =
   checknav_deep loc_ast;
   interp_vernac ~interactive:true ~check:true doc sid loc_ast
-
-let warn_file_no_extension =
-  CWarnings.create ~name:"file-no-extension" ~category:"filesystem"
-         (fun (f,ext) ->
-          str "File \"" ++ str f ++
-            strbrk "\" has been implicitly expanded to \"" ++
-            str f ++ str ext ++ str "\"")
-
-let ensure_ext ext f =
-  if Filename.check_suffix f ext then f
-  else begin
-    warn_file_no_extension (f,ext);
-    f ^ ext
-  end
-
-let chop_extension f =
-  try Filename.chop_extension f with _ -> f
-
-let ensure_bname src tgt =
-  let src, tgt = Filename.basename src, Filename.basename tgt in
-  let src, tgt = chop_extension src, chop_extension tgt in
-  if src <> tgt then
-    vernac_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++
-                  str "Source: " ++ str src                                                ++ fnl () ++
-                  str "Target: " ++ str tgt)
-
-let ensure ext src tgt = ensure_bname src tgt; ensure_ext ext tgt
-
-let ensure_v v = ensure ".v" v v
-let ensure_vo v vo = ensure ".vo" v vo
-let ensure_vio v vio = ensure ".vio" v vio
-
-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 ~mode ~doc ~f_in ~f_out=
-  let check_pending_proofs () =
-    let pfs = Proof_global.get_all_proof_names () in
-    if not (List.is_empty pfs) then
-      vernac_error (str "There are pending proofs: "
-                    ++ (pfs
-                        |> List.rev
-                        |> prlist_with_sep pr_comma Names.Id.print)
-                    ++ str ".")
-  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 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
-      Stm.set_compilation_hints long_f_dot_vo;
-      Aux_file.(start_aux_file
-        ~aux_file:(aux_file_name_for long_f_dot_vo)
-        ~v_file:long_f_dot_v);
-      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 ~check:true ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
-      let _doc = Stm.join ~doc in
-      let wall_clock2 = Unix.gettimeofday () in
-      check_pending_proofs ();
-      Library.save_library_to ldir long_f_dot_vo (Global.opaque_tables ());
-      Aux_file.record_in_aux_at "vo_compile_time"
-        (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
-      Aux_file.stop_aux_file ();
-      Dumpglob.end_dump_glob ()
-  | BuildVio ->
-      let long_f_dot_v = ensure_v f_in in
-      ensure_exists long_f_dot_v;
-      let long_f_dot_vio =
-        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 ~check:false ~interactive:false doc (Stm.get_current_state ~doc) long_f_dot_v in
-      let doc = Stm.finish ~doc in
-      check_pending_proofs ();
-      let _doc = Stm.snapshot_vio ~doc ldir long_f_dot_vio in
-      Stm.reset_task_queue ()
-  | Vio2Vo ->
-      let open Filename in
-      Dumpglob.noglob ();
-      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 ~verbosely ~mode ~doc ~f_in ~f_out =
-  ignore(CoqworkmgrApi.get 1);
-  compile ~verbosely ~mode ~doc ~f_in ~f_out;
-  CoqworkmgrApi.giveback 1
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index d3a45ce9d..f9a430026 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -18,8 +18,3 @@ val process_expr : Stm.doc -> Stateid.t -> Vernacexpr.vernac_expr Loc.located ->
     echo the commands if [echo] is set. Callers are expected to handle
     and print errors in form of exceptions. *)
 val load_vernac : verbosely:bool -> check:bool -> interactive:bool -> Stm.doc -> Stateid.t -> string -> Stm.doc * Stateid.t
-
-type compilation_mode = BuildVo | BuildVio | Vio2Vo
-
-(** Compile a vernac file, (f is assumed without .v suffix) *)
-val compile : verbosely:bool -> mode:compilation_mode -> doc:Stm.doc -> f_in:string -> f_out:string option -> unit