[isabelle-dev] sledgehammer

[Makarius]

On Sat, 28 Mar 2009, Mamoun FILALI-AMINE wrote:

> I use the snapshot:
> Unofficial version of Isabelle/HOL (Isabelle repository snapshot 94b74365ceb9 
> (23-Mar-2009))
>
> I have the following problem with the isabelle command sledgehammer:
> Sledgehammer: external prover "remote_vampire" for subgoal 1:
> finite {t?nat. t < (t'?nat) ? t mod b_period (b?'buffer) = deadline (owner b) 
> mod b_period b}
> Error: Bad executable: $ISABELLE_HOME/contrib/SystemOnTPTP/remote (I have an 
> intel mac)

Very strange.  Please try this within the same Isabelle / Proof General 
session:

   ML {* getenv "ISABELLE_HOME" *}

This should point to your Isabelle snapshot, and the 
contrib/SystemOnTPTP/remote should be in there, unless it got lost 
somehow.


 	Makarius