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
comment:2 Changed 11 years ago by
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
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
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
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
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
Resolution: | → fixed |
---|---|
Status: | new → closed |
This is fixed for v8.5 and trunk. Probably by the fixes I made in error processing some month ago.
Probably related to coqtop sending the warning message to stderr and the error message to stdout. -- Dan Grayson