Guard against parser modification in interp phase

Hopefully detects issues like
https://rocq-prover.zulipchat.com/#narrow/channel/237662-VsCoq-devs-.26-users/topic/.E2.9C.94.20VSCoq.20resetting.20a.20lot.20on.202.2E2.2E5/near/520048311

Author: SkySkimmer

lib/flags.ml

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

lib/flags.mli

@@ -45,7 +45,7 @@ val in_debugger : bool ref
 val in_ml_toplevel : bool ref
 
 (* Used to check stages are used correctly. *)
-val in_synterp_phase : bool ref
+val in_synterp_phase : bool option ref
 
 (* Set Printing All flag. For some reason it is a global flag *)
 val raw_print : bool ref

library/global.ml

@@ -35,7 +35,7 @@ let is_curmod_library () =
   Safe_typing.is_curmod_library !global_env
 
 let assert_not_synterp () =
-  if !Flags.in_synterp_phase then
+  if !Flags.in_synterp_phase = Some true then
     CErrors.anomaly (
       Pp.strbrk"The global environment cannot be accessed during the syntactic interpretation phase.")
 

parsing/procq.ml

@@ -55,6 +55,10 @@ let empty_full_state =
     custom_entries = EntryDataMap.empty;
   }
 
+let assert_synterp () =
+  if !Flags.in_synterp_phase = Some false then
+    CErrors.anomaly Pp.(str "The grammar cannot be modified during the interp phase.")
+
 (** Not marshallable! *)
 let state = ref empty_full_state
 
@@ -78,7 +82,9 @@ let modify_state_unsync f state =
   let current_state = if is_base then base_state else f state.current_state in
   { state with base_state; current_state }
 
-let modify_state_unsync f () = state := modify_state_unsync f !state
+let modify_state_unsync f () =
+  assert_synterp ();
+  state := modify_state_unsync f !state
 
 let modify_keyword_state f =
   modify_state_unsync (fun {estate;kwstate} -> {estate; kwstate = f kwstate})
@@ -95,6 +101,7 @@ let make_entry_unsync make remake state =
   { state with base_state; current_state }, e
 
 let make_entry_unsync make remake () =
+  assert_synterp();
   let statev, e = make_entry_unsync make remake !state in
   state := statev;
   e
@@ -134,7 +141,9 @@ let grammar_extend_sync user_state entry rules state =
     current_sync_extensions = GramExt entry :: state.current_sync_extensions;
   }
 
-let grammar_extend_sync st e r () = state := grammar_extend_sync st e r !state
+let grammar_extend_sync st e r () =
+  assert_synterp();
+  state := grammar_extend_sync st e r !state
 
 let extend_entry_sync (type a) (tag : a EntryCommand.tag) (name : string) state : _ * a Entry.t =
   let current_estate, e = Entry.make name state.current_state.estate in
@@ -158,6 +167,7 @@ let extend_entry_sync (type a) (tag : a EntryCommand.tag) (name : string) state
   state, e
 
 let extend_entry_command tag name =
+  assert_synterp();
   let statev, e = extend_entry_sync tag name !state in
   state := statev;
   e
@@ -467,19 +477,21 @@ let replay_sync_extension = function
   | GramExt (Dyn (tag,g)) -> extend_grammar_command tag g
   | EntryExt (tag,name) -> ignore (extend_entry_command tag name : _ Entry.t)
 
-let unfreeze = function
-  | {frozen_sync;} as frozen ->
-    let to_remove, to_add, _common = factorize_grams (!state).current_sync_extensions frozen_sync in
-    if CList.is_empty to_remove then begin
-      List.iter replay_sync_extension (List.rev to_add);
-      unfreeze_only_keywords frozen
-    end
-    else begin
-      state := reset_to_base !state;
-      List.iter replay_sync_extension (List.rev frozen_sync);
-      (* put back the keyword state, needed to support ssr hacks *)
-      unfreeze_only_keywords frozen
-    end
+let unfreeze ({frozen_sync;} as frozen) =
+  (* allow unfreezing synterp state even during interp phase *)
+  Flags.with_modified_ref Flags.in_synterp_phase (fun _ -> None) (fun () ->
+  let to_remove, to_add, _common = factorize_grams (!state).current_sync_extensions frozen_sync in
+  if CList.is_empty to_remove then begin
+    List.iter replay_sync_extension (List.rev to_add);
+    unfreeze_only_keywords frozen
+  end
+  else begin
+    state := reset_to_base !state;
+    List.iter replay_sync_extension (List.rev frozen_sync);
+    (* put back the keyword state, needed to support ssr hacks *)
+    unfreeze_only_keywords frozen
+  end)
+    ()
 
 let freeze_state state = {
   frozen_sync = state.current_sync_extensions;

stm/stm.ml

@@ -402,7 +402,7 @@ end = struct (* {{{ *)
 
        In case you are hitting the race enable stm_debug.
     *)
-    if !stm_debug then Flags.in_synterp_phase := false;
+    Flags.in_synterp_phase := Some false;
 
     let fname =
       "stm_" ^ Str.global_replace (Str.regexp " ") "_" (Spawned.process_id ()) in

vernac/synterp.ml

@@ -501,4 +501,4 @@ and synterp_control ~intern CAst.{ loc; v = cmd } =
   CAst.make ?loc { expr; control; attrs = cmd.attrs }
 
 let synterp_control ~intern cmd =
-  Flags.with_option Flags.in_synterp_phase (synterp_control ~intern) cmd
+  Flags.with_modified_ref Flags.in_synterp_phase (fun _ -> Some true) (synterp_control ~intern) cmd

vernac/vernacentries.ml

@@ -1698,8 +1698,13 @@ let vernac_require_interp needed modrefl export qidl =
     export
 
 let vernac_require ~intern from export qidl =
-  let needed, modrefl = Synterp.synterp_require ~intern from export qidl in
-  vernac_require_interp needed modrefl export qidl
+  let needed, modrefl = Flags.with_modified_ref Flags.in_synterp_phase (fun _ -> Some true) (fun () ->
+      Synterp.synterp_require ~intern from export qidl)
+      ()
+  in
+  Flags.with_modified_ref Flags.in_synterp_phase (fun _ -> Some false) (fun () ->
+      vernac_require_interp needed modrefl export qidl)
+    ()
 
 (* Coercions and canonical structures *)
 

vernac/vernacinterp.ml

@@ -37,7 +37,7 @@ let interp_control_gen ~loc ~st ~unfreeze_transient control f =
       ~with_local_state:(with_interp_state ~unfreeze_transient st)
       control
       ~noop
-      f
+      (Flags.with_modified_ref Flags.in_synterp_phase (fun _ -> Some false) f)
   in
   if VernacControl.after_last_phase ~loc control
   then noop