This is cross-posted from StackOverflow, FYI. I have a tactic whose expected behavior is to output an error message, and I want to run it in batch mode on a series of goals and for each goal, I want to record the goal and the error message from the tactic. It seems like I can’t do this with coqc since it will not continue on failure, so I’m doing this on Coqide. The closest I’ve been able to come to a solution is to have my file to have goals that look like this:
Theorem/Lemma blah.
Proof. Show. my_tactic. Admitted.
The first problem with this is that Show doesn’t retain the proof goals in the Messages tab of Coqide through the run of the file, and the second is that while the output of the tactic is retained in the Errors tab, I am not able to copy it. Any help would be appreciated. Thanks!