diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-10-04 10:13:56 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-04 10:13:56 +0200 |
commit | cf39d22df11bc33d393db42dfd4b5b0a2c8ded16 (patch) | |
tree | 954aad51e5b2190f9d3453aeebfbc85a2ea7da0c /stm | |
parent | d23df0ac40122ce2fb42683fce00f60fb85eaff9 (diff) | |
parent | ec59306708f9aec04ab82a7e03807017e1924507 (diff) |
Merge PR #1096: [stm] Warn about costly Undo operations in batch mode [BZ#5677]
Diffstat (limited to 'stm')
-rw-r--r-- | stm/stm.ml | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 7c44fc86f..984a87429 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 -> |