[isabelle-dev] Local Specification Mechanisms: Brief Experience Report

[Makarius]

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.


 	Makarius