[isabelle-dev] superfluous [?]
Makarius
makarius at sketis.net
Wed Oct 10 19:41:03 CEST 2012
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
More information about the isabelle-dev
mailing list