On Tue, 29 May 2012, Makarius wrote:
On Tue, 29 May 2012, Lawrence Paulson wrote:
I'm not talking about user interfaces or models. I am saying that function
definitions containing entirely redundant equations should be rejected,
also in batch mode.
Maybe you can do some routine investigations why the current situation
(63021e59cbf0) of the function package is the way it is.
I've now spent myself the canonical 10 min looking through the history.
The relevant changesets are:
changeset: 24356:65fd09a7243f
user: krauss
date: Mon Aug 20 20:36:19 2007 +0200
files: src/HOL/Tools/function_package/fundef_datatype.ML
description:
issue a warning, when encountering redundant equations (covered by
prece3ding clauses)
changeset: 42947:fcb6250bf6b4
user: krauss
date: Sun May 22 20:59:13 2011 +0200
files: src/HOL/Tools/Function/fun.ML
description:
fun command produces warning when patterns are incomplete (somewhat
analogous to primrec)
This does not say anything special, just that Alex Krauss added the
warning in an early version of the function package in 2007, and did not
remove or change it in a more recent refinement in 2011. Maybe it just
imitates the way of ML.
So I continue not claiming any expertise on this specific detail of the
function package.
Generally, the best "strength" of messages by the system is difficult to
determine. Proof General and the OCaml toplevel are very rude in the
sense that they stop at the first hard error. Compared to that, Poly/ML
is much better at error recovery, say to present a partially type-checked
piece of source with IDE markup. (I've recently shown the Isabelle/ML IDE
to some local OCaml experts and they were quite impressed by the quality
of the feedback from its static analysis produced in real time as the user
types the text.)
The Isabelle Prover IDE for logical part is still a bit crude here: it
skips over failed commands and retains any of the markup produced so far.
This also means a hard error is not so hard after all, and can sometimes
cause more confusion than a soft one, because the binding of the formal
entity to be defined will be absent from the context. Thus the scoping in
later text can change unexpectedly for the user: e.g. a bad function "foo"
used later in formal text becomes a free variable (luckily with the Haribo
color effect, which will gradually include more and more details about
scopes etc.)
So far I've only fine-tuned some messages sporadically, whenever grossly
confusing situations have shown up. Often it just means to propagate the
formal position information correctly. The basic interaction model and
the possibilities for extra markup are very relevant to get this right.
Optimizing for Proof General is different than optimizing for
Isabelle/jEdit. (Anyway, does anybody step forward to continue
maintenance of Isabelle Proof General?)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
