diff options
| author | Pierre-Marie Pédrot | 2020-05-03 14:24:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-03 14:24:43 +0200 |
| commit | 3452a14b58ab88af686d3006b843bc064ab8f911 (patch) | |
| tree | 01a6055b63e13e313e211a7b4ffc15bdc1ca0aaf /doc | |
| parent | 16b2734e050d4c28d5da1a509cd2387cb8cebe6b (diff) | |
| parent | 9b937b6f53c5e97faa5c7949e6032837f8708761 (diff) | |
Merge PR #12197: LtacProf now handles multi-success backtracking
Ack-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 18 |
2 files changed, 20 insertions, 6 deletions
diff --git a/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst new file mode 100644 index 0000000000..b90c8e7a1f --- /dev/null +++ b/doc/changelog/05-tactic-language/12197-ltacprof-multi-success.rst @@ -0,0 +1,8 @@ +- **Fixed:** + The :flag:`Ltac Profiling` machinery now correctly handles + backtracking into multi-success tactics. The call-counts of some + tactics are unfortunately inflated by 1, as some tactics are + implicitly implemented as :g:`tac + fail`, which has two + entry-points rather than one (Fixes `#12196 + <https://github.com/coq/coq/issues/12196>`_, `#12197 + <https://github.com/coq/coq/pull/12197>`_, by Jason Gross). diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 8418e9c73d..b184311bef 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1786,16 +1786,22 @@ performance issue. and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. +.. warn:: Ltac Profiler encountered an invalid stack (no \ + self node). This can happen if you reset the profile during \ + tactic execution + + Currently, :tacn:`reset ltac profile` is not very well-supported, + as it clears all profiling information about all tactics, including + ones above the current tactic. As a result, the profiler has + trouble understanding where it is in tactic execution. This mixes + especially poorly with backtracking into multi-success tactics. In + general, non-top-level calls to :tacn:`reset ltac profile` should + be avoided. + You can also pass the ``-profile-ltac`` command line option to ``coqc``, which turns the :flag:`Ltac Profiling` flag on at the beginning of each document, and performs a :cmd:`Show Ltac Profile` at the end. -.. warning:: - - Note that the profiler currently does not handle backtracking into - multi-success tactics, and issues a warning to this effect in many cases - when such backtracking occurs. - Run-time optimization tactic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |