Re: [isabelle] 2014-RC1 issues

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 and Scala.

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 user-level errors.

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 MHonArc.