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



On 14-06-11 02:09, Jasmin Christian Blanchette wrote:
Does "remote_vampire" normally work with official releases for you (e.g. Isabelle2013-2)?

Yes, all the remote provers work with Isabelle2013-2.

I'm assuming it's related to this comment by Makarius, that a new Cygwin is being used:

http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg05386.html:
The following Isabelle snapshot http://www4.in.tum.de/~wenzelm/unofficial/UITP2014 may be used for testing -- it happens to include many other updates of contributing components, including
a fresh Cygwin snapshot from some weeks ago.

(1) I do the following, and it works and generates the overlord problem files in .isabelle\Isabelle_28-May-2014

theorem "True"
  sledgehammer [provers = "z3", debug, overlord]
by(simp)

(2) With any remote prover, the "debug" causes a red error message, and the overlord problem files aren't generated, such as with this:

theorem "True"
  sledgehammer [provers = "remote_satallax", debug, overlord]
OUTPUT:
Sledgehammering...
Found no relevant facts.
"remote_satallax" slice #1 with 0 facts for 30.0 s...
The Perl module "libwww-perl" appears to be missing. You will need to install it if you want to invoke remote provers.
SystemOnTPTP is not available.

(3) I eliminate "debug" and it goes from an error to a warning message, but it still doesn't generate the overlord problem files:

theorem "True"
  sledgehammer [provers = "remote_satallax", overlord]
OUTPUT:
Sledgehammering...
The Perl module "libwww-perl" appears to be missing. You will need to install it if you want to invoke remote provers.
"remote_satallax": Error: SystemOnTPTP is not available.

Thanks,
GB






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