diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-26 00:57:41 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-27 18:13:20 +0200 |
commit | ec59306708f9aec04ab82a7e03807017e1924507 (patch) | |
tree | a3b4389c365def2f85eaabc66e1f08d82c516d66 | |
parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) |
[stm] Warn about costly Undo operations in batch mode [BZ#5677]
Undo & friends is very expensive in batch mode as backtracking state
is not kept and thus should be recomputed.
We thus warn the user.
-rw-r--r-- | stm/stm.ml | 12 | ||||
-rw-r--r-- | toplevel/vernac.ml | 6 |
2 files changed, 17 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e0064df9b..08f6de693 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 4b97ee0dd..b0f021cdc 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 |