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

[Makarius]

On Thu, 21 Nov 2013, Dmitriy Traytel wrote:

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

Both of this is related to the old question how much structural integrity 
the Goal.prove family of functions should enforce.  Historically there 
were many tools violating the basic context discipline, long before 
"localization" emerged as a slogan, so it could not be too rigid.

I had checked the situation last time in 2009, so the current cfe53047dc16 
to enforce more structure of goals was overdue.  This avoids the flexflex 
confusion of Issue2.  The hyps problem behind Issue1 is still open, 
because the Simplifier prems are not properly declared in the context, and 
thus some simprocs that use them with Goal.prove would crash.

There is always something left in the continuous localization process ...


 	Makarius