Emilio Jesús Gallego Arias (Apr 13 2021 at 22:37): Emilio Jesús Gallego Arias (Apr 13 2021 at 22:37):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.
Jason Gross (Apr 14 2021 at 00:13):@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.
Emilio Jesús Gallego Arias (Apr 14 2021 at 13:36):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: Apr 18 2024 at 22:02 UTC