Merge PR #17331: Separate parsing and execution of vernacular

Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: jfehrle
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

dev/ci/user-overlays/17331-separate-parsing-exec-vernac.sh

@@ -0,0 +1,11 @@
+overlay lean_importer https://github.com/maximedenes/coq-lean-import vernac-synterp 17331
+
+overlay elpi https://github.com/maximedenes/coq-elpi vernac-synterp 17331
+
+overlay serapi https://github.com/maximedenes/coq-serapi vernac-synterp 17331
+
+overlay coq_lsp https://github.com/maximedenes/coq-lsp.git vernac-synterp 17331
+
+overlay metacoq https://github.com/maximedenes/metacoq.git vernac-synterp 17331
+
+overlay tactician https://github.com/SkySkimmer/coq-tactician vernac-synterp 17331

ide/coqide/idetop.ml

@@ -70,9 +70,9 @@ let coqide_known_option table = List.mem table [
   ["Diffs"]]
 
 let is_known_option cmd = match cmd with
-  | VernacSetOption (_, o, OptionSetTrue)
-  | VernacSetOption (_, o, OptionSetString _)
-  | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o
+  VernacSynterp (VernacSetOption (_, o, OptionSetTrue)
+    | VernacSetOption (_, o, OptionSetString _)
+    | VernacSetOption (_, o, OptionUnset)) -> coqide_known_option o
   | _ -> false
 
 let ide_cmd_warns ~id { CAst.loc; v } =

lib/flags.ml

@@ -53,7 +53,7 @@ let in_toplevel = ref false
 
 let raw_print = ref false
 
-let we_are_parsing = ref false
+let in_synterp_phase = ref false
 
 (* Translate *)
 let beautify = ref false

lib/flags.mli

@@ -45,7 +45,7 @@ val in_debugger : bool ref
 val in_toplevel : bool ref
 
 (* development flag to detect race conditions, it should go away. *)
-val we_are_parsing : bool ref
+val in_synterp_phase : bool ref
 
 (* Set Printing All flag. For some reason it is a global flag *)
 val raw_print : bool ref

lib/system.ml

@@ -289,6 +289,7 @@ let output_int64 ch n =
 (* Time stamps. *)
 
 type time = {real: float; user: float; system: float; }
+type duration = time
 
 let get_time () =
   let t = Unix.times ()  in
@@ -300,33 +301,56 @@ let get_time () =
 (* Keep only 3 significant digits *)
 let round f = (floor (f *. 1e3)) *. 1e-3
 
+let duration_between ~start ~stop = {
+  real = stop.real -. start.real;
+  user = stop.user -. start.user;
+  system = stop.system -. start.system;
+}
+
+let duration_add t1 t2 = {
+  real = t1.real +. t2.real;
+  user = t1.user +. t2.user;
+  system = t1.system +. t2.system;
+}
+
 let diff1 proj ~start ~stop = round (proj stop -. proj start)
 
 let time_difference t1 t2 = diff1 (fun t -> t.real) ~start:t1 ~stop:t2
 
-let fmt_time_difference start stop =
-  real (diff1 (fun t -> t.real) ~start ~stop) ++ str " secs " ++
+let duration_real { real; _ } = real
+
+let fmt_duration { real = treal; user; system } =
+  real (round treal) ++ str " secs " ++
   str "(" ++
-  real (diff1 (fun t -> t.user) ~start ~stop) ++ str "u" ++
+  real (round user) ++ str "u" ++
   str "," ++
-  real (diff1 (fun t -> t.system) ~start ~stop) ++ str "s" ++
+  real (round system) ++ str "s" ++
   str ")"
 
-let with_time f x =
-  let tstart = get_time() in
-  let msg = "Finished transaction in " in
+let fmt_time_difference start stop =
+  fmt_duration (duration_between ~start ~stop)
+
+type 'a transaction_result = (('a * duration), (Exninfo.iexn * duration)) Result.t
+
+let measure_duration f x =
+  let start = get_time() in
   try
     let y = f x in
-    let tend = get_time() in
-    let msg2 = " (successful)" in
-    Feedback.msg_notice (str msg ++ fmt_time_difference tstart tend ++ str msg2);
-    y
+    let stop = get_time() in
+    Ok (y, duration_between ~start ~stop)
   with e ->
-    let tend = get_time() in
-    let msg = "Finished failing transaction in " in
-    let msg2 = " (failure)" in
-    Feedback.msg_notice (str msg ++ fmt_time_difference tstart tend ++ str msg2);
-    raise e
+    let stop = get_time() in
+    let exn = Exninfo.capture e in
+    Error (exn, duration_between ~start ~stop)
+
+let fmt_transaction_result x =
+  let msg, msg2, duration = match x with
+  | Ok(_, duration) ->
+    "Finished transaction in ", " (successful)", duration
+  | Error(_,duration) ->
+    "Finished failing transaction in ", " (failure)", duration
+  in
+  str msg ++ fmt_duration duration ++ str msg2
 
 (* We use argv.[0] as we don't want to resolve symlinks *)
 let get_toplevel_path ?(byte=Sys.(backend_type = Bytecode)) top =

lib/system.mli

@@ -108,13 +108,21 @@ val check_caml_version : caml:string -> file:string -> unit
 (** {6 Time stamps.} *)
 
 type time
+type duration
 
 val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
 
+val duration_between : start:time -> stop:time -> duration
+val duration_add : duration -> duration -> duration
+val duration_real : duration -> float
+
 val fmt_time_difference : time -> time -> Pp.t
+val fmt_duration : duration -> Pp.t
 
-val with_time : ('a -> 'b) -> 'a -> 'b
+type 'a transaction_result = (('a * duration), (Exninfo.iexn * duration)) Result.t
+val measure_duration : ('a -> 'b) -> 'a -> 'b transaction_result
+val fmt_transaction_result : 'a transaction_result -> Pp.t
 
 (** [get_toplevel_path program] builds a complete path to the
    executable denoted by [program]. This involves:

library/global.ml

@@ -30,12 +30,12 @@ let global_env, global_env_summary_tag =
 let is_joined_environment () =
   Safe_typing.is_joined_environment !global_env
 
-let assert_not_parsing () =
-  if !Flags.we_are_parsing then
+let assert_not_synterp () =
+  if !Flags.in_synterp_phase then
     CErrors.anomaly (
-      Pp.strbrk"The global environment cannot be accessed during parsing.")
+      Pp.strbrk"The global environment cannot be accessed during the syntactic interpretation phase.")
 
-let safe_env () = assert_not_parsing(); !global_env
+let safe_env () = assert_not_synterp(); !global_env
 
 let set_safe_env e = global_env := e
 
@@ -57,12 +57,12 @@ let globalize f =
 
 let globalize0_with_summary fs f =
   let env = f (safe_env ()) in
-  Summary.unfreeze_summaries ~partial:true fs;
+  Summary.Interp.unfreeze_summaries ~partial:true fs;
   GlobalSafeEnv.set_safe_env env
 
 let globalize_with_summary fs f =
   let res,env = f (safe_env ()) in
-  Summary.unfreeze_summaries ~partial:true fs;
+  Summary.Interp.unfreeze_summaries ~partial:true fs;
   GlobalSafeEnv.set_safe_env env;
   res
 

library/global.mli

@@ -80,7 +80,7 @@ val add_include :
 val open_section : unit -> unit
 (** [poly] is true when the section should be universe polymorphic *)
 
-val close_section : Summary.frozen -> unit
+val close_section : Summary.Interp.frozen -> unit
 (** Close the section and reset the global state to the one at the time when
     the section what opened. *)
 
@@ -91,11 +91,11 @@ val sections_are_opened : unit -> bool
 val start_module : Id.t -> ModPath.t
 val start_modtype : Id.t -> ModPath.t
 
-val end_module : Summary.frozen -> Id.t ->
+val end_module : Summary.Interp.frozen -> Id.t ->
   (Entries.module_struct_entry * inline) option ->
     ModPath.t * MBId.t list * Mod_subst.delta_resolver
 
-val end_modtype : Summary.frozen -> Id.t -> ModPath.t * MBId.t list
+val end_modtype : Summary.Interp.frozen -> Id.t -> ModPath.t * MBId.t list
 
 val add_module_parameter :
   MBId.t -> Entries.module_struct_entry -> inline ->

library/goptions.ml

@@ -431,6 +431,12 @@ let warn_unknown_option =
     Pp.(fun key -> strbrk "There is no flag or option with this name: \"" ++
                   str (nickname key) ++ str "\".")
 
+let get_option_value key =
+  try
+    let (_,_,(read,write,append)) = get_option key in
+    Some read
+  with Not_found -> None
+
 (** Sets the option only if [stage] matches the option declaration or if [stage]
   is omitted. If the option is not found, a warning is emitted only if the stage
   is [Interp] or omitted. *)

library/goptions.mli

@@ -192,6 +192,9 @@ type table_value =
   | StringRefValue of string
   | QualidRefValue of Libnames.qualid
 
+(** [get_option_value key] returns [None] if option with name [key] was not found. *)
+val get_option_value : option_name -> (unit -> option_value) option
+
 val set_option_value : ?locality:option_locality -> ?stage:Summary.Stage.t ->
   ('a -> option_value -> option_value) -> option_name -> 'a -> unit
 (** [set_option_value ?locality f name v] sets [name] to the result of