Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Perl Module Missing (Isabelle-RC3 on Linux)


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC