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.
Cheers,
Sascha
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
