Opened 11 years ago

Closed 9 years ago

#463 closed defect (fixed)

Warning messages suppress error messages and make PG have incorrect behavior with Coq

Reported by: coquser Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.3
Component: 2:pg-emacs Keywords:
Cc:

Description

The code

Local Reserved Notation "'Ω'".

Record foo := {

A : Set where "'Ω'" := A; B : 1 = true

}.

"compiles" in ProofGeneral with "Warning: This notation will not be used for printing as it is bound to a single variable", while it should fail with a type error.

Change History (7)

comment:1 Changed 11 years ago by coquser

Probably related to coqtop sending the warning message to stderr and the error message to stdout. -- Dan Grayson

comment:2 Changed 11 years ago by coquser

The given code produces an error and a warning, the warning starts with a character 0xFE and ends with 0xFF. Therefore the warning matches as urgent message. Because PG recognizes only errors that follow urgent messages, the error ist lost.

Not sure how to fix this.

Hendrik

comment:3 Changed 11 years ago by coquser

I've posted a bug report at https://coq.inria.fr/bugs/show_bug.cgi?id=3013, as well.

-Jason

comment:4 Changed 11 years ago by coquser

I am sorry for the confusion. It is not the message that needs to get changed in coq. Either the regular expressions for urgent messages in coq Proof General should be changed, such that the notation warning is not matched any more. Or, Proof General should be changed, such that it recognizes errors before urgent messages.

As you might have guessed by now, we have some support problem for coq Proof General at the moment, see http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2013/000304.html

Bye,

Hendrik

comment:5 Changed 11 years ago by coquser

Ah, ok. Over at the coq bugs list, they said:

Pierre-Marie Pédrot 2013-03-28 18:16:52 CET The way ProofGeneral discusses with Coq is outdated, as it is based on regexps to parse Coq answers. This is not reliable nor robust, as you mention.

As a general workaround to the type of problem you're describing, we need to find a volunteer to port ProofGeneral to the new XML messaging protocol used by CoqIDE since v8.4.

If ever you're interested...

-Jason

comment:6 Changed 11 years ago by coquser

There is a note in the coq bug tracker saying that the order of the warning and error message changed in the trunk version for this case. I therefore suggest to leave this bug open until the next coq version fixes it.

Hendrik

comment:7 Changed 9 years ago by courtieu

Resolution: fixed
Status: newclosed

This is fixed for v8.5 and trunk. Probably by the fixes I made in error processing some month ago.

Note: See TracTickets for help on using tickets.