diffs not shown when Coq is run completely silent

Open Flupp opened this issue 6 months ago • 1 comments

When coq-run-completely-silent is enabled, then coq-diffs has no effect and diffs are never shown.

When diffs are needed, coq-run-completely-silent can be disabled as a workaround.

When coq-run-completely-silent is enabled, Proof General requests goals explicitly via Show command, however, the output is then without diff markup. The Show Proof command (which displays the proof term; not the goal) has optional parameters for enabling printing with diff. There does not seem to be an equivalent for demanding a diff when explicitly showing goals.

Jun 23 '25 12:06 Flupp

See rocq-prover/rocq#20793; @Matafou @erikmd @cpitclaudel : maybe you are interested in leaving a comment in this rocq issue?

Jun 23 '25 21:06 hendriktews