Make "Set Ltac Debug" work

[coquser]

When Proof General attempts to handle compound tactics in debug mode, it freezes. If you switch to the *coq* buffer, you find that Coq has switched into an interactive mode, but there is no indication of this in the UI.

[David Aspinall]

Could you give a bit more of a description of what you want to be fixed/added, please?

[coquser]

Consider the following proof script:

Set Ltac Debug.
Goal True \/ True.
  constructor; auto.

When Proof General attempts to handle the compound tactic 'constructor; auto', it freezes. If you switch to the *coq* buffer, you find that Coq has switched into an interactive mode, but there is no indication of this in the UI. A good first step would be to automatically switch buffers when coqtop decides it needs extra user input.

Now, consider what happens if I retract my buffer past 'Set Ltac Debug', delete the line, and then attempt to run the proof. I'm still in debug mode. I need to explicitly 'Unset Ltac Debug'. This should not be necessary.

Those are probably the main things. Since you have a full UI, it might be easier to implement an interface that keeps track of previous information better than just a write-only terminal app could.

[David Aspinall]

Thanks for the extra info. Once upon a time there was an interactive debug facility just like this for Isabelle, taken from ​Isamode. But it seemed to be unused.

From a quick test, switching to the *coq* buffer automatically looks like it would be useful, indeed, I'll see if we can add a facility for this. But note that the *coq* buffer is quite limited as a shell, it deliberately cuts out a lot of the facility available in Emacs shell mode such as history, etc (for efficiency).

For undo of the Set LTac Debug command, the flag state handling needs some cleaning up between PG and Coq, these days it seems some flags state changes are stored in the undo history and some not. Somebody needs to look at this properly and figure out which ones really should be stored in the history/buffer and which not, and how to keep things in sync when they are.

[coquser]

Yeah. While debugging seems useful (and can be pretty useful for beginners), a lot of veteran Coq users think that the debugging toolchain just doesn't work that well (and end up copy-pasting their tactics into their proof script, translating semicolons into periods, so that they can take advantage of forwards and backwards motion, etc.) So while what I have described is the bare minimum to make this work, there's a lot more that can be done.

[coquser]

The coq bug ​http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2422 is related to this.

I wonder though, if it would make more sense to change the behavior of options based on whether they were entered into a script, or triggered through the UI. This could be handled by using a different syntax to set options from the UI. I suggest this, since I found when using the UI to set printing states, they ended up getting out-of-sync, since they get reset as I backtracked.

[David Aspinall]

Thanks for the follow up pointer.

Your suggestion sounds good, I think, if I've understood it right: you suggest having a different syntax for the commands when they are not written in the script, e.g.

Interface Set Ltac Debug

which would suggest that the effect of Set Ltac Debug should not be recorded in the history.

This sounds sensible, and it would be easy to adapt Proof General to use that form from the menus etc. Would you propose it to the Coq developers?

Of course, state changes when the user writes plain Set Ltac Debug in the proof script would not be reflected in the UI without an extra mechanism. (By the way, that extra mechanism is provided for in Proof General and is used with Isabelle, which can update the interface's view of flags and settings).

[David Aspinall]

The UI will now switch to display the *coq* window when debugging. (The flag state issue is not addressed by this fix).