Hi @Jason Gross , I'm not sure I understood why you need
Set Ltac Debug to work on
coqc, would you mind expanding a bit more?
[apologies in advance if you already did, the corresponding PR is beyond what github's interface can handle]
It is OK indeed to keep that behavior for
coqc if you need it, however it feels weird that coqc would hang expecting user input in that case.
@Emilio Jesús Gallego Arias One of the most common use cases is to debug a tactic script that some PR broke. I will
Set Ltac Debug. Set Ltac Batch Debug. above the relevant automation, build the dependencies with both versions of Coq (the working and the non-working), and then pipe the output of coqc on this file to logs for both versions. Then I can use a differ to tell me exactly where the first change in behavior is. (This does not work very well for widely separated versions of Coq, when there are likely to be changes in spacing, universe numbering, etc, but it works well for versions separated only by a couple of commits.) I am fine with it being an error to run any tactic under
Set Ltac Debug without
Set Ltac Batch Debug in
coqc, and I'm also fine with having
Set Ltac Debug imply
Set Ltac Batch Debug for coqc; I do not need the interactivity, but being able to pipe the full trace to a file is essential.
Understood, I don't think there is a problem with that. I guess we could tho make the setup a bit cleaner and have
Set Ltac Debug and
Set Ltac Batch Debug to be two independent options.
Last updated: Oct 21 2021 at 19:03 UTC