# HG changeset patch
# User wenzelm
# Date 1631714524 -7200
# Node ID 19022ea3f8cc587c138ebbbd0a63f7eba08e40a8
# Parent  d7a62db70a0780db1b075d517789a92502c6856e
clarified name and options for old vampire-4.2.2;

diff -r d7a62db70a07 -r 19022ea3f8cc Admin/components/components.sha1
--- 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
diff -r d7a62db70a07 -r 19022ea3f8cc Admin/components/main
--- 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
diff -r d7a62db70a07 -r 19022ea3f8cc src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- 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 "") ^