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.

Cheers,

Jasmin





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