Re: [isabelle] 2014-RC1 issues
- To: Peter Lammich <lammich at in.tum.de>
- Subject: Re: [isabelle] 2014-RC1 issues
- From: Makarius <makarius at sketis.net>
- Date: Fri, 1 Aug 2014 10:27:47 +0200 (CEST)
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <1406790685.2398.87.camel@lapbroy33>
- References: <1406708816.2398.53.camel@lapbroy33> <53D8DA09.firstname.lastname@example.org> <alpine.LNX.email@example.com> <1406790685.2398.87.camel@lapbroy33>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Thu, 31 Jul 2014, Peter Lammich wrote:
The invocation of error "" is the same as raise ERROR "", which makes the
ML code fail and the Isar toplevel wrapper print the exeptions. The error
message is empty, which means it is vacous according to ancient Isabelle
traditions, which hold until today. The effect was not visible in the old
TTY times, because that adds a prefix of "*** " by default. Note that
there are other situations where ML failure might lead to no error output,
notably involving Exn.Interrupt.
Such non-printing exceptions should not show up under normal circumstances
-- they indicate a programming mistake somewhere.
The question is "why are these errors/interrupts not visible?"
Interrupts are not program errors, but physical events. The
"implementation" manual explains the difference in the important section
0.5, with clear guidelines how user-space tools need to work with
interrupts, such that there are passed-through the code unhindered. The
system uses interrupts internally in various ways to manage executions,
but for this to work the user-space code needs to be done right.
ERROR "" used to be a semantic ML programming error until yesterday, when
I incorporated the concept into the "user error" notion to simplify life.
Regular Isabelle sources never suffered from that mistake in the past
decades to the best of my knowledge, but there is no problem here to make
the system more resiliant against improper use and declare it proper. So
in the next Isabelle2014-RC1 the error message will be "Error", both in ML
Nonetheless, it is important that Isabelle/ML users read the
implementation manual carefully, and more than just once in a life-time.
As discussed earlier on this list, they make false theorems look as if
proven, when the proof tactics contain an programming error (or fail due
to a bug in the parallel proof scheduling). This behaviour is contrary
to the spirit of LCF-provers.
The LCF approach in its strict sense is based on sucessully produced
values of some abstract datatype of theorems, not the absence of
There is a general problem to ensure that errors actually reach the
end-user -- despite continuous efforts to make this as robust as feasible,
there are routinely situations where messages get dropped, e.g. by odd
Java/Swing GUI components.
This inherent unreliability of prover interfaces is well-known, it was the
same in the old days of Proof General.
The only official authentic check is a batch build.
This archive was generated by a fusion of
Pipermail (Mailman edition) and