# HG changeset patch
# User blanchet
# Date 1282215877 -7200
# Node ID a57d04dd1b256bd96dfe98c6a65538480c6aa554
# Parent  d5d7eecb953e7b90911de7aa41a1ca8282fc56d9
fix SInE's error handling + run "vampire" locally if either SPASS or E is missing

diff -r d5d7eecb953e -r a57d04dd1b25 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 19 12:04:07 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Aug 19 13:04:37 2010 +0200
@@ -261,7 +261,9 @@
 
 val remote_e = remotify_prover e "EP---"
 val remote_vampire = remotify_prover vampire "Vampire---9"
-val remote_sine_e = remote_prover "sine_e" "SInE---" [] [] 150 (* FIXME *) false
+val remote_sine_e =
+  remote_prover "sine_e" "SInE---" []
+                [(Unprovable, "says Unknown")] 150 (* FIXME *) false
 val remote_snark =
   remote_prover "snark" "SNARK---" [("refutation.", "end_refutation.")] []
                 50 (* FIXME *) false
@@ -276,7 +278,11 @@
 fun default_atps_param_value () =
   space_implode " " ([maybe_remote e] @
                      (if is_installed (snd spass) then [fst spass] else []) @
-                     [remotify_name (fst vampire), fst remote_sine_e])
+                     [if forall (is_installed o snd) [e, spass] then
+                        remotify_name (fst vampire)
+                      else
+                        maybe_remote vampire,
+                      fst remote_sine_e])
 
 val provers = [e, spass, vampire, remote_e, remote_vampire, remote_sine_e,
                remote_snark]