The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

> On Sun, Jun 16, 2013 at 1:20 AM, Math Prover 
> <mathprover AT gmail.com>
>  wrote:
> Hi,

>  I've installed proof-general and set "Set Ltac Debug." This is the results 
> from just hitting <enter>. Can someone help me get started on debugging 
> this? (This is installed on a separate machine; it has Coq 8.4pl2 compiled 
> from source; but not access to CpdtTactics).

Hi,
On this particular point: the debugging mode has no real support, you
can just go to the *coq* buffer and use it as if you were using coq
from a terminal. This is not very handy but at least it works. The
whole workflow for debugging is:

1) go to the line before the tactic call you want to debug.
2) On the line before the tactic, write "Set Ltac Debug." and script it.
3) script the tactic, the "queued region" now covers your tactic but
it is not transformed in to a "locked region". scripting is freezed
4) switch to the *coq* buffer, go to the end and use the debugger
commands directly in this buffer ("h" for help).

When you want to go back to scripting:
5) go back to the script buffer
6) If the debugged tactic is not finished, abort it with "Proof
General -> interrupt prover", you can safely go back or forward but
beware that you are still in debug mode.

When you want to stop debugging mode (since the debug mode is not
synchronized with the state of the prover, going back and deleting the
Set Ltac Debug is not enough)
7) script back to "Set Ltac Debug"
8) edit it to "Unset Ltac Debug" and script it
9) you are back in non debugging mode, you can script back and remove
theUnset Ltac Debug  line.

Hope this helps.
Pierre