On Tue, 29 May 2012, Lawrence Paulson wrote:
I am marking some student work submitted for the Cambridge Isabelle
course, and have seen some examples where students have gone terribly
wrong because they overlooked the warning “Ignoring redundant equation"
in a function definition. This sort of mistake could happen to anybody,
and it means that proofs are being undertaken on the basis of a mistaken
definition. Somebody reading the theory could also overlook this
mistake, which goes against the idea that structured proofs should be
readable without being executed.
I propose that this particular warning should become a fatal error.
I cannot say anything specific about the function package -- by default
such things are done the right way, until someone who really understands
it says something else.
Generally the issue of different degrees of warnings vs. errors is a very
old one, and used to be intertwined with the infathomable ways of Proof
General filtering and rearranging prover messages. In Isabelle/jEdit the
rules are a bit different, more close to the real output of the prover
(which can be sometimes confusion for other reasons).
Anyway, in our recent Isabelle tutorial, I was surprised how well the
current scheme of warnings or errors of the main packages already works in
typical theory development, e.g. when datatype constructors are added or
removed, and consecutive function definitions (and proofs) need to be
adapted.
The warnings were shown nicely in the Prover IDE, although some fine
points still need to be addressed. It is better to invest the time here,
than to optimize for the old Proof General model, which tends to require
more rudeness for messages to be seen by the user.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
