Hi
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 ...
Peter
On Mi, 2012-10-10 at 17:52 +0200, Makarius wrote:
On Wed, 10 Oct 2012, Ondřej Kunčar wrote:
This problem refers to 3fc6b3289c31.
If I type in this simple formalization
lemma c: x = x
by metis
thm c
the following theorem is printed ?x = ?x [?]. What is that suspicious
question mark? It seems to be produced by any metis call. And it is
reproducible almost always.
This is the normal result of printing Thm.status_of in the traditional
way. It is now getting in the way, because terminal proofs ('by') are
always parallel in Isabelle/jEdit.
I am about to rework this critical kernal status information, but it
requires some more thinking. Last time I changed something there, it was
immediately reported as problem that fewer [!] were printed as before.
Makarius
___ isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
