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

1 files changed, 8 insertions, 4 deletions

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