[isabelle-dev] NEWS -> Redundant lemmas
makarius at sketis.net
Fri Sep 23 00:03:10 CEST 2011
On Thu, 22 Sep 2011, Brian Huffman wrote:
> I actually like Peter's idea of a "deprecated" flag better than my
> Legacy.thy idea. We might implement it by adding a new "deprecated" flag
> to each entry in the "naming" type implemented in
> Pure/General/name_space.ML. Deprecated names would be treated
> identically to non-deprecated names, except that looking up a deprecated
> name would cause a legacy warning message to be printed. I don't think
> it would be necessary to modify any other tools or packages.
> Of course, we'd also need to invent some interface for marking names as
> deprecated in the first place. It might also be nice to associate a text
> string to each deprecated name (perhaps saying what other name/feature
> to use instead) instead of just using a boolean flag.
This would be the basic plan, but it also needs to be wired up with the
Prover IDE protocol and stylesheets (which are still only half finished).
The part about the name space is relatively easy, but the "annotation"
part in the source text requires some further thoughts. Concerning the
extra text, the attitude in PIDE is to point to the original source for
additional information. There could be a semi-formal comment telling the
user, maybe as simple as the existing "-- cmt" form. (Some people in
Edinburgh have proposed "social tagging" :-)
Anyway, I am the one who is responsible for these parts of the system. It
is old wisdom in Isabelle develoment (with its 25 years) that it is more
efficient to consult the experts and main responsable persons for each
particular component, instead of tinkering oneself. (The latter has
occasionally happened, either leading to code in terminal condition that
nobody undertstands anymore, or forcing some poor fellow to re-engineer it
from the ground up. For the name space module both has happened in
variations several times already.)
More information about the isabelle-dev