Re: [isabelle] Cygwin Isabelle2014 sledgehammer libwww-perl missing

Hi Gottfried,

> I get this message when running Sledgehammer:
> The Perl module "libwww-perl" appears to be missing. You will need to install it if you want to invoke remote provers.
> "remote_vampire": Error: SystemOnTPTP is not available.
> I tried to add libwww-perl through the Cygwin setup, but it didn't show up in the setup.

Does "remote_vampire" normally work with official releases for you (e.g. Isabelle2013-2)?

It might be that the error message is confusing. Sledgehammer tries to guess what goes wrong. It could help to pass "debug" and "overlord" to Sledgehammer, e.g.,

    sledgehammer [prover = remote_vampire, debug, overlord]

and look at the generated files in $ISABELLE_HOME_USER (typically the ".isabelle" subdirectory of your home directory), which contain the problem files and the raw prover output, including any more specific errors.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.