Warnings missing in proof mode in Coq

[Evgeny Makarov]

Dear Proof General Developers,

When Coq issues a warning inside a proof, PG shows the warning in the minibuffer, but it does not show the resulting goal.

For example:

Goal True /\ True -> True.
intro H.
destruct H as [H1 H2 H3].

After the last command, the minibuffer contains "[Coq] Warning: Unused introduction pattern : H3", but the *response* buffer is empty. The same happens if I process

Require Import Setoid.
Goal False.
setoid_replace False with True.

The minibuffer contains a truncated warning "[Coq] Warning: There are several relations of the carrier 'Prop'. The relation (P", but the response buffer is again empty.

I am not sure what the correct behavior in this case should be (should PG display the warning *and* the goal?), but the goal should probably be displayed.

I am using CVS snapshot of PG updated on September 3, 2007 and Coq trunk 10056.

Thank you, Evgeny

[David Aspinall]

Thanks for raising this and sending the test cases.

I've tested with CVS PG, Coq 8.1, Emacs 22.1.1 but there I cannot reproduce the problem: the warning message and the goal are both displayed, which is the correct behaviour I think. So I assume the problem is with recent changes in Coq source repository.

PG is quite sensitive to the order and markup on output messages, which has been designed a long time ago with convenient conventions (e.g. to suppress long outputs from the prover), so this might be easily broken by reversing the order of outputs. The documentation of `proof-shell-filter' explains the strategy, see the Proof General adapting manual.

By the way, to see both messages at once you need to enable three window mode:

  Proof General -> Options -> Display -> Use Three Panes

or if you prefer the two window mode, use C-c C-o to rotate the output buffers (also under Buffers on the PG menu).