On Mon, 22 Aug 2011, Brian Huffman wrote:
Isabelle prints out warning messages whenever anyone declares a
duplicate simp rule, intro rule, etc. It would be nice if Isabelle would
print a similar warning whenever a definition reuses a name that is
already in scope in the current context. For example, if a theory
defines a class like this...
class complete_boolean_algebra = distributive_complete_lattice +
boolean_algebra
...and a class called "complete_boolean_algebra" is already in scope,
then a warning message ought to be printed.
Such a warning message would be useful for constant names, lemma names,
etc. as well.
When I've seen the "complete_boolean_algebra" incident on the other thread
my first impulse was to check how far the wiring of the class package wrt.
the Isabelle document markup was. In principle the prover can provide
useful clues in non-intrusive ways here, if done right. E.g. in
Isabelle/jEdit one can hover over the text with COMMAND/CONTROL to ask
"What is this?" and often get useful feedback already.
Unfortunately, the class package is still in a confusing state here, so I
did not even put it on the list of things to be done, because it is just
another instance of similar ongoing reforms, and there are so many really
pressing things in the pipeline. (Quite a bit has happened here already,
like purging the name space module from historic cruft one more time, and
assembling all syntax layers clearly in one place.)
Anyway, your above idea of "warning whenever a definition reuses a name
that is already in scope in the current context" does not really remind me
of how this works internally. What means "name" here? E.g. a package
defining some "induct" rule is perfectly right to do so in the presence of
another "induct", as long as additional name qualification makes things
clear to the system and the user.
We have reasonably well-established concepts of "binding", "naming", and
"morphisms" on bindings. Any new feature somehow needs to fit smoothly
into the picture. Also note that a special twist is the name space merge
that happens at theory import time: independent specifications can
silently cause a conflicting situation in the application context.
What could work, and is on my list for a long time already, is to give
some feedback in situations where *ambiguity* occurs in name space
resolution. This would also follow the intention behind the names_unique
(formerly unique_names) option, only that the prover would show such spots
spontaneously and non-intrustively whenever they appear in input or
output, both in defining and referencing positions. (BTW, in Scala
ambiguity after additional imports is treated as an error, and causes the
conflicting name entries to be canceled out.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
