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)

notepad begin
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.