Re: [isabelle] 2014-RC1 issues



> 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?" 
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. Moreover, if those things are programming
mistakes and should not show up under normal circumstances anyway, there
is no point in not highlighting them as an error.


--
  Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.