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 here:

  * 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 somewhere else.

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 MHonArc.