Email Gateway (Aug 22 2022 at 12:33): Email Gateway (Aug 22 2022 at 12:33):From: "C. Diekmann" <diekmann@in.tum.de>
Hi,
I discovered an error reporting behavior of isabelle that might be misleading.
Assume I have a file bar.thy.
The file contains
theory foo
imports
Main
begin
end
In the output field, I get the expected error message:
Bad theory name "foo" for file "bar.thy"
However, if I change the file to the following, the error reporting
gets misleading:
theory foo
imports
Main
begin
baz
end
Now jEdit presents a red exclamation mark right next to "baz" and the error is:
Outer syntax error⌂: command expected,
but identifier baz⌂ was found
The error about the bad theory name is no longer reported.
Expected behavior: The first error is the wrong theory name and should
be reported first.
Circumstances how I triggered this:
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.
Best Regards
Cornelius
Email Gateway (Aug 22 2022 at 12:47):From: Makarius <makarius@sketis.net>
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.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC