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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev