[isabelle-dev] Not (always) reported errors [was: New (Co)datatypes: Status & Plan 2]

[Dmitriy Traytel]

Am 20.11.2013 15:11, schrieb Jasmin Blanchette:
>> Dmitriy had sent me some explanations which sessions represent the material to be moved to HOL in either case, but I never tried it out myself.  It is high time to do that now.  In particularly I would like to get a feeling for HOL-Proofs.  We also had some obscure drop-outs in summer with TTY / Proof General, if that is still relevant.
> I seem to recall that the dropouts were in "HOL-BNF-Examples". This is of course suboptimal, but it isn't directly related to the move from "HOL-BNF" to "HOL".
If I understand him correctly, by drop-outs Makarius does not refer to 
HOL-Proofs but to two other issues that we ran into. Both issues are of 
the form that certain errors would not reach the human user. The errors 
were caused by (in the meantime resolved) programming errors in the BNF 
package. However the issues (not their cause) still persist in Isabelle.

I've minimized both (attached).

Issue1:
The theory is happily accepted by Isabelle/jEdit and Proof General, 
while the build system chokes on it. The problem is the attempt to prove 
the theorem in the wrong context.

However, I consider this a low precedence issue since it
* is discovered by the build system
* requires some Isabelle/ML
* occurs in Isabelle2013, Isabelle2013-1, and Isabelle/483131676087

Issue2 is perhaps slightly more severe:
With parallel proofs on this theory runs through (i.e. Isabelle/jEdit 
and build are satisfied by default). With parallel proofs off one gets 
an "unresolved flex-flex pair" (i.e. fails by default in Proof General). 
I'm not sure if the parallel mode is smashing the pairs or simply 
ignoring them (I hope the first).

Again this is not release-critical since it occurs in Isabelle2013, 
Isabelle2013-1, and Isabelle/483131676087.

Dmitriy

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Issue1.thy
Type: application/x-extension-thy
Size: 1133 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20131121/d8921ea4/attachment-0004.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Issue2.thy
Type: application/x-extension-thy
Size: 406 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20131121/d8921ea4/attachment-0005.bin>
-------------- next part --------------
session Issue1 = HOL +
  theories
    Issue1