[isabelle-dev] Redundant equations in function declarations
makarius at sketis.net
Thu Jun 28 22:15:47 CEST 2012
On Sun, 3 Jun 2012, Alexander Krauss wrote:
> Technically, this situation represents a recoverable error (the
> definition and the rest of the theory can be processed), but always
> indicates a problem in the sources that should be fixed. It seems that
> we do not currently have a corresponding severity level. Therefore
> choosing between "ignored spam warning" and "break your leg error" is a
> bit difficult.
> - Do we need a level for such messages/annotations? In IDE terms, a
> little yellow triangle with an exclamation mark comes to my mind. I
> wouldn't want to see this for most iother warnings, but here it might
> make sense.
In principle the Prover IDE markup model supports arbitrary kinds of
messages and hilighting. Nonetheless one should reduce such things to the
bare minimum, such that tool authors still have a clear understanding what
is intended to be what message.
De-facto, the Isabelle/jEdit interpretation of plain-old warning and error
is slightly different than in Proof General:
* Warnings tend to be stronger, unlike PG where they often disappear.
* Errors tend to be weaker, because the (crude) recovery strategy will
skip over failed commands, and continue.
So yes, a duplicate constant definition is actually ignored.
> Is it already possible for a package to emit a message/report that
> carries position information, say to underline one of the clauses in a
> specification processed by read_specification? This could also improve
> the error reporting in other cases.
To affix messages to certain positions in the source one merely needs to
mention the position via Position.str_of somewhere in the message text.
This already works for approx. half of the prover messages.
For read_specification the position of the clauses in question are still
not passed through to the package. This will come some day, but needs at
least a tiny little bit of thinking, because clauses can conceptually
consist of several outer syntax term tokens (although that is not fully
implemented right now).
More information about the isabelle-dev