Email Gateway (Aug 18 2022 at 18:31): Email Gateway (Aug 18 2022 at 18:31):From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Hi all,
This is a warning to users of Isabelle2009{,-1,-2} who also rely on Sledgehammer and remote Vampire. These versions of Isabelle had the version number of Vampire hardcoded to 9.0, which is really ancient. Geoff Sutcliffe would like to take 9.0 down from his server but he still sees calls to it. What this means is that for you remote Vampire will stop working.
There are several workarounds for this, such as convincing Geoff to keep 9.0 up longer, or upgrading to a more recent Isabelle, or trying to replace the string "Vampire---9" in "atp_wrapper.ML" or "atp_systems.ML" with ""Vampire---" and hope that things work, or installing the Vampire 9.0 binary locally, or using another prover.
(Newer versions of Sledgehammer gracefully fall back on whatever version of the ATP is available if the "favorite" version is not available, so that this doesn't happen again.)
Jasmin
Last updated: Apr 27 2024 at 01:05 UTC