[vernac] Pass control attributes to interpretation of delayed proofs.

Fixes #10452

3 files changed, 72 insertions, 32 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index fb1c91b8af..17cef26997 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1054,9 +1054,9 @@ end = struct (* {{{ *)
 end (* }}} *)
 
 (* Wrapper for the proof-closing special path for Qed *)
-let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc pending : Vernacstate.t =
+let stm_qed_delay_proof ?route ~proof ~info ~id ~st ~loc ~control pending : Vernacstate.t =
   set_id_for_feedback ?route dummy_doc id;
-  Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ?loc:loc pending
+  Vernacentries.interp_qed_delayed_proof ~proof ~info ~st ?loc:loc ~control pending
 
 (* Wrapper for Vernacentries.interp to set the feedback id *)
 (* It is currently called 19 times, this number should be certainly
@@ -1532,7 +1532,7 @@ end = struct (* {{{ *)
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           stm_qed_delay_proof ~st ~id:stop
-            ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc (Proved (opaque,None))) in
+            ~proof:pobject ~info:(Lemmas.Info.make ()) ~loc ~control:[] (Proved (opaque,None))) in
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
@@ -1683,7 +1683,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 ~info ~loc (Proved (opaque,None)));
+      ignore(stm_qed_delay_proof ~id:stop ~st ~proof ~info ~loc ~control:[] (Proved (opaque,None)));
       `OK proof
       end
     with e ->
@@ -2352,7 +2352,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
      believe as proof injection shouldn't happen here. *)
   let extract_pe (x : aast) =
     match x.expr.CAst.v.expr with
-    | VernacEndProof pe -> pe
+    | VernacEndProof pe -> x.expr.CAst.v.control, pe
     | _ -> CErrors.anomaly Pp.(str "Non-qed command classified incorrectly") in
 
   (* ugly functions to process nested lemmas, i.e. hard to reproduce
@@ -2487,7 +2487,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                     if not delegate then ignore(Future.compute fp);
                     reach view.next;
                     let st = Vernacstate.freeze_interp_state ~marshallable:false in
-                    ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x));
+                    let control, pe = extract_pe x in
+                    ignore(stm_qed_delay_proof ~id ~st ~proof ~info ~loc ~control pe);
                     feedback ~id:id Incomplete
                 | { VCS.kind = `Master }, _ -> assert false
                 end;
@@ -2527,7 +2528,8 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
                 let _st = match proof with
                   | None ->  stm_vernac_interp id st x
                   | Some (proof, info) ->
-                    stm_qed_delay_proof ~id ~st ~proof ~info ~loc (extract_pe x)
+                    let control, pe = extract_pe x in
+                    stm_qed_delay_proof ~id ~st ~proof ~info ~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/vernacentries.ml b/vernac/vernacentries.ml
index 2c55f73a88..74438f3c16 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2249,7 +2249,33 @@ let locate_if_not_already ?loc (e, info) =
   | None   -> (e, Option.cata (Loc.add_loc info) info loc)
   | Some l -> (e, info)
 
-exception End_of_input
+let mk_time_header ~vernac =
+  let pr_time_header vernac =
+    (* Drop the time header to print the command, we should indeed use a
+       different mechanism to `-time` commands than the current hack of
+       adding a time control to the AST. *)
+    let vernac = match vernac with
+      | { v = { control = ControlTime _ :: control; attrs; expr }; loc } ->
+        CAst.make ?loc { control; attrs; expr }
+      | _ -> vernac
+    in
+    Topfmt.pr_cmd_header vernac
+  in
+  Lazy.from_fun (fun () -> pr_time_header vernac)
+
+let interp_control_flag ~time_header (f : control_flag) ~st
+    (fn : st:Vernacstate.t -> Vernacstate.LemmaStack.t option) =
+  match f with
+  | ControlFail ->
+    with_fail ~st (fun () -> fn ~st);
+    st.Vernacstate.lemmas
+  | ControlTimeout timeout ->
+    vernac_timeout ~timeout (fun () -> fn ~st) ()
+  | ControlTime batch ->
+    let header = if batch then Lazy.force time_header  else Pp.mt () in
+    System.with_time ~batch ~header (fun () -> fn ~st) ()
+  | ControlRedirect s ->
+    Topfmt.with_output_to_file s (fun () -> fn ~st) ()
 
 (* EJGA: We may remove this, only used twice below *)
 let vernac_require_open_lemma ~stack f =
@@ -2640,6 +2666,8 @@ and interp_expr ~atts ~st c =
    without a considerable amount of refactoring.
 *)
 and vernac_load ~verbosely fname =
+  let exception End_of_input in
+
   (* Note that no proof should be open here, so the state here is just token for now *)
   let st = Vernacstate.freeze_interp_state ~marshallable:false in
   let fname =
@@ -2673,23 +2701,16 @@ and vernac_load ~verbosely fname =
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
   ()
 
-and pop_control cl = CAst.map (fun cmd -> { cmd with control = cl })
-and interp_control ~st ({ v = cmd } as vernac) = match cmd.control with
-  | [] ->
-    let before_univs = Global.universes () in
-    let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
-    if before_univs == Global.universes () then pstack
-    else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack
-  | ControlFail :: cl ->
-    with_fail ~st (fun () -> interp_control ~st (pop_control cl vernac));
-    st.Vernacstate.lemmas
-  | ControlTimeout timeout :: cl ->
-    vernac_timeout ~timeout (interp_control ~st) (pop_control cl vernac)
-  | ControlRedirect s :: cl ->
-    Topfmt.with_output_to_file s (interp_control ~st) (pop_control cl vernac)
-  | ControlTime batch :: cl ->
-    let header = if batch then Topfmt.pr_cmd_header vernac else Pp.mt () in
-    System.with_time ~batch ~header (interp_control ~st) (pop_control cl vernac)
+and interp_control ~st ({ v = cmd } as vernac) =
+  let time_header = mk_time_header ~vernac in
+  List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
+    cmd.control
+    (fun ~st ->
+       let before_univs = Global.universes () in
+       let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
+       if before_univs == Global.universes () then pstack
+       else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack)
+    ~st
 
 let () =
   declare_int_option
@@ -2714,16 +2735,32 @@ let interp ?(verbosely=true) ~st cmd =
     Vernacstate.invalidate_cache ();
     iraise exn
 
-let interp_qed_delayed_proof ~proof ~info ~st ?loc pe : Vernacstate.t =
+(* Interpreting a possibly delayed proof *)
+let interp_qed_delayed ~proof ~info ~st pe : Vernacstate.LemmaStack.t option =
   let stack = st.Vernacstate.lemmas in
   let stack = Option.cata (fun stack -> snd @@ Vernacstate.LemmaStack.pop stack) None stack in
+  let () = match pe with
+    | Admitted ->
+      save_lemma_admitted_delayed ~proof ~info
+    | Proved (_,idopt) ->
+      save_lemma_proved_delayed ~proof ~info ~idopt in
+  stack
+
+let interp_qed_delayed_control ~proof ~info ~st ?loc ~control pe : Vernacstate.t =
+  let vernac = CAst.make ?loc { control; attrs = []; expr = VernacEndProof pe } in
+  let time_header = mk_time_header ~vernac in
+  let stack =
+    List.fold_right (fun flag fn -> interp_control_flag ~time_header flag fn)
+      control
+      (fun ~st -> interp_qed_delayed ~proof ~info ~st pe)
+      ~st
+  in
+  Vernacstate.Proof_global.set stack [@ocaml.warning "-3"];
+  Vernacstate.freeze_interp_state ~marshallable:false
+
+let interp_qed_delayed_proof ~proof ~info ~st ?loc ~control pe : Vernacstate.t =
   try
-    let () = match pe with
-      | Admitted ->
-        save_lemma_admitted_delayed ~proof ~info
-      | Proved (_,idopt) ->
-        save_lemma_proved_delayed ~proof ~info ~idopt in
-    { st with Vernacstate.lemmas = stack }
+    interp_qed_delayed_control ~proof ~info ~st ?loc ~control pe
   with exn ->
     let exn = CErrors.push exn in
     let exn = locate_if_not_already ?loc exn in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index e618cdcefe..ad5a849fed 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -18,6 +18,7 @@ val interp_qed_delayed_proof
   -> info:Lemmas.Info.t
   -> st:Vernacstate.t
   -> ?loc:Loc.t
+  -> control:Vernacexpr.control_flag list
   -> Vernacexpr.proof_end
   -> Vernacstate.t