--- a/Admin/components/components.sha1 Mon Sep 13 17:06:44 2021 +0200
+++ b/Admin/components/components.sha1 Wed Sep 15 16:02:04 2021 +0200
@@ -262,6 +262,7 @@
e1b34e8f54e7e5844873612635444fed434718a1 naproche-7d0947a91dd5.tar.gz
26df569cee9c2fd91b9ac06714afd43f3b37a1dd nunchaku-0.3.tar.gz
e573f2cbb57eb7b813ed5908753cfe2cb41033ca nunchaku-0.5.tar.gz
+3d7b7690dfd09e25ad56e64b519f61f06e3ab706 old_vampire-4.2.2.tar.gz
fe57793aca175336deea4f5e9c0d949a197850ac opam-1.2.2.tar.gz
eb499a18e7040ca0fe1ca824c9dcb2087c47c9ba opam-2.0.3-1.tar.gz
002f74c9e65e650de2638bf54d7b012b8de76c28 opam-2.0.3.tar.gz
--- a/Admin/components/main Mon Sep 13 17:06:44 2021 +0200
+++ b/Admin/components/main Wed Sep 15 16:02:04 2021 +0200
@@ -15,6 +15,7 @@
jortho-1.0-2
kodkodi-1.5.6-1
nunchaku-0.5
+old_vampire-4.2.2
opam-2.0.7
polyml-5.8.2
postgresql-42.2.18
@@ -24,7 +25,6 @@
sqlite-jdbc-3.34.0
ssh-java-20190323
stack-2.7.3
-vampire-4.2.2
verit-2020.10-rmx-1
xz-java-1.8
z3-4.4.0pre-3
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Sep 13 17:06:44 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Sep 15 16:02:04 2021 +0200
@@ -319,7 +319,7 @@
val iprover_config : atp_config =
{exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
- ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^
+ ["--clausifier \"$OLD_VAMPIRE_HOME\"/vampire " ^
"--clausifier_options \"--mode clausify\" " ^
"--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
proof_delims = tstp_proof_delims,
@@ -477,7 +477,11 @@
\\"vampire_noncommercial\" to \"yes\" (e.g. via the Isabelle/jEdit menu Plugin Options \
\/ Isabelle / General)")))
-val vampire_basic_options = "--proof tptp --output_axiom_names on $VAMPIRE_EXTRA_OPTIONS"
+val vampire_basic_options =
+ "--proof tptp --output_axiom_names on" ^
+ (if ML_System.platform_is_windows
+ then "" (*time slicing is not support in the Windows version of Vampire*)
+ else " --mode casc")
val vampire_full_proof_options =
" --proof_extra free --forced_options avatar=off:equality_proxy=off:general_splitting=off:inequality_splitting=0:naming=0"
@@ -486,7 +490,7 @@
let
val format = TFF (Without_FOOL, Monomorphic)
in
- {exec = (["VAMPIRE_HOME"], ["vampire"]),
+ {exec = (["OLD_VAMPIRE_HOME"], ["vampire"]),
arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
(check_vampire_noncommercial ();
[vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^