Re: [isabelle] prover remote_vampire not responding

On 12/02/18 15:45, Dr A. Koutsoukou-Argyraki wrote:
> 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?

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.


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