Email Gateway (Aug 22 2022 at 16:44): Email Gateway (Aug 22 2022 at 16:44):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Isabelle users,
I've noticed that the prover remote_vampire never responds when I run
sledgehammer.
In the box I can see all 5 provers (cvc4 z3 spass e remote_vampire)
but every time I run sledgehammer only the first 4 respond.
Two of my colleagues have also noticed the same.
Any ideas about why this is happening?
Many thanks,
kind regards,
Angeliki
Email Gateway (Aug 22 2022 at 16:45):From: Makarius <makarius@sketis.net>
I guess you have 4 cores -- or a nominal number of threads=4.
The latter can be changed in the Isabelle/jEdit dialog Plugins / Plugin
Options / Isabelle / General / Parallel Processing / Threads, but I
recommend to do this only for experimentation.
A different possibility is to put remote_vampire first in the list of
provers temporarily.
Another source of occasional problems is the Software-as-a-Service
nature of remote_vampire: it means that it can be sporadically
unavailable, silently change versions on the server side, or fail by
other means. (I've heard some rumors, that vampire might become a local
prover in the next Isabelle release and thus more reliable.)
Side-remark: normally Jasmin Blanchette is responsible for Sledgehammer
questions on this list, but he is probably on vacation from the Internet.
Makarius
Email Gateway (Aug 22 2022 at 16:45):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Makarius,
many thanks for your answer.
After trying out your suggestions I noticed the following:
-my threads number was set by default to threads=0. When I changed it to
5, indeed
remote_vampire "appeared" after using sledgehammer but only gave the
message:
"a prover error occurred".
The same happened in both a context where the other 4 provers gave a
proof, and a
context where the other 4 provers failed.
thanks again,
Angeliki
Email Gateway (Aug 22 2022 at 16:45):From: Makarius <makarius@sketis.net>
Here is another way to invoke just remote_vampire with more output:
lemma "[x] = [y] ⟹ x = y"
sledgehammer [prover = remote_vampire, verbose]
This gives me:
"remote_vampire": A prover error occurred:
ERROR: Line 809 Char 31 Token "~" continuing with "Y = nil_typerep) =>"
So it might be again a problem of the vampire "Software-as-a-Service".
Makarius
Email Gateway (Aug 22 2022 at 16:46):From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear Makarius,
thank you for your answer. By trying the same
i.e.
lemma "[x] = [y] ⟹ x = y"
sledgehammer [prover = remote_vampire, verbose]
I also get an error and moreover I get the following mysterious message:
"remote_vampire": A prover error occurred:
% SZS start RequiredInformation
% Congratulations - you have become a registered power user of
SystemOnTPTP, at IP address 128.232.*.
% Please consider donating to the TPTP project - see www.tptp.org for
details.
% When you donate this message will disappear.
% If you do not donate a random delay might be added to your processing
time.
% SZS end RequiredInformation
ERROR: Line 1203 Char 47 Token "~" continuing with "nil_typerep = cons_"
Angeliki
Email Gateway (Aug 22 2022 at 16:46):From: Lawrence Paulson <lp15@cam.ac.uk>
This message is standard for people who are heavy users of the remote_vampire based at the University of Miami. It is unfortunate in your case, given that Vampire has never worked for you. Unfortunately, Vampire doesn't appear to be available for downloading at this time.
Larry
Email Gateway (Aug 22 2022 at 16:46):From: Makarius <makarius@sketis.net>
Note that there are two messages: the last line looks line a genuine
error. Maybe due to a change of the remote vampire version; or maybe
that is normal: Jasmin Blanchette should be able to say when he is back
from vacation.
Makarius
Last updated: Apr 26 2024 at 20:16 UTC