Merge PR #13425: [stm] [declare] Try to propagate safe bits of proof information

Reviewed-by: gares

7 files changed, 43 insertions, 72 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index df7e35beb5..f7d66b7b53 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1003,9 +1003,9 @@ end = struct (* {{{ *)
 end (* }}} *)
 
 (* Wrapper for the proof-closing special path for Qed *)
-let stm_qed_delay_proof ?route ~proof ~pinfo ~id ~st ~loc ~control pending : Vernacstate.t =
+let stm_qed_delay_proof ?route ~proof ~id ~st ~loc ~control pending : Vernacstate.t =
   set_id_for_feedback ?route dummy_doc id;
-  Vernacinterp.interp_qed_delayed_proof ~proof ~pinfo ~st ~control (CAst.make ?loc pending)
+  Vernacinterp.interp_qed_delayed_proof ~proof ~st ~control (CAst.make ?loc pending)
 
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 (* It is currently called 19 times, this number should be certainly
@@ -1470,16 +1470,15 @@ 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 =
             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
+                ~proof:pobject ~loc ~control:[] (Proved (opaque,None)) in
             ()
           with exn ->
             (* If [stm_qed_delay_proof] fails above we need to use the
@@ -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 =
         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 *)
 
@@ -1638,7 +1634,7 @@ end = struct (* {{{ *)
        *)
       (* STATE We use the state resulting from reaching start. *)
       let st = Vernacstate.freeze_interp_state ~marshallable:false in
-      ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~pinfo ~loc ~control:[] (Proved (opaque,None)));
+      ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~loc ~control:[] (Proved (opaque,None)));
       (* Is this name the same than the one in scope? *)
       let name = Declare.Proof.get_po_name proof in
       `OK name
@@ -2219,13 +2215,13 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                       | VtKeepDefined ->
                         CErrors.anomaly (Pp.str "Cannot delegate transparent proofs, this is a bug in the STM.")
                     in
-                    let proof, pinfo =
+                    let proof =
                       PG_compat.close_future_proof ~feedback_id:id fp in
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     let st = Vernacstate.freeze_interp_state ~marshallable:false in
                     let control, pe = extract_pe x in
-                    ignore(stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe);
+                    ignore(stm_qed_delay_proof ~id ~st ~proof ~loc ~control pe);
                     feedback ~id:id Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
@@ -2264,9 +2260,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 let st = Vernacstate.freeze_interp_state ~marshallable:false in
                 let _st = match proof with
                   | None ->  stm_vernac_interp id st x
-                  | Some (proof, pinfo) ->
+                  | Some proof ->
                     let control, pe = extract_pe x in
-                    stm_qed_delay_proof ~id ~st ~proof ~pinfo ~loc ~control pe
+                    stm_qed_delay_proof ~id ~st ~proof ~loc ~control pe
                 in
                 let wall_clock3 = Unix.gettimeofday () in
                 Aux_file.record_in_aux_at ?loc:x.expr.CAst.loc "proof_check_time"
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 1e8771b641..73ebca276d 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
 
@@ -1367,14 +1369,6 @@ module Proof_info = struct
     ; proof_ending = CEphemeron.create proof_ending
     }
 
-  (* This is used due to a deficiency on the API, should fix *)
-  let add_first_thm ~pinfo ~name ~typ ~impargs =
-    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 =
@@ -1388,7 +1382,6 @@ type t =
 
 (*** Proof Global manipulation ***)
 
-let info { pinfo } = pinfo
 let get ps = ps.proof
 let get_name ps = (Proof.data ps.proof).Proof.name
 let get_initial_euctx ps = ps.initial_euctx
@@ -1566,6 +1559,7 @@ type proof_object =
   (* [name] only used in the STM *)
   ; entries : Evd.side_effects proof_entry list
   ; uctx: UState.t
+  ; pinfo : Proof_info.t
   }
 
 let get_po_name { name } = name
@@ -1673,7 +1667,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps =
     definition_entry_core ~opaque ?using ~univs:utyp ~univsbody:ubody ~types:typ ~eff body
   in
   let entries = CList.map make_entry elist  in
-  { name; entries; uctx }
+  { name; entries; uctx; pinfo }
 
 type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
 
@@ -1718,7 +1712,7 @@ let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.comput
     |> delayed_definition_entry ~opaque ~feedback_id ~using ~univs ~types
   in
   let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in
-  { name; entries; uctx = initial_euctx }
+  { name; entries; uctx = initial_euctx; pinfo }
 
 let close_future_proof = close_proof_delayed
 
@@ -1961,7 +1955,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
@@ -2083,7 +2077,7 @@ let save ~pm ~proof ~opaque ~idopt =
   let proof_info = process_idopt_for_save ~idopt proof.pinfo in
   finalize_proof ~pm proof_obj proof_info
 
-let save_regular ~proof ~opaque ~idopt =
+let save_regular ~(proof : t) ~opaque ~idopt =
   let open Proof_ending in
   match CEphemeron.default proof.pinfo.Proof_info.proof_ending Regular with
   | Regular ->
@@ -2094,8 +2088,8 @@ let save_regular ~proof ~opaque ~idopt =
 (***********************************************************************)
 (* Special case to close a lemma without forcing a proof               *)
 (***********************************************************************)
-let save_lemma_admitted_delayed ~pm ~proof ~pinfo =
-  let { entries; uctx } = proof in
+let save_lemma_admitted_delayed ~pm ~proof =
+  let { entries; uctx; pinfo } = proof in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
   let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
@@ -2106,16 +2100,10 @@ let save_lemma_admitted_delayed ~pm ~proof ~pinfo =
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
   finish_admitted ~pm ~uctx ~pinfo ~sec_vars ~univs
 
-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 *)
-  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
-    finalize_proof ~pm proof info
-  else
-    let info = process_idopt_for_save ~idopt pinfo in
-    finalize_proof ~pm proof info
+let save_lemma_proved_delayed ~pm ~proof ~idopt =
+  (* vio2vo used to call this with invalid [pinfo], now it should work fine. *)
+  let pinfo = process_idopt_for_save ~idopt proof.pinfo in
+  finalize_proof ~pm proof pinfo
 
 end (* Proof module *)
 
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 0520bf8717..e4c77113af 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -278,14 +278,6 @@ module Proof : sig
       environment and empty evar_map. *)
   val get_current_context : t -> Evd.evar_map * Environ.env
 
-  (* Internal, don't use *)
-  module Proof_info : sig
-    type t
-    (* Make a dummy value, used in the stm *)
-    val default : unit -> t
-  end
-  val info : t -> Proof_info.t
-
   (** {2 Proof delay API, warning, internal, not stable *)
 
   (* Intermediate step necessary to delegate the future.
@@ -313,13 +305,11 @@ module Proof : sig
   val save_lemma_admitted_delayed :
        pm:OblState.t
     -> proof:proof_object
-    -> pinfo:Proof_info.t
     -> OblState.t
 
   val save_lemma_proved_delayed
     : pm:OblState.t
     -> proof:proof_object
-    -> pinfo:Proof_info.t
     -> idopt:Names.lident option
     -> OblState.t * GlobRef.t list
 
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index edf48fef1a..57d9e0ac3c 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -226,24 +226,24 @@ and interp_control ~st ({ CAst.v = cmd } as vernac) =
 *)
 
 (* Interpreting a possibly delayed proof *)
-let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t =
+let interp_qed_delayed ~proof ~st pe : Vernacstate.LemmaStack.t option * Declare.OblState.t =
   let stack = st.Vernacstate.lemmas in
   let pm = st.Vernacstate.program in
   let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
   let pm = match pe with
     | Admitted ->
-      Declare.Proof.save_lemma_admitted_delayed ~pm ~proof ~pinfo
+      Declare.Proof.save_lemma_admitted_delayed ~pm ~proof
     | Proved (_,idopt) ->
-      let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~pinfo ~idopt in
+      let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~idopt in
       pm
   in
   stack, pm
 
-let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } =
+let interp_qed_delayed_control ~proof ~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 ~pinfo ~st pe)
+    (fun ~st -> interp_qed_delayed ~proof ~st pe)
     ~st
 
 (* General interp with management of state *)
@@ -273,6 +273,6 @@ let interp_gen ~verbosely ~st ~interp_fn cmd =
 let interp ?(verbosely=true) ~st cmd =
   interp_gen ~verbosely ~st ~interp_fn:interp_control cmd
 
-let interp_qed_delayed_proof ~proof ~pinfo ~st ~control pe : Vernacstate.t =
+let interp_qed_delayed_proof ~proof ~st ~control pe : Vernacstate.t =
   interp_gen ~verbosely:false ~st
-    ~interp_fn:(interp_qed_delayed_control ~proof ~pinfo ~control) pe
+    ~interp_fn:(interp_qed_delayed_control ~proof ~control) pe
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 84d3256c9f..f31bebf7db 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -15,7 +15,6 @@ val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control ->
    proof and won't be forced *)
 val interp_qed_delayed_proof
   :  proof:Declare.Proof.proof_object
-  -> pinfo:Declare.Proof.Proof_info.t
   -> st:Vernacstate.t
   -> control:Vernacexpr.control_flag list
   -> Vernacexpr.proof_end CAst.t
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 204008997d..011d943c9b 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -204,18 +204,14 @@ module Declare_ = struct
       s_lemmas := Some stack;
       res
 
-  type closed_proof = Declare.Proof.proof_object * Declare.Proof.Proof_info.t
-
   let return_proof () = cc Declare.Proof.return_proof
   let return_partial_proof () = cc Declare.Proof.return_partial_proof
 
   let close_future_proof ~feedback_id pf =
-    cc (fun pt -> Declare.Proof.close_future_proof ~feedback_id pt pf,
-                  Declare.Proof.info pt)
+    cc (fun pt -> Declare.Proof.close_future_proof ~feedback_id pt pf)
 
   let close_proof ~opaque ~keep_body_ucst_separate =
-    cc (fun pt -> Declare.Proof.close_proof ~opaque ~keep_body_ucst_separate pt,
-                  Declare.Proof.info pt)
+    cc (fun pt -> Declare.Proof.close_proof ~opaque ~keep_body_ucst_separate pt)
 
   let discard_all () = s_lemmas := None
   let update_sigma_univs ugraph = dd (Declare.Proof.update_sigma_univs ugraph)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index e1b13dcb73..e9e06e6d8e 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -104,13 +104,15 @@ module Declare : sig
   val return_proof : unit -> Declare.Proof.closed_proof_output
   val return_partial_proof : unit -> Declare.Proof.closed_proof_output
 
-  type closed_proof = Declare.Proof.proof_object * Declare.Proof.Proof_info.t
-
-  val close_future_proof :
-    feedback_id:Stateid.t ->
-    Declare.Proof.closed_proof_output Future.computation -> closed_proof
-
-  val close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> closed_proof
+  val close_future_proof
+    : feedback_id:Stateid.t
+    -> Declare.Proof.closed_proof_output Future.computation
+    -> Declare.Proof.proof_object
+
+  val close_proof
+    : opaque:Vernacexpr.opacity_flag
+    -> keep_body_ucst_separate:bool
+    -> Declare.Proof.proof_object
 
   val discard_all : unit -> unit
   val update_sigma_univs : UGraph.t -> unit