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



Am 17.07.2014 um 00:30 schrieb Lars Noschinski <noschinl at in.tum.de>:
> But I stumbled upon some interesting behaviour: Apparently, in this
> proof, sledgehammer tries to use a theorem whose proof (in another
> theory) failed. So, in the sledgehammer window, I don't see the output
> of sledgehammer, but rather the error message belonging to the failed
> "by" of said theorem.
> 
> -- Lars

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.

Fabian





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