[isabelle-dev] sledgehammer / yices
boehmes at in.tum.de
Thu Jul 19 12:49:22 CEST 2012
>> I am sure this is already in the pipeline. It seems that the
>> variable YICES_INSTALLED (and the analogue for other solvers)
>> should be mentioned in the documentation of sledgehammer (since
>> what is currently given as installation instructions in `isabelle
>> doc sledgehammer` of changeset 3060e6343953 does not work without
>> setting YICES_INSTALLED="yes").
> Thanks for the report. I wasn't aware of this variable -- it seems
> like this was introduced in January 2011, after I wrote the
> documentation in Sledgehammer.
> The variable seems superfluous to me. It should be sufficient to
> check whether "YICES_SOLVER" is set. Sascha, any thoughts?
I don't know for sure. It might be that YICES_INSTALLED and friends
were added as a sanity check to avoid errors when invoking the solver
locally and it doesn't exist. If that's the case, it's probably better
to remove YICES_INSTALLED and just test if the file pointed to by
YICES_SOLVER does exist.
More information about the isabelle-dev