[isabelle-dev] "ISABELLE_ATP" is not set

[Makarius]

On Thu, 6 Jan 2011, Sascha Boehme wrote:

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

You probably mean "some arbitrary repository version" of Isabelle.  We are 
not using svn, but Mercurial; there are more than 40000 known versions so 
far, so "the" version is not defined.

A quick grep over version Isabelle/1b31460c2e3a (from today) reveals that 
ISABELLE_ATP is set via the component src/HOL/Tools/ATP, which happens to 
be one of those that are part of the main repository.  This means the lack 
of ISABELLE_ATP indicates that there is something more fundamentally 
wrong, maybe in the way you have started up the Isabelle process.

You can also check settings manually like this:

   $ isabelle getenv ISABELLE_ATP
   ISABELLE_ATP=/Users/makarius/isabelle/repos/src/HOL/Tools/ATP


Anyway, it is slightly easier to experiment with some arbitrary snapshot 
from http://isabelle.in.tum.de/devel/


 	Makarius