The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 06/15/2016 06:39 PM, Pierre Courtieu wrote:
> Supporting Ltac debug mode would be good.

On 2016-06-15 18:44, Murali Vijayaraghavan wrote:
> I second this :) At least I can figure out what to do with it then!

On 2016-06-15 19:34, Jonathan Leivent wrote:
> Does anyone use that?  I find it unhelpful.

Not so fast :) Pierre (kudos btw!) has recently pushed improvements to PG 
that at least show the goal as it evolves through your debugging session, so 
at the very least (in 8.5) it's a good tool to step through the execution of 
a tactic and see the successive goals (IMHO it looks very nice).

I talked to various people at the DeepSpec meeting about having a more 
powerful Ltac debugger. One of the big challenges is collecting 
source-line-level information, so that one can step around. Once we have that 
info, though, it should be a breeze to connect it to a package like realgud 
(https://github.com/realgud/realgud). Then it would be very very nice, I 
think.

So I'd definitely think it's a good thing to keep in mind :)

Attachment: signature.asc
Description: OpenPGP digital signature