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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and