[isabelle-dev] Circular reasoning via multithreading seems too easy

[Makarius]

On 05/12/16 11:00, Peter Lammich wrote:
> Poking on the problem a bit more, I realized that, in the
> Isabelle/jedit IDE, promises seem to be never checked. The following
> theory works fine in the IDE, but, fortunately, fails in build mode.
> 
> I would have expected, at least at some point, to be notified of the
> problem (mismatch of promised and proved thm) by the IDE. However, I
> can even import Scratch.thy from some other theory, without ever seeing
> any error in the IDE. 

It is part of the current concepts of the Prover IDE that there is no
"closing" of the checking process. So the above behaviour is the
expected one.

Batch mode is different: it goes through great pains and complexity to
join all forks, and consolidate the type thm vs. theory content in the
end. (The problem encountered here is probably due to a conflict of this
documented / published approach vs. the actual implementation that has
to cope with proof terms and "close_derivation" as additional aspect.)


At some point, both the PIDE model and the batch checking should
converge to just one uniform approach: thus batch mode will become
slightly less strict, but interaction much more strict. It is just the
usual balancing of possibilities in a real system.


	Makarius