Merge PR coq#18952: Cleanup some STM related APIs in declare.ml

Reviewed-by: ppedrot Reviewed-by: gares Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Apr 21, 2024 · 88a27ca · 88a27ca
2 parents d9f7f94 + 970b051
commit 88a27ca
Show file tree

Hide file tree

Showing 6 changed files with 28 additions and 42 deletions.
diff --git a/stm/stm.ml b/stm/stm.ml
@@ -143,7 +143,7 @@ struct
 end
 
 module Vcs_ = Vcs.Make(Stateid.Self)(Kind)
-type future_proof = Declare.Proof.closed_proof_output Future.computation
+type future_proof = Declare.Proof.closed_proof_output option Future.computation
 
 type branch_type = Vcs_.Branch.t Kind.t
 (* TODO 8.7 : split commands and tactics, since this type is too messy now *)
@@ -1309,7 +1309,7 @@ module rec ProofTask : sig
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Declare.Proof.closed_proof_output Future.assignment -> unit;
+    t_assign   : Declare.Proof.closed_proof_output option Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1332,7 +1332,7 @@ module rec ProofTask : sig
     ?loc:Loc.t ->
     drop_pt:bool ->
     Stateid.exn_info -> Stateid.t ->
-      Declare.Proof.closed_proof_output Future.computation
+      Declare.Proof.closed_proof_output option Future.computation
 
 end = struct (* {{{ *)
 
@@ -1345,7 +1345,7 @@ end = struct (* {{{ *)
     t_stop     : Stateid.t;
     t_drop     : bool;
     t_states   : competence;
-    t_assign   : Declare.Proof.closed_proof_output Future.assignment -> unit;
+    t_assign   : Declare.Proof.closed_proof_output option Future.assignment -> unit;
     t_loc      : Loc.t option;
     t_uuid     : Future.UUID.t;
     t_name     : string }
@@ -1368,7 +1368,7 @@ end = struct (* {{{ *)
     e_safe_states : Stateid.t list }
 
   type response =
-    | RespBuiltProof of Declare.Proof.closed_proof_output * float
+    | RespBuiltProof of Declare.Proof.closed_proof_output option * float
     | RespError of error
     | RespStates of (Stateid.t * State.partial_state) list
 
@@ -1445,7 +1445,7 @@ end = struct (* {{{ *)
     let wall_clock2 = Unix.gettimeofday () in
     Aux_file.record_in_aux_at ?loc "proof_build_time"
       (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
-    let p = if drop_pt then PG_compat.return_partial_proof () else PG_compat.return_proof () in
+    let p = if drop_pt then None else Some (PG_compat.return_proof ()) in
     if drop_pt then feedback ~id Complete;
     p
 
@@ -1473,9 +1473,11 @@ end = struct (* {{{ *)
        * a bad fixpoint *)
       (* STATE: We use the current installed imperative state *)
       let st = State.freeze () in
-      if not drop then begin
-        (* Unfortunately close_future_proof and friends are not pure so we need
-           to set the state manually here *)
+      let () = match proof with
+        | None -> (* drop *) ()
+        | Some proof ->
+          (* Unfortunately close_future_proof and friends are not pure so we need
+             to set the state manually here *)
           State.unfreeze st;
           let pobject =
             PG_compat.close_future_proof ~feedback_id:stop (Future.from_val proof) in
@@ -1495,7 +1497,7 @@ end = struct (* {{{ *)
             let iexn = Exninfo.capture exn in
             let iexn = State.exn_on exn_info.Stateid.id ~valid:exn_info.Stateid.valid iexn in
             Exninfo.iraise iexn
-        end;
+      in
       (* STATE: Restore the state XXX: handle exn *)
       State.unfreeze st;
       RespBuiltProof(proof,time)
@@ -2089,8 +2091,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 fp' = Future.chain fp (function
+                        | Some p -> p
+                        | None ->
+                          CErrors.anomaly Pp.(str "Attempting to force admitted proof contents."))
+                    in
                     let proof =
-                      PG_compat.close_future_proof ~feedback_id:id fp in
+                      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_full_state () in

diff --git a/vernac/declare.ml b/vernac/declare.ml
@@ -1723,15 +1723,11 @@ let get_open_goals ps =
   List.length (Evd.shelf sigma)
 
 type proof_object =
-  { name : Names.Id.t
-  (* [name] only used in the STM *)
-  ; entries : proof_entry list
+  { entries : proof_entry list
   ; uctx: UState.t
   ; pinfo : Proof_info.t
   }
 
-let get_po_name { name } = name
-
 let { Goptions.get = private_poly_univs } =
   Goptions.declare_bool_option_and_ref
     ~key:["Private";"Polymorphic";"Universes"]
@@ -1831,7 +1827,7 @@ let close_proof ?warn_incomplete ~opaque ~keep_body_ucst_separate ps =
 
   let { using; proof; initial_euctx; pinfo } = ps in
   let { Proof_info.info = { Info.udecl } } = pinfo in
-  let { Proof.name; poly } = Proof.data proof in
+  let { Proof.poly } = Proof.data proof in
   let elist, uctx = prepare_proof ?warn_incomplete ps in
   let opaque = match opaque with
     | Vernacexpr.Opaque -> true
@@ -1850,14 +1846,14 @@ let close_proof ?warn_incomplete ~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; pinfo }
+  { entries; uctx; pinfo }
 
 type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t
 
 let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) =
   let { using; proof; initial_euctx; pinfo } = ps in
   let { Proof_info.info = { Info.udecl } } = pinfo in
-  let { Proof.name; poly; entry; sigma } = Proof.data proof in
+  let { Proof.poly; entry; sigma } = Proof.data proof in
 
   (* We don't allow poly = true in this path *)
   if poly then
@@ -1876,6 +1872,7 @@ let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.comput
     let univs = UState.univ_entry ~poly:false initial_euctx in
     let types = nf (EConstr.Unsafe.to_constr types) in
 
+    (* NB: for Admitted proofs [fpl] is not valid (raises anomaly when forced) *)
     Future.chain fpl (fun (pf, uctx) ->
         let (pt, eff) = List.nth pf i in
         (* Deferred proof, we already checked the universe declaration with
@@ -1893,20 +1890,10 @@ 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 = CList.map_i make_entry 0 (Proofview.initial_goals entry) in
-  { name; entries; uctx = initial_euctx; pinfo }
+  { entries; uctx = initial_euctx; pinfo }
 
 let close_future_proof = close_proof_delayed
 
-let return_partial_proof { proof } =
- let proofs = Proof.partial_proof proof in
- let Proof.{sigma=evd} = Proof.data proof in
- let eff = Evd.eval_side_effects evd in
- (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-     side-effects... This may explain why one need to uniquize side-effects
-     thereafter... *)
- let proofs = List.map (fun c -> EConstr.Unsafe.to_constr c, eff) proofs in
- proofs, Evd.evar_universe_context evd
-
 let return_proof ps =
   let p, uctx = prepare_proof ps in
   List.map (fun (((_ub, body),eff),_) -> (body,eff)) p, uctx
@@ -2294,7 +2281,8 @@ let save_lemma_admitted_delayed ~pm ~proof =
 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
+  let pm, _ = finalize_proof ~pm proof pinfo in
+  pm
 
 end (* Proof module *)
 

diff --git a/vernac/declare.mli b/vernac/declare.mli
@@ -308,10 +308,6 @@ module Proof : sig
   (** Requires a complete proof. *)
   val return_proof : t -> closed_proof_output
 
-  (** An incomplete proof is allowed (no error), and a warn is given if
-      the proof is complete. *)
-  val return_partial_proof : t -> closed_proof_output
-
   (** XXX: This is an internal, low-level API and could become scheduled
       for removal from the public API, use higher-level declare APIs
       instead *)
@@ -331,10 +327,7 @@ module Proof : sig
     : pm:OblState.t
     -> proof:proof_object
     -> idopt:Names.lident option
-    -> OblState.t * GlobRef.t list
-
-  (** Used by the STM only to store info, should go away *)
-  val get_po_name : proof_object -> Id.t
+    -> OblState.t
 
 end
 

diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
@@ -176,7 +176,7 @@ let interp_qed_delayed ~proof ~st pe =
       | Admitted ->
         Declare.Proof.save_lemma_admitted_delayed ~pm ~proof
       | Proved (_,idopt) ->
-        let pm, _ = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~idopt in
+        let pm = Declare.Proof.save_lemma_proved_delayed ~pm ~proof ~idopt in
         pm)
       pm
   in

diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
@@ -256,7 +256,6 @@ module Declare_ = struct
       res
 
   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 =
     NewProfile.profile "close_future_proof" (fun () ->

diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
@@ -136,7 +136,6 @@ module Declare : sig
       (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
 
   val return_proof : unit -> Declare.Proof.closed_proof_output
-  val return_partial_proof : unit -> Declare.Proof.closed_proof_output
 
   val close_future_proof
     : feedback_id:Stateid.t