Merge PR #13418: [sysinit] new component

Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: JasonGross

7 files changed, 173 insertions, 362 deletions

diff --git a/stm/dune b/stm/dune
index c369bd00fb..27d561334e 100644
--- a/stm/dune
+++ b/stm/dune
@@ -3,4 +3,4 @@
  (synopsis "Coq's Document Manager and Proof Checking Scheduler")
  (public_name coq.stm)
  (wrapped false)
- (libraries vernac))
+ (libraries sysinit))
diff --git a/stm/stm.ml b/stm/stm.ml
index 0b00524bd5..7de109e596 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -297,13 +297,11 @@ end (* }}} *)
 (*************************** THE DOCUMENT *************************************)
 (******************************************************************************)
 
-type interactive_top = TopLogical of DirPath.t | TopPhysical of string
-
 (* The main document type associated to a VCS *)
 type stm_doc_type =
   | VoDoc       of string
   | VioDoc      of string
-  | Interactive of interactive_top
+  | Interactive of Coqargs.top
 
 (* Dummy until we land the functional interp patch + fixed start_library *)
 type doc = int
@@ -517,7 +515,7 @@ end = struct (* {{{ *)
   type vcs = (branch_type, transaction, vcs state_info, box) t
   let vcs : vcs ref = ref (empty Stateid.dummy)
 
-  let doc_type = ref (Interactive (TopLogical (Names.DirPath.make [])))
+  let doc_type = ref (Interactive (Coqargs.TopLogical (Names.DirPath.make [])))
   let ldir = ref Names.DirPath.empty
 
   let init dt id ps =
@@ -801,6 +799,9 @@ let state_of_id ~doc id =
     | EmptyState | ParsingState _ -> `Valid None
   with VCS.Expired -> `Expired
 
+let () =
+  Stateid.set_is_valid (fun ~doc id -> state_of_id ~doc id <> `Expired)
+
 (****** A cache: fills in the nodes of the VCS document with their value ******)
 module State : sig
 
@@ -2305,37 +2306,13 @@ end (* }}} *)
 
 (** STM initialization options: *)
 
-type option_command =
-  | OptionSet of string option
-  | OptionAppend of string
-  | OptionUnset
-
-type injection_command =
-  | OptionInjection of (Goptions.option_name * option_command)
-  (** Set flags or options before the initial state is ready. *)
-  | RequireInjection of (string * string option * bool option)
-  (** Require libraries before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
-  (* -load-vernac-source interleaving is not supported yet *)
-  (* | LoadInjection of (string * bool) *)
-
 type stm_init_options =
   { doc_type : stm_doc_type
   (** The STM does set some internal flags differently depending on
      the specified [doc_type]. This distinction should disappear at
      some some point. *)
 
-  ; ml_load_path : CUnix.physical_path list
-  (** OCaml load paths for the document. *)
-
-  ; vo_load_path   : Loadpath.vo_path list
-  (** [vo] load paths for the document. Usually extracted from -R
-     options / _CoqProject *)
-
-  ; injections : injection_command list
+  ; injections : Coqargs.injection_command list
   (** Injects Require and Set/Unset commands before the initial
      state is ready *)
 
@@ -2352,68 +2329,17 @@ let doc_type_module_name (std : stm_doc_type) =
   | Interactive mn -> Names.DirPath.to_string mn
 *)
 
+let init_process stm_flags =
+  Spawned.init_channels ();
+  CoqworkmgrApi.(init stm_flags.AsyncOpts.async_proofs_worker_priority)
+
 let init_core () =
   if !cur_opt.async_proofs_mode = APon then Control.enable_thread_delay := true;
   if !Flags.async_proofs_worker_id = "master" then Partac.enable_par ~nworkers:!cur_opt.async_proofs_n_tacworkers;
   State.register_root_state ()
 
-let dirpath_of_file f =
-  let ldir0 =
-    try
-      let lp = Loadpath.find_load_path (Filename.dirname f) in
-      Loadpath.logical lp
-    with Not_found -> Libnames.default_root_prefix
-  in
-  let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in
-  let id = Id.of_string f in
-  let ldir = Libnames.add_dirpath_suffix ldir0 id in
-  ldir
-
-let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
-
-  let require_file (dir, from, exp) =
-    let mp = Libnames.qualid_of_string dir in
-    let mfrom = Option.map Libnames.qualid_of_string from in
-    Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
-
-  let interp_set_option opt v old =
-    let open Goptions in
-    let err expect =
-      let opt = String.concat " " opt in
-      let got = v in (* avoid colliding with Pp.v *)
-      CErrors.user_err
-        Pp.(str "-set: " ++ str opt ++
-            str" expects " ++ str expect ++
-            str" but got " ++ str got)
-    in
-    match old with
-    | BoolValue _ ->
-      let v = match String.trim v with
-        | "true" -> true
-        | "false" | "" -> false
-        | _ -> err "a boolean"
-      in
-      BoolValue v
-    | IntValue _ ->
-      let v = String.trim v in
-      let v = match int_of_string_opt v with
-        | Some _ as v -> v
-        | None -> if v = "" then None else err "an int"
-      in
-      IntValue v
-    | StringValue _ -> StringValue v
-    | StringOptValue _ -> StringOptValue (Some v) in
-
-  let set_option = let open Goptions in function
-      | opt, OptionUnset -> unset_option_value_gen ~locality:OptLocal opt
-      | opt, OptionSet None -> set_bool_option_value_gen ~locality:OptLocal opt true
-      | opt, OptionSet (Some v) -> set_option_value ~locality:OptLocal (interp_set_option opt) opt v
-      | opt, OptionAppend v -> set_string_option_append_value_gen ~locality:OptLocal opt v in
 
-  let handle_injection = function
-    | RequireInjection r -> require_file r
-    (* | LoadInjection l -> *)
-    | OptionInjection o -> set_option o in
+let new_doc { doc_type ; injections; stm_options } =
 
   (* Set the options from the new documents *)
   AsyncOpts.cur_opt := stm_options;
@@ -2423,37 +2349,27 @@ let new_doc { doc_type ; ml_load_path; vo_load_path; injections; stm_options } =
 
   let doc = VCS.init doc_type Stateid.initial (Vernacstate.Parser.init ()) in
 
-  (* Set load path; important, this has to happen before we declare
-     the library below as [Declaremods/Library] will infer the module
-     name by looking at the load path! *)
-  List.iter Mltop.add_ml_dir ml_load_path;
-  List.iter Loadpath.add_vo_path vo_load_path;
-
   Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff;
 
-  begin match doc_type with
-    | Interactive ln ->
-      let dp = match ln with
-        | TopLogical dp -> dp
-        | TopPhysical f -> dirpath_of_file f
-      in
-      Declaremods.start_library dp
+  let top =
+    match doc_type with
+    | Interactive top -> Coqargs.dirpath_of_top top
 
     | VoDoc f ->
-      let ldir = dirpath_of_file f in
-      let () = Flags.verbosely Declaremods.start_library ldir in
+      let ldir = Coqargs.(dirpath_of_top (TopPhysical f)) in
       VCS.set_ldir ldir;
-      set_compilation_hints f
+      set_compilation_hints f;
+      ldir
 
     | VioDoc f ->
-      let ldir = dirpath_of_file f in
-      let () = Flags.verbosely Declaremods.start_library ldir in
+      let ldir = Coqargs.(dirpath_of_top (TopPhysical f)) in
       VCS.set_ldir ldir;
-      set_compilation_hints f
-  end;
+      set_compilation_hints f;
+      ldir
+    in
 
-  (* Import initial libraries. *)
-  List.iter handle_injection injections;
+  (* Start this library and import initial libraries. *)
+  Coqinit.start_library ~top injections;
 
   (* We record the state at this point! *)
   State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
diff --git a/stm/stm.mli b/stm/stm.mli
index e0c33a309b..bd42359cea 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -42,32 +42,13 @@ module AsyncOpts : sig
 
 end
 
-type interactive_top = TopLogical of DirPath.t | TopPhysical of string
-
 (** The STM document type [stm_doc_type] determines some properties
    such as what uncompleted proofs are allowed and what gets recorded
    to aux files. *)
 type stm_doc_type =
   | VoDoc       of string       (* file path *)
   | VioDoc      of string       (* file path *)
-  | Interactive of interactive_top    (* module path *)
-
-type option_command =
-  | OptionSet of string option
-  | OptionAppend of string
-  | OptionUnset
-
-type injection_command =
-  | OptionInjection of (Goptions.option_name * option_command)
-  (** Set flags or options before the initial state is ready. *)
-  | RequireInjection of (string * string option * bool option)
-  (** Require libraries before the initial state is
-     ready. Parameters follow [Library], that is to say,
-     [lib,prefix,import_export] means require library [lib] from
-     optional [prefix] and [import_export] if [Some false/Some true]
-     is used.  *)
-  (* -load-vernac-source interleaving is not supported yet *)
-  (* | LoadInjection of (string * bool) *)
+  | Interactive of Coqargs.top    (* module path *)
 
 (** STM initialization options: *)
 type stm_init_options =
@@ -76,14 +57,7 @@ type stm_init_options =
      the specified [doc_type]. This distinction should disappear at
      some some point. *)
 
-  ; ml_load_path : CUnix.physical_path list
-  (** OCaml load paths for the document. *)
-
-  ; vo_load_path   : Loadpath.vo_path list
-  (** [vo] load paths for the document. Usually extracted from -R
-     options / _CoqProject *)
-
-  ; injections : injection_command list
+  ; injections : Coqargs.injection_command list
   (** Injects Require and Set/Unset commands before the initial
      state is ready *)
 
@@ -94,8 +68,10 @@ type stm_init_options =
 (** The type of a STM document *)
 type doc
 
-(** [init_core] performs some low-level initialization; should go away
-   in future releases. *)
+(** [init_process] performs some low-level initialization, call early *)
+val init_process : AsyncOpts.stm_opt -> unit
+
+(** [init_core] snapshorts the initial system state *)
 val init_core : unit -> unit
 
 (** [new_doc opt] Creates a new document with options [opt] *)
diff --git a/stm/stm.mllib b/stm/stm.mllib
index 831369625f..a77e0c79e7 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -3,10 +3,10 @@ Dag
 Vcs
 TQueue
 WorkerPool
-Vernac_classifier
 CoqworkmgrApi
 AsyncTaskQueue
 Partac
 Stm
+Stmargs
 ProofBlockDelimiter
 Vio_checking
diff --git a/stm/stmargs.ml b/stm/stmargs.ml
new file mode 100644
index 0000000000..e2c7649a8f
--- /dev/null
+++ b/stm/stmargs.ml
@@ -0,0 +1,140 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+let fatal_error exn =
+  Topfmt.(in_phase ~phase:ParsingCommandLine print_err_exn exn);
+  let exit_code = if (CErrors.is_anomaly exn) then 129 else 1 in
+  exit exit_code
+
+let set_worker_id opt s =
+  assert (s <> "master");
+  Flags.async_proofs_worker_id := s
+
+let get_host_port opt s =
+  match String.split_on_char ':' s with
+  | [host; portr; portw] ->
+    Some (Spawned.Socket(host, int_of_string portr, int_of_string portw))
+  | ["stdfds"] -> Some Spawned.AnonPipe
+  | _ ->
+    Coqargs.error_wrong_arg ("Error: host:portr:portw or stdfds expected after option "^opt)
+
+let get_error_resilience opt = function
+  | "on" | "all" | "yes" -> `All
+  | "off" | "no" -> `None
+  | s -> `Only (String.split_on_char ',' s)
+
+let get_priority opt s =
+  try CoqworkmgrApi.priority_of_string s
+  with Invalid_argument _ ->
+    Coqargs.error_wrong_arg ("Error: low/high expected after "^opt)
+
+let get_async_proofs_mode opt = let open Stm.AsyncOpts in function
+  | "no" | "off" -> APoff
+  | "yes" | "on" -> APon
+  | "lazy" -> APonLazy
+  | _ ->
+    Coqargs.error_wrong_arg ("Error: on/off/lazy expected after "^opt)
+
+let get_cache opt = function
+  | "force" -> Some Stm.AsyncOpts.Force
+  | _ ->
+    Coqargs.error_wrong_arg ("Error: force expected after "^opt)
+
+let parse_args ~init arglist : Stm.AsyncOpts.stm_opt * string list =
+  let args = ref arglist in
+  let extras = ref [] in
+  let rec parse oval = match !args with
+  | [] ->
+    (oval, List.rev !extras)
+  | opt :: rem ->
+    args := rem;
+    let next () = match !args with
+      | x::rem -> args := rem; x
+      | [] -> Coqargs.error_missing_arg opt
+    in
+    let noval = begin match opt with
+
+    |"-async-proofs" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_mode = get_async_proofs_mode opt (next())
+      }
+    |"-async-proofs-j" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_n_workers = (Coqargs.get_int ~opt (next ()))
+      }
+    |"-async-proofs-cache" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_cache = get_cache opt (next ())
+      }
+
+    |"-async-proofs-tac-j" ->
+      let j = Coqargs.get_int ~opt (next ()) in
+      if j <= 0 then begin
+        Coqargs.error_wrong_arg ("Error: -async-proofs-tac-j only accepts values greater than or equal to 1")
+      end;
+      { oval with
+        Stm.AsyncOpts.async_proofs_n_tacworkers = j
+      }
+
+    |"-async-proofs-worker-priority" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_worker_priority = get_priority opt (next ())
+      }
+
+    |"-async-proofs-private-flags" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_private_flags = Some (next ());
+      }
+
+    |"-async-proofs-tactic-error-resilience" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_tac_error_resilience = get_error_resilience opt (next ())
+      }
+
+    |"-async-proofs-command-error-resilience" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_cmd_error_resilience = Coqargs.get_bool ~opt (next ())
+      }
+
+    |"-async-proofs-delegation-threshold" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_delegation_threshold = Coqargs.get_float ~opt (next ())
+      }
+
+    |"-worker-id" -> set_worker_id opt (next ()); oval
+
+    |"-main-channel" ->
+      Spawned.main_channel := get_host_port opt (next()); oval
+
+    |"-control-channel" ->
+      Spawned.control_channel := get_host_port opt (next()); oval
+
+    (* Options with zero arg *)
+    |"-async-queries-always-delegate"
+    |"-async-proofs-always-delegate"
+    |"-async-proofs-never-reopen-branch" ->
+      { oval with
+        Stm.AsyncOpts.async_proofs_never_reopen_branch = true
+      }
+    |"-stm-debug" -> Stm.stm_debug := true; oval
+    (* Unknown option *)
+    | s ->
+      extras := s :: !extras;
+      oval
+    end in
+    parse noval
+  in
+  try
+    parse init
+  with any -> fatal_error any
+
+let usage = "\
+\n  -stm-debug             STM debug mode (will trace every transaction)\
+"
diff --git a/stm/vernac_classifier.mli b/stm/stmargs.mli
index 61bf3a503a..f760afdc98 100644
--- a/stm/vernac_classifier.mli
+++ b/stm/stmargs.mli
@@ -8,12 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Vernacextend
+val parse_args : init:Stm.AsyncOpts.stm_opt -> string list -> Stm.AsyncOpts.stm_opt * string list
 
-val string_of_vernac_classification : vernac_classification -> string
-
-(** What does a vernacular do *)
-val classify_vernac : Vernacexpr.vernac_control -> vernac_classification
-
-(**  *)
-val stm_allow_nested_proofs_option_name : string list
+val usage : string
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
deleted file mode 100644
index ffae2866c0..0000000000
--- a/stm/vernac_classifier.ml
+++ /dev/null
@@ -1,215 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open CErrors
-open Util
-open Pp
-open CAst
-open Vernacextend
-open Vernacexpr
-
-let string_of_vernac_when = function
-  | VtLater -> "Later"
-  | VtNow -> "Now"
-
-let string_of_vernac_classification = function
-  | VtStartProof _ -> "StartProof"
-  | VtSideff (_,w) -> "Sideff"^" "^(string_of_vernac_when w)
-  | VtQed (VtKeep VtKeepAxiom) -> "Qed(admitted)"
-  | VtQed (VtKeep (VtKeepOpaque | VtKeepDefined)) -> "Qed(keep)"
-  | VtQed VtDrop -> "Qed(drop)"
-  | VtProofStep {  proof_block_detection } ->
-      "ProofStep " ^ Option.default "" proof_block_detection
-  | VtQuery -> "Query"
-  | VtMeta -> "Meta "
-  | VtProofMode _ -> "Proof Mode"
-
-let vtkeep_of_opaque = function
-  | Opaque -> VtKeepOpaque
-  | Transparent -> VtKeepDefined
-
-let idents_of_name : Names.Name.t -> Names.Id.t list =
-  function
-  | Names.Anonymous -> []
-  | Names.Name n -> [n]
-
-let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"]
-
-let options_affecting_stm_scheduling =
-  [ Attributes.universe_polymorphism_option_name;
-    stm_allow_nested_proofs_option_name;
-    Vernacinterp.proof_mode_opt_name;
-    Attributes.program_mode_option_name;
-    Proof_using.proof_using_opt_name;
-  ]
-
-let classify_vernac e =
-  let static_classifier ~atts e = match e with
-    (* Univ poly compatibility: we run it now, so that we can just
-     * look at Flags in stm.ml.  Would be nicer to have the stm
-     * look at the entire dag to detect this option. *)
-    | VernacSetOption (_, l,_)
-      when CList.exists (CList.equal String.equal l)
-        options_affecting_stm_scheduling ->
-       VtSideff ([], VtNow)
-    (* Qed *)
-    | VernacAbort _ -> VtQed VtDrop
-    | VernacEndProof Admitted -> VtQed (VtKeep VtKeepAxiom)
-    | VernacEndProof (Proved (opaque,_)) -> VtQed (VtKeep (vtkeep_of_opaque opaque))
-    | VernacExactProof _ -> VtQed (VtKeep VtKeepOpaque)
-    (* Query *)
-    | VernacShow _ | VernacPrint _ | VernacSearch _ | VernacLocate _
-    | VernacCheckMayEval _ -> VtQuery
-    (* ProofStep *)
-    | VernacProof _
-    | VernacFocus _ | VernacUnfocus
-    | VernacSubproof _
-    | VernacCheckGuard
-    | VernacUnfocused
-    | VernacSolveExistential _ ->
-        VtProofStep { proof_block_detection = None }
-    | VernacBullet _ ->
-        VtProofStep { proof_block_detection = Some "bullet" }
-    | VernacEndSubproof ->
-        VtProofStep { proof_block_detection = Some "curly" }
-    (* StartProof *)
-    | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) ->
-      VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i)
-
-    | VernacDefinition (_,({v=i},_),ProveBody _) ->
-      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
-      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof(guarantee, idents_of_name i)
-    | VernacStartTheoremProof (_,l) ->
-      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
-      let ids = List.map (fun (({v=i}, _), _) -> i) l in
-      let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-      VtStartProof (guarantee,ids)
-    | VernacFixpoint (discharge,l) ->
-      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
-       let guarantee =
-         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
-         else GuaranteesOpacity
-       in
-        let ids, open_proof =
-          List.fold_left (fun (l,b) {Vernacexpr.fname={CAst.v=id}; body_def} ->
-            id::l, b || body_def = None) ([],false) l in
-        if open_proof
-        then VtStartProof (guarantee,ids)
-        else VtSideff (ids, VtLater)
-    | VernacCoFixpoint (discharge,l) ->
-      let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
-       let guarantee =
-         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
-         else GuaranteesOpacity
-       in
-        let ids, open_proof =
-          List.fold_left (fun (l,b) { Vernacexpr.fname={CAst.v=id}; body_def } ->
-            id::l, b || body_def = None) ([],false) l in
-        if open_proof
-        then VtStartProof (guarantee,ids)
-        else VtSideff (ids, VtLater)
-    (* Sideff: apply to all open branches. usually run on master only *)
-    | VernacAssumption (_,_,l) ->
-        let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in
-        VtSideff (ids, VtLater)
-    | VernacPrimitive ((id,_),_,_) ->
-        VtSideff ([id.CAst.v], VtLater)
-    | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
-    | VernacInductive (_,l) ->
-        let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with
-        | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
-        | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
-           CList.map_filter (function
-            | AssumExpr({v=Names.Name n},_,_), _ -> Some n
-            | _ -> None) l) l in
-        VtSideff (List.flatten ids, VtLater)
-    | VernacScheme l ->
-        let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in
-        VtSideff (ids, VtLater)
-    | VernacCombinedScheme ({v=id},_) -> VtSideff ([id], VtLater)
-    | VernacBeginSection {v=id} -> VtSideff ([id], VtLater)
-    | VernacUniverse _ | VernacConstraint _
-    | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _
-    | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _
-    | VernacChdir _
-    | VernacCreateHintDb _ | VernacRemoveHints _ | VernacHints _
-    | VernacArguments _
-    | VernacReserve _
-    | VernacGeneralizable _
-    | VernacSetOpacity _ | VernacSetStrategy _
-    | VernacSetOption _
-    | VernacAddOption _ | VernacRemoveOption _
-    | VernacMemOption _ | VernacPrintOption _
-    | VernacGlobalCheck _
-    | VernacDeclareReduction _
-    | VernacExistingClass _ | VernacExistingInstance _
-    | VernacRegister _
-    | VernacNameSectionHypSet _
-    | VernacComments _
-    | VernacDeclareInstance _ -> VtSideff ([], VtLater)
-    (* Who knows *)
-    | VernacLoad _ -> VtSideff ([], VtNow)
-    (* (Local) Notations have to disappear *)
-    | VernacEndSegment _ -> VtSideff ([], VtNow)
-    (* Modules with parameters have to be executed: can import notations *)
-    | VernacDeclareModule (exp,{v=id},bl,_)
-    | VernacDefineModule (exp,{v=id},bl,_,_) ->
-        VtSideff ([id], if bl = [] && exp = None then VtLater else VtNow)
-    | VernacDeclareModuleType ({v=id},bl,_,_) ->
-        VtSideff ([id], if bl = [] then VtLater else VtNow)
-    (* These commands alter the parser *)
-    | VernacDeclareCustomEntry _
-    | VernacOpenCloseScope _ | VernacDeclareScope _
-    | VernacDelimiters _ | VernacBindScope _
-    | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
-    | VernacSyntaxExtension _
-    | VernacSyntacticDefinition _
-    | VernacRequire _ | VernacImport _ | VernacInclude _
-    | VernacDeclareMLModule _
-    | VernacContext _ (* TASSI: unsure *) -> VtSideff ([], VtNow)
-    | VernacProofMode pm -> VtProofMode pm
-    | VernacInstance ((name,_),_,_,props,_) ->
-      let program, refine =
-        Attributes.(parse_drop_extra Notations.(program ++ Classes.refine_att) atts)
-      in
-      if program || (props <> None && not refine) then
-        VtSideff (idents_of_name name.CAst.v, VtLater)
-      else
-        let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
-        let guarantee = if polymorphic then Doesn'tGuaranteeOpacity else GuaranteesOpacity in
-        VtStartProof (guarantee, idents_of_name name.CAst.v)
-    (* Stm will install a new classifier to handle these *)
-    | VernacBack _ | VernacAbortAll
-    | VernacUndoTo _ | VernacUndo _
-    | VernacResetName _ | VernacResetInitial
-    | VernacRestart -> VtMeta
-    (* What are these? *)
-    | VernacRestoreState _
-    | VernacWriteState _ -> VtSideff ([], VtNow)
-    (* Plugins should classify their commands *)
-    | VernacExtend (s,l) ->
-        try Vernacextend.get_vernac_classifier s l
-        with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
-  in
-  let static_control_classifier ({ CAst.v ; _ } as cmd) =
-    (* Fail Qed or Fail Lemma must not join/fork the DAG *)
-    (* XXX why is Fail not always Query? *)
-    if Vernacprop.has_Fail cmd then
-      (match static_classifier ~atts:v.attrs v.expr with
-         | VtQuery | VtProofStep _ | VtSideff _
-         | VtMeta as x -> x
-         | VtQed _ -> VtProofStep { proof_block_detection = None }
-         | VtStartProof _ | VtProofMode _ -> VtQuery)
-    else
-      static_classifier ~atts:v.attrs v.expr
-
-  in
-  static_control_classifier e