Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]

2 files changed, 17 insertions, 1 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index 7c44fc86fb..984a874296 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1044,8 +1044,18 @@ end = struct (* {{{ *)
         match f acc (id, vcs, ids, tactic, undo) with
         | `Stop x -> x
         | `Cont acc -> next acc
- 
+
+  let undo_costly_in_batch_mode =
+    CWarnings.create ~name:"undo-batch-mode" ~category:"non-interactive" Pp.(fun v ->
+        str "Command " ++ Ppvernac.pr_vernac v ++
+        str (" is not recommended in batch mode. In particular, going back in the document" ^
+             " is not efficient in batch mode due to Coq not caching previous states for memory optimization reasons." ^
+             " If your use is intentional, you may want to disable this warning and pass" ^
+             " the \"-async-proofs-cache force\" option to Coq."))
+
   let undo_vernac_classifier v =
+    if !Flags.batch_mode && !Flags.async_proofs_cache <> Some Flags.Force
+    then undo_costly_in_batch_mode v;
     try
       match v with
       | VernacResetInitial ->
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4b97ee0dde..b0f021cdcd 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -132,10 +132,16 @@ let rec interp_vernac sid (loc,com) =
          highly dynamic and depends on the structure of the
          document. Hopefully this is fixed when VtBack can be removed
          and Undo etc... are just interpreted regularly. *)
+
+      (* XXX: The classifier can emit warnings so we need to guard
+         against that... *)
+      let wflags = CWarnings.get_flags () in
+      CWarnings.set_flags "none";
       let is_proof_step = match fst (Vernac_classifier.classify_vernac v) with
         | VtProofStep _ | VtBack (_, _) | VtStartProof _ -> true
         | _ -> false
       in
+      CWarnings.set_flags wflags;
 
       let nsid, ntip = Stm.add ~ontop:sid (not !Flags.quiet) (loc,v) in