[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.

2 files changed, 77 insertions, 13 deletions

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