Merge PR #20674: Stronger synterp/interp phase split checking

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

Author: coqbot-app[bot]

dev/ci/user-overlays/20674-SkySkimmer-stronger-synterp-flag.sh

@@ -0,0 +1 @@
+overlay elpi https://github.com/SkySkimmer/coq-elpi stronger-synterp-flag 20674

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.")
 

library/lib.ml

@@ -515,7 +515,20 @@ let add_discharged_leaf obj =
 
 let add_leaf obj =
   Libobject.cache_object (prefix(),obj);
-  match Libobject.object_stage obj with
+  let ostage = Libobject.object_stage obj in
+  let ok_stage = match !Flags.in_synterp_phase with
+    | None -> true
+    | Some false -> ostage == Interp
+    | Some true -> ostage == Synterp
+  in
+  let () = if not ok_stage then
+      let ppstage = match ostage with Interp -> "interp" | Synterp -> "synterp" in
+      CErrors.anomaly
+        Pp.(str "Adding object " ++
+            str (Libobject.object_name obj) ++
+            str " in incorrect stage (object_stage = " ++ str ppstage ++ str ").")
+  in
+  match ostage with
   | Summary.Stage.Synterp ->
     SynterpActions.add_leaf_entry (AtomicObject obj)
   | Summary.Stage.Interp ->

library/libobject.ml

@@ -246,6 +246,10 @@ let object_stage (Dyn.Dyn (tag, v)) =
   let O decl = DynMap.find tag !cache_tab in
   decl.object_stage
 
+let object_name (Dyn.Dyn (tag, v)) =
+  let O decl = DynMap.find tag !cache_tab in
+  decl.object_name
+
 let dump = Dyn.dump
 
 let local_object_nodischarge ?stage s ~cache =

library/libobject.mli

@@ -238,6 +238,7 @@ val load_object : int -> object_prefix * obj -> unit
 val open_object : open_filter -> int -> object_prefix * obj -> unit
 val subst_object : substitution * obj -> obj
 val classify_object : obj -> substitutivity
+val object_name : obj -> string
 val object_stage : obj -> Summary.Stage.t
 
 type discharged_obj

parsing/procq.ml

@@ -49,6 +49,10 @@ let empty_full_state =
     user_state = GramState.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
 
@@ -73,7 +77,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;recover;has_non_assoc} -> {estate; kwstate = f kwstate; recover; has_non_assoc})
@@ -90,6 +96,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
@@ -129,7 +136,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
 
 type ('a,'b) entry_extension = {
   eext_fun : 'a -> 'b Entry.t -> GramState.t -> GramState.t;
@@ -157,6 +166,7 @@ let extend_entry_sync (type a b)
   state, e
 
 let extend_entry_sync tag interp data () =
+  assert_synterp();
   let statev, e = extend_entry_sync tag interp data !state in
   state := statev;
   e
@@ -469,19 +479,21 @@ let replay_sync_extension = function
   | GramExt (Dyn (tag,g)) -> extend_grammar_command tag g
   | EntryExt (tag,data) -> ignore (extend_entry_command tag data : _ 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

@@ -502,4 +502,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