# Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP

On Fri, 1 Aug 2014, Jasmin Christian Blanchette wrote:


I have recently seen this behavior as well (in Isabelle2014-RC1) and can reproduce it as follows (it seems important that mashine learning is "finished"):

theory Scratch imports Main begin

lemma True sledgehammer learn_isar by (rule TrueI)

fix P
have "P"
by nothing
have "P"
(* invoke s/h here *)

inserting a textual "sledgehammer" or "sledgehammer learn_isar" command shows nothing in the output, but colors the command in red.



The attached changeset for "isabelle-release" fixes it. In short, it's naive to expect "Thm.proof_body_of" never to throw any exceptions.

There is some documentation about it in the implementation manual:

\item @{ML Thm.proof_of}~ at {text "thm"} and @{ML
Thm.proof_body_of}~ at {text "thm"} produce the proof term or proof
body (with digest of oracles and theorems) from a given theorem.
Note that this involves a full join of internal futures that fulfill
pending proof promises, and thus disrupts the natural bottom-up
construction of proofs by introducing dynamic ad-hoc dependencies.
Parallel performance may suffer by inspecting proof terms at
run-time.


This makes it clear that looking at the internal derivation of a theorem means to side-step the normal order of processing -- as a consequence you may see failures from forked branches of the parallel execution.



Makarius: Could you apply the attached changeset to "isabelle-release"?


OK, I will push this over to bitbucket soon.


Although the deeper problem remains: How to inspect parallel derivations robustly while the system is running? The Thm.get_name_hint approach is fragile anyway -- I have just been there with another guy today. Isn't that one of the hints from the Isabelle cookbook that don't quite work?


Makarius



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