Email Gateway (Aug 19 2022 at 14:38): Email Gateway (Aug 19 2022 at 14:38):From: Makarius <makarius@sketis.net>
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
Email Gateway (Aug 19 2022 at 14:39):From: Gottfried Barrow <igbi@gmx.com>
On 14-06-26 07:31, Makarius wrote:
Thanks for testing that unofficial integration-test snapshot. It
shows that there was something wrong with the integration, namely the
cygwin component.
As it turns out, I'm not really testing it, I'm using it.
Everything seems to work good. When my CPU meter is at 100% for too
long, when it doesn't seem it should be, my first tendency was, and can
be, to think that it's gone into a bad, deep loop, and that something's
wrong.
I now try remember to first ask, "Is one of the auto tools that I have
enabled causing this?" I think that when I have incomplete, error
causing syntax, that auto Nitpick will go into heavy usage for a longer
than normal time, but I'm not sure.
I don't use "Auto Sledgehammer", and I see that "Auto Time Limit" is
only 2 seconds, but when I'm getting that long CPU heavy, when I don't
think I should be, when I disable all the auto tools, that seems to
eliminate the heavy CPU usage.
I mention this because a person, me and probably others too, can think
there's a problem when some features just need to be disabled. I have a
keyboard shortcut to quickly enable and disable continuous proving, but
I don't think I can assign keyboard shortcuts to options in "Plugin
Options/ Isabelle / General / Automatically tried tools".
Part of the heavy usage can sometimes come from my using split screens,
so sometimes I need to change what file is being displayed in an edit
buffer I'm not working in.
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:
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.
There's not really a problem here, other than my problem, and my
problems aren't necessarily other people's problems.
Because of search engines, I compartmentalize on the Web, and I don't
want a profile on isabelle-dev. Unfortunately, I've created a small one
there, even though it was my intention for that not to happen.
My pointing out the failure of Sledgehammer shows the value of watching
that list and saying things, and I foresee a reason, maybe once a year,
to say something similar. The only solution is to send in an email under
a different handle, so if someone who appears to be me does that, it
could be me, it could be someone else, or it could be someone who can
neither confirm nor deny that it's me. I partly say this to show that
I'm willing to create another email account to abide by the list
etiquette that you want. A better solution could be just to live with
problems, for however long they exist.
Contrary to any possible appearance, I haven't been involved in any of
the development process, though it may be that I extend Isabelle in ways
that nobody else is extending it, which could be perceived as
development. I'm an independent operator, and it's too easy to get a
higher profile than I warrant due to light traffic on isabelle-dev.
That's where professionals with connections to big name institutions
operate.
Regards,
GB
Email Gateway (Aug 19 2022 at 14:39):From: Makarius <makarius@sketis.net>
On Fri, 27 Jun 2014, Gottfried Barrow wrote:
As it turns out, I'm not really testing it, I'm using it.
By definition, when your are "using" an arbitrary repository snapshot, you
are "testing" it. It can change rather quickly, as you have seen, and not
always to the better. Serious work requires serious stable software
releases.
We have this global trend, that many projects give up the principle of
proper stable releases, and everyone is hooked on a repository for "latest
and greatest snapshots". Isabelle is still in the furtunate situation of
not following that.
I haven't been involved in any of the development process, though it may
be that I extend Isabelle in ways that nobody else is extending it,
which could be perceived as development. I'm an independent operator,
and it's too easy to get a higher profile than I warrant due to light
traffic on isabelle-dev.
Systems extensions are perfectly normal for users, on normal stable
releases. In some sense, all of Isabelle/HOL is just a user-space
library, although a very big and complex one.
What makes you part of the development process is the "use" (i.e.
"testing") of an arbtrary snapshot of the present state of the
development.
Makarius
Email Gateway (Aug 19 2022 at 14:43):From: Gottfried Barrow <igbi@gmx.com>
Hi,
I'm using the pre-RC Isabelle2014 from here:
http://www.mail-archive.com/isabelle-dev@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.
Regards,
GB
Email Gateway (Aug 19 2022 at 14:43):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Gottfried,
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
Email Gateway (Aug 19 2022 at 14:44):From: Gottfried Barrow <igbi@gmx.com>
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@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
Email Gateway (Aug 19 2022 at 14:45):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Gottfried,
Indeed, this is probably the issue. Makarius is currently on vacation, but he would probably be the best person to help you there.
You could also try running the script "src/HOL/Tools/ATP/scripts/remote_atp" directly and see if/why it fails more directly than through Isabelle.
Cheers,
Jasmin
Last updated: Apr 24 2024 at 20:16 UTC