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



On Mon, 23 Feb 2015, Joachim Breitner wrote:

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, I recommend to insert a different exception there, e.g. TERM with the relevant arguments for more information.


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.


	Makarius





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