[stm] [declare] Try to propagate safe bits of proof information

Since 8.5, the STM could not delegate proof information it was
contained inside a closure. This could potentially create some
problems, as witnessed in #12586.

Recent refactoring have reified however much of this state, so it
seems a good idea to use bits of the state now, at the cost of
introducing some safeguards in `declare.ml` w.r.t. `Ephemerons`.

3 files changed, 11 insertions, 14 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index df7e35beb5..977b814e93 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1470,14 +1470,13 @@ end = struct (* {{{ *)
         (* Unfortunately close_future_proof and friends are not pure so we need
            to set the state manually here *)
           State.unfreeze st;
-          let pobject, _info =
+          let pobject, pinfo =
             PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           let opaque = Opaque in
           try
             let _pstate =
-              let pinfo = Declare.Proof.Proof_info.default () in
               stm_qed_delay_proof ~st ~id:stop
                 ~proof:pobject ~pinfo ~loc ~control:[] (Proved (opaque,None)) in
             ()
@@ -1621,12 +1620,9 @@ end = struct (* {{{ *)
       else begin
       let opaque = Opaque in
 
-      (* The original terminator, a hook, has not been saved in the .vio*)
-      let proof, _info =
+      let proof, pinfo =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true in
 
-      let pinfo = Declare.Proof.Proof_info.default () in
-
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
 
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 1e8771b641..a7d9a604b1 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -39,8 +39,10 @@ module Hook = struct
   let make_g hook = CEphemeron.create hook
   let make (hook : S.t -> unit) : t = CEphemeron.create (fun x () -> hook x)
 
-  let call_g ?hook x s = Option.cata (fun hook -> CEphemeron.get hook x s) s hook
-  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x ()) hook
+  let hcall hook x s = CEphemeron.default hook (fun _ x -> x) x s
+
+  let call_g ?hook x s = Option.cata (fun hook -> hcall hook x s) s hook
+  let call ?hook x = Option.iter (fun hook -> hcall hook x ()) hook
 
 end
 
@@ -1372,9 +1374,6 @@ module Proof_info = struct
     let cinfo : Constr.t CInfo.t = CInfo.make ~name ~impargs ~typ:(EConstr.Unsafe.to_constr typ) () in
     { pinfo with cinfo = cinfo :: pinfo.cinfo }
 
-  (* This is called by the STM, and we have to fixup cinfo later as
-     indeed it will not be correct *)
-  let default () = make ~cinfo:[] ~info:(Info.make ()) ()
 end
 
 type t =
@@ -1961,7 +1960,7 @@ let compute_proof_using_for_admitted proof typ pproofs =
 let finish_admitted ~pm ~pinfo ~uctx ~sec_vars ~univs =
   let cst = MutualEntry.declare_variable ~pinfo ~uctx ~sec_vars ~univs in
   (* If the constant was an obligation we need to update the program map *)
-  match CEphemeron.get pinfo.Proof_info.proof_ending with
+  match CEphemeron.default pinfo.Proof_info.proof_ending Proof_ending.Regular with
   | Proof_ending.End_obligation oinfo ->
     Obls_.obligation_admitted_terminator ~pm oinfo uctx (List.hd cst)
   | _ -> pm
@@ -2109,6 +2108,7 @@ let save_lemma_admitted_delayed ~pm ~proof ~pinfo =
 let save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt =
   (* vio2vo calls this but with invalid info, we have to workaround
      that to add the name to the info structure *)
+  (* IMPORTANT: after #13425 this may not be needed. *)
   if CList.is_empty pinfo.Proof_info.cinfo then
     let name = get_po_name proof in
     let info = Proof_info.add_first_thm ~pinfo ~name ~typ:EConstr.mkSet ~impargs:[] in
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 0520bf8717..2d8e9656b1 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -280,9 +280,10 @@ module Proof : sig
 
   (* Internal, don't use *)
   module Proof_info : sig
+    (* Note to developers, when marshalled, this will still lose some
+       fields, such as hooks or proof terminators, as they are still
+       closures. *)
     type t
-    (* Make a dummy value, used in the stm *)
-    val default : unit -> t
   end
   val info : t -> Proof_info.t