Email Gateway (Aug 22 2022 at 09:45): Email Gateway (Aug 22 2022 at 09:45):From: Alfio Martini <alfio.martini@acm.org>
Dear Users,
When using sledgehammer with Isabelle-RC3 on Linux (Mint) I get
the warning message
"The Perl module "libwww-perl" appears to be missing. You will need to
install it if you want to invoke remote provers".
After installing the library the message disappears and most importantly,
I no longer get the s/h message "remote_vampire": Error: SystemOnTPTP is
not available". I wonder if something
in this direction needs or could be done for the Windows installation.
Best!
Email Gateway (Aug 22 2022 at 09:46):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Alfio,
Our installation page lists “libwww” as a dependency on Linux:
http://isabelle.in.tum.de/website-Isabelle2015-RC4/installation.html
For some reason, it’s not part of the list on Windows and Mac. Makarius, perhaps this should be changed? I think even on the Mac, it’s optimistic to expect it to be available, or has this changed now?
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 09:46):From: Alfio Martini <alfio.martini@acm.org>
Hi Jasmin,
Thank you for this feedback.
Best!
Alfio Martini
Associate Professor
Faculdade de Informática - PUCRS
www.inf.pucrs.br/alfio
Email Gateway (Aug 22 2022 at 09:47):From: Makarius <makarius@sketis.net>
On Windows we have a bundled Cygwin that contains excactly what is
required by default. The details are determined here:
http://isabelle.in.tum.de/repos/isabelle/file/e1d8c5099bef/Admin/lib/Tools/makedist_cygwin#l58
For Isabelle2015 the dependencies actually shrunk a bit: Python is no
longer needed. Since JDK only includes the JRE now, the overall bundle
has become quite slim.
On Mac OS X the assumption is that the user has a normal Mac OS X
installation from Apple, without any special tricks. The /usr/bin/perl
used there already includes the usual add-on libraries, to the best of my
knowledge and explicit testing on various machines. Expert users can
pretend to have a more crude Unixish platform via MacPorts or Homebrew:
the additional problems introduced by that can be resolved by looking at
the explanations for Isabelle on Linux.
Makarius
Email Gateway (Aug 22 2022 at 09:47):From: Alfio Martini <alfio.martini@acm.org>
Hi Makarius,
On Windows we have a bundled Cygwin that contains excactly what is required
Email Gateway (Aug 22 2022 at 09:47):From: Makarius <makarius@sketis.net>
I got used to see that occasionally, ever since the TPTP support was
introduced several years ago -- it can happen on all platforms. Jasmin is
the expert on that aspect, maybe he can explain more side-conditions.
I don't think that any perl modules are missing on Windows. I managed to
run sledgehammer with remote_vampire sucessfully with various examples
examples.
The above URL actually points to this line:
--packages perl,perl-libwww-perl,rlwrap,unzip,vim
Makarius
Email Gateway (Aug 22 2022 at 09:47):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Alfio,
Is it “quite common” or “happening every single time”? I see this message quite often myself, e.g. when I do proving without an Internet connection. A missing library such as libwww would make this fail every single time.
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 09:48):From: Alfio Martini <alfio.martini@acm.org>
Hi Jasmin,
Is it “quite common” or “happening every single time”? I see this message
quite often myself e.g. when I do proving without an >Internet connection.
Of course that I am assuming in my remark the existence of an Internet
connection.
Best!
Last updated: Nov 21 2024 at 12:39 UTC