Re: [isabelle] Isabelle2016-RC2 -- Misleading error message if bad theory name in addition to error in theory
On Mon, 1 Feb 2016, C. Diekmann wrote:
Expected behavior: The first error is the wrong theory name and should
be reported first.
The system disagrees with the user about what is the first error. This
effect occasionally happens with malformed input. It is particularly
critical for the theory header, but I can imagine many other improvements
* automatically create a well-formed header (template) for new files
* provide hyperlinks to theory imports
* remind the user of hard and fast naming conventions for theory names
(capitalized words, usually in singular, separated by underscore)
I triggered this behavior when I copy-pasted a theory. The theory had
many other theories imported. One of them defined the command "baz".
Because of the bad theory name, jEdit did not load the theory which
defined "baz". But jEdit displayed an error at baz. It took a few
minutes of debugging the call to baz to figure out that the error was
Variations on that confusion can happen. In the past, the system would
pretend that all commands are always defined. Now it requires proper
theory imports to have commands in the theory body.
None of this is a regression wrt. Isabelle2015. So these observation are
stacked on the pile of possible improvements for future releases.
This archive was generated by a fusion of
Pipermail (Mailman edition) and