[vernac] Split vernacular translation and interpretation.

This allows UI clients to implement a different state management
strategy with regards to proofs, and in particular to override
`Vernacinterp.interp`.

This is work in progress towards having a true `VtTactic` which shall
not perform any state changes non-functionally, and actually removing
the series of `assert false` due to meta-vernacs.

6 files changed, 322 insertions, 298 deletions

diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 4868182bb3..03bf008529 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -32,10 +32,9 @@ ComFixpoint
 ComProgramFixpoint
 Record
 Assumptions
-Vernacstate
 Mltop
 Topfmt
 Loadpath
 Vernacentries
-
-Misctypes
+Vernacstate
+Vernacinterp
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bc47ad8699..40786fe0b4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -35,12 +35,6 @@ module NamedDecl = Context.Named.Declaration
 (** TODO: make this function independent of Ltac *)
 let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
-let debug = false
-
-(* XXX Should move to a common library *)
-let vernac_pperr_endline pp =
-  if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else ()
-
 (* Utility functions, at some point they should all disappear and
    instead enviroment/state selection should be done at the Vernac DSL
    level. *)
@@ -468,28 +462,6 @@ let vernac_notation ~atts =
 let vernac_custom_entry ~module_local s =
   Metasyntax.declare_custom_entry module_local s
 
-(* Default proof mode, to be set at the beginning of proofs for
-   programs that cannot be statically classified. *)
-let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
-let get_default_proof_mode () = !default_proof_mode
-
-let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode
-let set_default_proof_mode_opt name =
-  default_proof_mode :=
-    match Pvernac.lookup_proof_mode name with
-    | Some pm -> pm
-    | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))
-
-let proof_mode_opt_name = ["Default";"Proof";"Mode"]
-let () =
-  Goptions.declare_string_option Goptions.{
-    optdepr = false;
-    optname = "default proof mode" ;
-    optkey = proof_mode_opt_name;
-    optread = get_default_proof_mode_opt;
-    optwrite = set_default_proof_mode_opt;
-  }
-
 (***********)
 (* Gallina *)
 
@@ -2237,115 +2209,9 @@ let vernac_check_guard ~pstate =
       (str ("Condition violated: ") ++s)
   in message
 
-(** A global default timeout, controlled by option "Set Default Timeout n".
-    Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
-
-let default_timeout = ref None
-
-(* Timeout *)
-let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b =
-  match !default_timeout, timeout with
-  | _, Some n
-  | Some n, None ->
-    Control.timeout n f x Timeout
-  | None, None ->
-    f x
-
-(* Fail *)
-let test_mode = ref false
-
-(* Restoring the state is the caller's responsibility *)
-let with_fail f : (Pp.t, unit) result =
-  try
-    let _ = f () in
-    Error ()
-  with
-  (* Fail Timeout is a common pattern so we need to support it. *)
-  | e when CErrors.noncritical e || e = Timeout ->
-    (* The error has to be printed in the failing state *)
-    Ok CErrors.(iprint (push e))
-
-(* We restore the state always *)
-let with_fail ~st f =
-  let res = with_fail f in
-  Vernacstate.invalidate_cache ();
-  Vernacstate.unfreeze_interp_state st;
-  match res with
-  | Error () ->
-    user_err ~hdr:"Fail" (str "The command has not failed!")
-  | Ok msg ->
-    if not !Flags.quiet || !test_mode
-    then Feedback.msg_notice (str "The command has indeed failed with message:" ++ fnl () ++ msg)
-
-let locate_if_not_already ?loc (e, info) =
-  match Loc.get_loc info with
-  | None   -> (e, Option.cata (Loc.add_loc info) info loc)
-  | Some l -> (e, info)
-
-let mk_time_header =
-  (* Drop the time header to print the command, we should indeed use a
-     different mechanism to `-time` commands than the current hack of
-     adding a time control to the AST. *)
-  let pr_time_header vernac =
-    let vernac = match vernac with
-      | { v = { control = ControlTime _ :: control; attrs; expr }; loc } ->
-        CAst.make ?loc { control; attrs; expr }
-      | _ -> vernac
-    in
-    Topfmt.pr_cmd_header vernac
-  in
-  fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac)
-
-let interp_control_flag ~time_header (f : control_flag) ~st
-    (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) =
-  match f with
-  | ControlFail ->
-    with_fail ~st (fun () -> fn ~st);
-    st.Vernacstate.lemmas
-  | ControlTimeout timeout ->
-    vernac_timeout ~timeout (fun () -> fn ~st) ()
-  | ControlTime batch ->
-    let header = if batch then Lazy.force time_header  else Pp.mt () in
-    System.with_time ~batch ~header (fun () -> fn ~st) ()
-  | ControlRedirect s ->
-    Topfmt.with_output_to_file s (fun () -> fn ~st) ()
-
-(* EJGA: We may remove this, only used twice below *)
-let vernac_require_open_lemma ~stack f =
-  match stack with
-  | Some stack -> f stack
-  | None -> user_err Pp.(str "Command not supported (No proof-editing in progress)")
-
-let interp_typed_vernac c ~stack =
-  let open Vernacextend in
-  match c with
-  | VtDefault f -> f (); stack
-  | VtNoProof f ->
-    if Option.has_some stack then
-      user_err Pp.(str "Command not supported (Open proofs remain)");
-    let () = f () in
-    stack
-  | VtCloseProof f ->
-    vernac_require_open_lemma ~stack (fun stack ->
-        let lemma, stack = Vernacstate.LemmaStack.pop stack in
-        f ~lemma;
-        stack)
-  | VtOpenProof f ->
-    Some (Vernacstate.LemmaStack.push stack (f ()))
-  | VtModifyProof f ->
-    Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack
-  | VtReadProofOpt f ->
-    let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in
-    f ~pstate;
-    stack
-  | VtReadProof f ->
-    vernac_require_open_lemma ~stack
-      (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate));
-    stack
-
 (* We interpret vernacular commands to a DSL that specifies their
    allowed actions on proof states *)
-let rec translate_vernac ~atts v = let open Vernacextend in match v with
+let translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacAbortAll
   | VernacRestart
   | VernacUndo _
@@ -2355,6 +2221,9 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacBack _
   | VernacAbort _ ->
     anomaly (str "type_vernac")
+  | VernacLoad _ ->
+    anomaly (str "Load is not supported recursively")
+
   (* Syntax *)
   | VernacSyntaxExtension (infix, sl) ->
     VtDefault(fun () -> with_module_locality ~atts vernac_syntax_extension infix sl)
@@ -2656,141 +2525,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacEndProof pe ->
     VtCloseProof (vernac_end_proof pe)
 
-  | VernacLoad (verbosely,fname) ->
-    VtNoProof(fun () ->
-      unsupported_attributes atts;
-      vernac_load ~verbosely fname)
-
   (* Extensions *)
   | VernacExtend (opn,args) ->
     Vernacextend.type_vernac ~atts opn args
-
-(* "locality" is the prefix "Local" attribute, while the "local" component
- * is the outdated/deprecated "Local" attribute of some vernacular commands
- * still parsed as the obsolete_locality grammar entry for retrocompatibility.
- * loc is the Loc.t of the vernacular command being interpreted. *)
-and interp_expr ~atts ~st c =
-  let stack = st.Vernacstate.lemmas in
-  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
-  match c with
-
-  (* The STM should handle that, but LOAD bypasses the STM... *)
-  | VernacAbortAll    -> CErrors.user_err  (str "AbortAll cannot be used through the Load command")
-  | VernacRestart     -> CErrors.user_err  (str "Restart cannot be used through the Load command")
-  | VernacUndo _      -> CErrors.user_err  (str "Undo cannot be used through the Load command")
-  | VernacUndoTo _    -> CErrors.user_err  (str "UndoTo cannot be used through the Load command")
-
-  (* Resetting *)
-  | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm.")
-  | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
-  | VernacBack _       -> anomaly (str "VernacBack not handled by Stm.")
-
-  (* This one is possible to handle here *)
-  | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
-
-  | v ->
-    let fv = translate_vernac ~atts v in
-    interp_typed_vernac ~stack fv
-
-(* XXX: This won't properly set the proof mode, as of today, it is
-   controlled by the STM. Thus, we would need access information from
-   the classifier. The proper fix is to move it to the STM, however,
-   the way the proof mode is set there makes the task non trivial
-   without a considerable amount of refactoring.
-*)
-and vernac_load ~verbosely fname =
-  let exception End_of_input in
-
-  (* Note that no proof should be open here, so the state here is just token for now *)
-  let st = Vernacstate.freeze_interp_state ~marshallable:false in
-  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 input =
-    let longfname = Loadpath.locate_file fname in
-    let in_chan = open_utf8_file_in longfname in
-    Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
-  (* Parsing loop *)
-  let v_mod = if verbosely then Flags.verbosely else Flags.silently in
-  let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
-      (fun po ->
-         match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
-         | Some x -> x
-         | None -> raise End_of_input) in
-  let rec load_loop ~stack =
-    try
-      let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
-      let stack =
-        v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack })
-          (parse_sentence proof_mode input) in
-      load_loop ~stack
-    with
-      End_of_input ->
-      stack
-  in
-  let stack = load_loop ~stack:st.Vernacstate.lemmas in
-  (* If Load left a proof open, we fail too. *)
-  if Option.has_some stack then
-    CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
-  ()
-
-and interp_control ~st ({ v = cmd } as vernac) =
-  let time_header = mk_time_header vernac in
-  List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
-    cmd.control
-    (fun ~st ->
-       let before_univs = Global.universes () in
-       let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
-       if before_univs == Global.universes () then pstack
-       else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack)
-    ~st
-
-(* Interpreting a possibly delayed proof *)
-let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option =
-  let stack = st.Vernacstate.lemmas in
-  let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
-  let () = match pe with
-    | Admitted ->
-      save_lemma_admitted_delayed ~proof ~info
-    | Proved (_,idopt) ->
-      save_lemma_proved_delayed ~proof ~info ~idopt in
-  stack
-
-let interp_qed_delayed_control ~proof ~info ~st ~control { loc; v=pe } =
-  let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in
-  List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
-    control
-    (fun ~st -> interp_qed_delayed ~proof ~info ~st pe)
-    ~st
-
-(* General interp with management of state *)
-let () =
-  declare_int_option
-    { optdepr  = false;
-      optname  = "the default timeout";
-      optkey   = ["Default";"Timeout"];
-      optread  = (fun () -> !default_timeout);
-      optwrite = ((:=) default_timeout) }
-
-(* Be careful with the cache here in case of an exception. *)
-let interp_gen ~verbosely ~st ~interp_fn cmd =
-  Vernacstate.unfreeze_interp_state st;
-  try vernac_timeout (fun st ->
-      let v_mod = if verbosely then Flags.verbosely else Flags.silently in
-      let ontop = v_mod (interp_fn ~st) cmd in
-      Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"];
-      Vernacstate.freeze_interp_state ~marshallable:false
-    ) st
-  with exn ->
-    let exn = CErrors.push exn in
-    let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in
-    Vernacstate.invalidate_cache ();
-    iraise exn
-
-(* Regular interp *)
-let interp ?(verbosely=true) ~st cmd =
-  interp_gen ~verbosely ~st ~interp_fn:interp_control cmd
-
-let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t =
-  interp_gen ~verbosely:false ~st
-    ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index e65f9d3cfe..6368ebeed8 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,25 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** The main interpretation function of vernacular expressions *)
-val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
-
-(** Execute a Qed but with a proof_object which may contain a delayed
-   proof and won't be forced *)
-val interp_qed_delayed_proof
-  :  proof:Proof_global.proof_object
-  -> info:Lemmas.Info.t
-  -> st:Vernacstate.t
-  -> control:Vernacexpr.control_flag list
-  -> Vernacexpr.proof_end CAst.t
-  -> Vernacstate.t
-
-(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *)
-val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit
-
-(** Flag set when the test-suite is called. Its only effect to display
-    verbose information for [Fail] *)
-val test_mode : bool ref
+(** Vernac Translation into the Vernac DSL *)
+val translate_vernac
+  : atts:Attributes.vernac_flags
+  -> Vernacexpr.vernac_expr
+  -> Vernacextend.typed_vernac
 
 (** Vernacular require command *)
 val vernac_require :
@@ -38,8 +24,3 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
 
 (** Miscellaneous stuff *)
 val command_focus : unit Proof.focus_kind
-
-(** Default proof mode set by `start_proof` *)
-val get_default_proof_mode : unit -> Pvernac.proof_mode
-
-val proof_mode_opt_name : string list
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 2725516a76..e29086d726 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -54,7 +54,6 @@ and proof_block_name = string (** open type of delimiters *)
 
 type typed_vernac =
   | VtDefault of (unit -> unit)
-
   | VtNoProof of (unit -> unit)
   | VtCloseProof of (lemma:Lemmas.t -> unit)
   | VtOpenProof of (unit -> Lemmas.t)
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
new file mode 100644
index 0000000000..c14fc78462
--- /dev/null
+++ b/vernac/vernacinterp.ml
@@ -0,0 +1,278 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \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 Vernacexpr
+
+(* XXX Should move to a common library *)
+let debug = false
+let vernac_pperr_endline pp =
+  if debug then Format.eprintf "@[%a@]@\n%!" Pp.pp_with (pp ()) else ()
+
+(* EJGA: We may remove this, only used twice below *)
+let vernac_require_open_lemma ~stack f =
+  match stack with
+  | Some stack -> f stack
+  | None ->
+    CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress)")
+
+let interp_typed_vernac c ~stack =
+  let open Vernacextend in
+  match c with
+  | VtDefault f -> f (); stack
+  | VtNoProof f ->
+    if Option.has_some stack then
+      CErrors.user_err (Pp.str "Command not supported (Open proofs remain)");
+    let () = f () in
+    stack
+  | VtCloseProof f ->
+    vernac_require_open_lemma ~stack (fun stack ->
+        let lemma, stack = Vernacstate.LemmaStack.pop stack in
+        f ~lemma;
+        stack)
+  | VtOpenProof f ->
+    Some (Vernacstate.LemmaStack.push stack (f ()))
+  | VtModifyProof f ->
+    Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:(fun pstate -> f ~pstate)) stack
+  | VtReadProofOpt f ->
+    let pstate = Option.map (Vernacstate.LemmaStack.with_top_pstate ~f:(fun x -> x)) stack in
+    f ~pstate;
+    stack
+  | VtReadProof f ->
+    vernac_require_open_lemma ~stack
+      (Vernacstate.LemmaStack.with_top_pstate ~f:(fun pstate -> f ~pstate));
+    stack
+
+(* Default proof mode, to be set at the beginning of proofs for
+   programs that cannot be statically classified. *)
+let default_proof_mode = ref (Pvernac.register_proof_mode "Noedit" Pvernac.Vernac_.noedit_mode)
+let get_default_proof_mode () = !default_proof_mode
+
+let get_default_proof_mode_opt () = Pvernac.proof_mode_to_string !default_proof_mode
+let set_default_proof_mode_opt name =
+  default_proof_mode :=
+    match Pvernac.lookup_proof_mode name with
+    | Some pm -> pm
+    | None -> CErrors.user_err Pp.(str (Format.sprintf "No proof mode named \"%s\"." name))
+
+let proof_mode_opt_name = ["Default";"Proof";"Mode"]
+let () =
+  Goptions.declare_string_option Goptions.{
+    optdepr = false;
+    optname = "default proof mode" ;
+    optkey = proof_mode_opt_name;
+    optread = get_default_proof_mode_opt;
+    optwrite = set_default_proof_mode_opt;
+  }
+
+(** A global default timeout, controlled by option "Set Default Timeout n".
+    Use "Unset Default Timeout" to deactivate it (or set it to 0). *)
+
+let default_timeout = ref None
+
+(* Timeout *)
+let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b =
+  match !default_timeout, timeout with
+  | _, Some n
+  | Some n, None ->
+    Control.timeout n f x CErrors.Timeout
+  | None, None ->
+    f x
+
+(* Fail *)
+let test_mode = ref false
+
+(* Restoring the state is the caller's responsibility *)
+let with_fail f : (Pp.t, unit) result =
+  try
+    let _ = f () in
+    Error ()
+  with
+  (* Fail Timeout is a common pattern so we need to support it. *)
+  | e when CErrors.noncritical e || e = CErrors.Timeout ->
+    (* The error has to be printed in the failing state *)
+    Ok CErrors.(iprint (push e))
+
+(* We restore the state always *)
+let with_fail ~st f =
+  let res = with_fail f in
+  Vernacstate.invalidate_cache ();
+  Vernacstate.unfreeze_interp_state st;
+  match res with
+  | Error () ->
+    CErrors.user_err ~hdr:"Fail" (Pp.str "The command has not failed!")
+  | Ok msg ->
+    if not !Flags.quiet || !test_mode
+    then Feedback.msg_notice Pp.(str "The command has indeed failed with message:" ++ fnl () ++ msg)
+
+let locate_if_not_already ?loc (e, info) =
+  match Loc.get_loc info with
+  | None   -> (e, Option.cata (Loc.add_loc info) info loc)
+  | Some l -> (e, info)
+
+let mk_time_header =
+  (* Drop the time header to print the command, we should indeed use a
+     different mechanism to `-time` commands than the current hack of
+     adding a time control to the AST. *)
+  let pr_time_header vernac =
+    let vernac = match vernac with
+      | { CAst.v = { control = ControlTime _ :: control; attrs; expr }; loc } ->
+        CAst.make ?loc { control; attrs; expr }
+      | _ -> vernac
+    in
+    Topfmt.pr_cmd_header vernac
+  in
+  fun vernac -> Lazy.from_fun (fun () -> pr_time_header vernac)
+
+let interp_control_flag ~time_header (f : control_flag) ~st
+    (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) =
+  match f with
+  | ControlFail ->
+    with_fail ~st (fun () -> fn ~st);
+    st.Vernacstate.lemmas
+  | ControlTimeout timeout ->
+    vernac_timeout ~timeout (fun () -> fn ~st) ()
+  | ControlTime batch ->
+    let header = if batch then Lazy.force time_header  else Pp.mt () in
+    System.with_time ~batch ~header (fun () -> fn ~st) ()
+  | ControlRedirect s ->
+    Topfmt.with_output_to_file s (fun () -> fn ~st) ()
+
+(* "locality" is the prefix "Local" attribute, while the "local" component
+ * is the outdated/deprecated "Local" attribute of some vernacular commands
+ * still parsed as the obsolete_locality grammar entry for retrocompatibility.
+ * loc is the Loc.t of the vernacular command being interpreted. *)
+let rec interp_expr ~atts ~st c =
+  let stack = st.Vernacstate.lemmas in
+  vernac_pperr_endline Pp.(fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
+  match c with
+
+  (* The STM should handle that, but LOAD bypasses the STM... *)
+  | VernacAbortAll    -> CErrors.user_err (Pp.str "AbortAll cannot be used through the Load command")
+  | VernacRestart     -> CErrors.user_err (Pp.str "Restart cannot be used through the Load command")
+  | VernacUndo _      -> CErrors.user_err (Pp.str "Undo cannot be used through the Load command")
+  | VernacUndoTo _    -> CErrors.user_err (Pp.str "UndoTo cannot be used through the Load command")
+
+  (* Resetting *)
+  | VernacResetName _  -> CErrors.anomaly (Pp.str "VernacResetName not handled by Stm.")
+  | VernacResetInitial -> CErrors.anomaly (Pp.str "VernacResetInitial not handled by Stm.")
+  | VernacBack _       -> CErrors.anomaly (Pp.str "VernacBack not handled by Stm.")
+
+  (* This one is possible to handle here *)
+  | VernacAbort id    -> CErrors.user_err (Pp.str "Abort cannot be used through the Load command")
+  | VernacLoad (verbosely, fname) ->
+    Attributes.unsupported_attributes atts;
+    vernac_load ~verbosely fname
+  | v ->
+    let fv = Vernacentries.translate_vernac ~atts v in
+    interp_typed_vernac ~stack fv
+
+and vernac_load ~verbosely fname =
+  let exception End_of_input in
+
+  (* Note that no proof should be open here, so the state here is just token for now *)
+  let st = Vernacstate.freeze_interp_state ~marshallable:false in
+  let fname =
+    Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (Pp.str x)) fname in
+  let fname = CUnix.make_suffix fname ".v" in
+  let input =
+    let longfname = Loadpath.locate_file fname in
+    let in_chan = Util.open_utf8_file_in longfname in
+    Pcoq.Parsable.make ~loc:(Loc.initial (Loc.InFile longfname)) (Stream.of_channel in_chan) in
+  (* Parsing loop *)
+  let v_mod = if verbosely then Flags.verbosely else Flags.silently in
+  let parse_sentence proof_mode = Flags.with_option Flags.we_are_parsing
+      (fun po ->
+         match Pcoq.Entry.parse (Pvernac.main_entry proof_mode) po with
+         | Some x -> x
+         | None -> raise End_of_input) in
+  let rec load_loop ~stack =
+    try
+      let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
+      let stack =
+        v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack })
+          (parse_sentence proof_mode input) in
+      load_loop ~stack
+    with
+      End_of_input ->
+      stack
+  in
+  let stack = load_loop ~stack:st.Vernacstate.lemmas in
+  (* If Load left a proof open, we fail too. *)
+  if Option.has_some stack then
+    CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
+  stack
+
+and interp_control ~st ({ CAst.v = cmd } as vernac) =
+  let time_header = mk_time_header vernac in
+  List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
+    cmd.control
+    (fun ~st ->
+       let before_univs = Global.universes () in
+       let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
+       if before_univs == Global.universes () then pstack
+       else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack)
+    ~st
+
+(* XXX: This won't properly set the proof mode, as of today, it is
+   controlled by the STM. Thus, we would need access information from
+   the classifier. The proper fix is to move it to the STM, however,
+   the way the proof mode is set there makes the task non trivial
+   without a considerable amount of refactoring.
+*)
+
+(* Interpreting a possibly delayed proof *)
+let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option =
+  let stack = st.Vernacstate.lemmas in
+  let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
+  let () = match pe with
+    | Admitted ->
+      Lemmas.save_lemma_admitted_delayed ~proof ~info
+    | Proved (_,idopt) ->
+      Lemmas.save_lemma_proved_delayed ~proof ~info ~idopt in
+  stack
+
+let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } =
+  let time_header = mk_time_header (CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe }) in
+  List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
+    control
+    (fun ~st -> interp_qed_delayed ~proof ~info ~st pe)
+    ~st
+
+(* General interp with management of state *)
+let () = let open Goptions in
+  declare_int_option
+    { optdepr  = false;
+      optname  = "the default timeout";
+      optkey   = ["Default";"Timeout"];
+      optread  = (fun () -> !default_timeout);
+      optwrite = ((:=) default_timeout) }
+
+(* Be careful with the cache here in case of an exception. *)
+let interp_gen ~verbosely ~st ~interp_fn cmd =
+  Vernacstate.unfreeze_interp_state st;
+  try vernac_timeout (fun st ->
+      let v_mod = if verbosely then Flags.verbosely else Flags.silently in
+      let ontop = v_mod (interp_fn ~st) cmd in
+      Vernacstate.Proof_global.set ontop [@ocaml.warning "-3"];
+      Vernacstate.freeze_interp_state ~marshallable:false
+    ) st
+  with exn ->
+    let exn = CErrors.push exn in
+    let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in
+    Vernacstate.invalidate_cache ();
+    Util.iraise exn
+
+(* Regular interp *)
+let interp ?(verbosely=true) ~st cmd =
+  interp_gen ~verbosely ~st ~interp_fn:interp_control cmd
+
+let interp_qed_delayed_proof ~proof ~info ~st ~control pe : Vernacstate.t =
+  interp_gen ~verbosely:false ~st
+    ~interp_fn:(interp_qed_delayed_control ~proof ~info ~control) pe
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
new file mode 100644
index 0000000000..16849686da
--- /dev/null
+++ b/vernac/vernacinterp.mli
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \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)         *)
+(************************************************************************)
+
+(** The main interpretation function of vernacular expressions *)
+val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
+
+(** Execute a Qed but with a proof_object which may contain a delayed
+   proof and won't be forced *)
+val interp_qed_delayed_proof
+  :  proof:Proof_global.proof_object
+  -> info:Lemmas.Info.t
+  -> st:Vernacstate.t
+  -> control:Vernacexpr.control_flag list
+  -> Vernacexpr.proof_end CAst.t
+  -> Vernacstate.t
+
+(** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *)
+val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit
+
+(** Flag set when the test-suite is called. Its only effect to display
+    verbose information for [Fail] *)
+val test_mode : bool ref
+
+(** Default proof mode set by `start_proof` *)
+val get_default_proof_mode : unit -> Pvernac.proof_mode
+val proof_mode_opt_name : string list