On Wed, 10 Oct 2012, Peter Lammich wrote:
It's always problematic if the user cannot be sure whether his theorem
is actually proved, or the proof method is just diverging in a parallel
thread. Thus, a UI should provide very clear information to the user,
otherwise we will get "Problem" reports of the form: "Everything runs
fine in JEdit, but when building the session via command line it
computes for 10 minutes and then fails ..."
So have you tried Isabelle/jEdit in the meantime? As part of the
parallelization of terminal proofs there is much more red in the text than
before.
See also the recent "quick and dirty" thread:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2012-October/msg00003.html
This motivates again why different behaviour in different "modes" causes
confusion about what the system might be doing.
BTW, the [?] printing can be avoided by enabling quick_and_dirty mode,
what Proof General normally does.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
