Re: [isabelle] exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop



Dear Makarius,

thanks for your reply.

Am Dienstag, den 24.02.2015, 15:50 +0100 schrieb Makarius:
> > what is usually the cause for the error message
> >
> >        *** exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop
> >
> > To reproduce with Isabelle-2014, run
> > $ git clone https://github.com/gattschardo/open-inductive
> > $ cd open-inductive
> > add "Open_Arith_Eval" to "theories" in ROOT
> > $ isabelle build -D .
> >
> >
> > It does not (seem to) occur in Isabelle/jEdit.
> 
> The parallelism is less aggressive in interactive PIDE document processing 
> than in batch build.  This might be a reason for the breakdown of the 
> forked proof, see als src/Pure/thm.ML function future_result.
> 
> Since I can't reproduce the problem,

do you meant the problem does not occur for you, or that you were unable
to attempt to reproduce it?

> I recommend to insert a different 
> exception there, e.g. TERM with the relevant arguments for more 
> information.

Thanks, weâll try that.

> Skimming over the sources of open_inductive.ML, there are various points 
> that look a bit suspicious concerning hyps and context, which might be a 
> source of such problems.  Occasionally it looks like the abstract notion 
> of goal state -- which happens to be represented as concrete thm, but with 
> certain implicit policies -- is not properly observed.
> 
> I have more to say about the sources, but that has to wait.

A review of that code would be highly appreciated â you can probably
tell that it was not written with a great lot of experience with and
comprehensive knowledge of the Isabelle internals.

Greetings,
Joachim

-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.