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!