Thank you for investigating. I have been waiting for Alex to present
his view.
Sorry for being late. I've been offline for some days and am a bit
behind now :-)
Naturally, the current treatment resembles ML's.
Yes. I don't think there were any further considerations.
[...]
There is no reason to allow a specification to contain material that
may contradict another part of the specification.
Well, the meaning of an equation in the "fun" command is: If the
equation overlaps with a previous one, consider just the
non-overlapping part. And your proposed change would be an exception
to this rule.
It does not happen very often, but I have occasionally written thing
like this myself in intermediate experimentation stages. Eventually, I
clean things up of course, but having a hard error would force me to
comment out more stuff temporarily...
But I understand your concerns.
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.
Questions:
- 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.
- @Larry: Do you think your students would have noticed it if the
redundant equations had been underlined in yellow?
- @Makarius: 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.
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
