[isabelle-dev] sledgehammer

[Tobias Nipkow]

Looking at the source code, the "Bad executable" indicates that the file
could not be found by Isabelle. But since it exists and is executable,
as you have confirmed by executing it by hand, I can only guess that
$ISABELLE_HOME is not pointing to the right place - but I don't know how
to figure this out or correct it.

Tobias

Mamoun FILALI-AMINE schrieb:
> Hello (again, sorry my last message was not terminated),
> 
> 
> I use the snapshot:
> Unofficial version of Isabelle/HOL (Isabelle repository snapshot
> 94b74365ceb9 (23-Mar-2009))
> See also http://isabelle.in.tum.de/repos/isabelle/log/94b74365ceb9
> (with polyml-5.2.1)
> 
> 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)
> 
> (by the way :
> while if I execute: $ISABELLE_HOME/contrib/SystemOnTPTP/remote
> Missing problem file at /usr/local/Isabelle/contrib/SystemOnTPTP/remote
> line 70
> )
> 
> Has any one encountered these installation problems?
> 
> thanks
> 
> Mamoun
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev