[isabelle-dev] Local Specification Mechanisms: Brief Experience Report
makarius at sketis.net
Fri Dec 17 15:58:34 CET 2010
On Fri, 17 Dec 2010, Tjark Weber wrote:
> So here's an attempt:
> | Sorry, Isabelle cannot establish the requested sublocale relationship
> | because the effected chain of interpretations would be too long.
> | Please try to establish a different sublocale relationship.
> | Section 7.1 of the Tutorial to Locales and Locale Interpretation
> | provides further information on how to avoid infinite chains of
> | interpretations.
This kind of error message would be outdated and misleading in a very
short time. We also have an internal collection of jokes about packages
that were a bit too chatty, pretending to know what the user needs to do
in a certain situation. The principles of modularity, maintainability etc.
need to be applied to error messages, too.
More information about the isabelle-dev