[isabelle-dev] sledgehammer / yices

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Thu Jul 19 10:08:58 CEST 2012

Hi Christian,

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



More information about the isabelle-dev mailing list