[isabelle-dev] superfluous [?]

[Peter Lammich]

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