[isabelle-dev] [isabelle] "ISABELLE_ATP" is not set

s.wong.731 at gmail.com s.wong.731 at gmail.com
Fri Jan 7 20:18:25 CET 2011


Hi Sascha,

Mercurial doesn't work for me, possibly because I downloaded the gzip on 22  
Dec.

Basically, I get a problem even when I do:

lemma "P"
sledgehammer

Thanks
Steve

On Jan 6, 2011 3:03pm, Sascha Boehme <boehmes at in.tum.de> wrote:
> Hi Steve,



> An arbitrary development snapshot of Isabelle is not required to run

> as expected, but many snapshots do. Since your question is related to

> such an arbitray version of Isabelle, I took the freedom to move your

> question to the developer list.



> To solve your issue, could you please specify which precise instance

> of Isabelle you have, eg, by issuing the command "hg id" at your

> console? Furthermore, how did the error manifest itself, ie, under

> what conditions do you see the error? Do you maybe have a small

> example theory?



> Sascha



> s.wong.731 at gmail.com wrote:

> > Hi all,

> >

> > I'm using the svn version of Isabelle and when I try to run

> > sledgehammer, I get an error complaining that the environment

> > variable "ISABELLE_ATP" is not set. How do I set it? I can't seem to

> > find it in the etc/settings file.

> >

> > Thanks for the help.

> >

> > Steve


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110107/a575f5fc/attachment-0002.html>


More information about the isabelle-dev mailing list