Re: [isabelle] Cygwin Isabelle2014 sledgehammer libwww-perl missing
> 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