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



On Wed, 11 Jun 2014, Gottfried Barrow wrote:

I'm using the pre-RC Isabelle2014 from here:

http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg05386.html

(This official isabelle-dev archive has stopped working for me:
  https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev)

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.

Thanks for testing that unofficial integration-test snapshot. It shows that there was something wrong with the integration, namely the cygwin component.

This thread should have remained on isabelle-dev, though, where the development process happens, and everything is constantly moving -- hopefully forwards and usually quite fast. See also this change from 3 weeks ago:

changeset:   57132:f6fead547e9b
user:        wenzelm
date:        Fri May 30 15:34:14 2014 +0200
files: Admin/components/bundled-windows Admin/components/components.sha1 Admin/lib/Tools/makedist_cygwin
description:
updated cygwin -- include perl_vendor for libwww-perl;


Public testing of isabelle-users of Isabelle2014-RC0 should start at the end of next week. Until then the continued development happens at isabelle-dev.


	Makarius




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