# HG changeset patch
# User blanchet
# Date 1281959944 -7200
# Node ID 9043eefe8d71ec44ceda2e40573f47f664a406f9
# Parent  1e28e2e1c2fb4321a7fdfb6ad475f4b4ec9578db
detect old Vampire and give a nicer error message

diff -r 1e28e2e1c2fb -r 9043eefe8d71 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 16 09:39:05 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Aug 16 13:59:04 2010 +0200
@@ -8,9 +8,7 @@
 signature ATP_SYSTEMS =
 sig
   datatype failure =
-    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
-    OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
-    MalformedOutput | UnknownError
+    Unprovable | IncompleteUnprovable | MalformedOutput | UnknownError
 
   type prover_config =
     {exec: string * string,
@@ -39,9 +37,9 @@
 (* prover configuration *)
 
 datatype failure =
-    Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
-    OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
-    MalformedOutput | UnknownError
+  Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
+  OldSpass | OldVampire | NoPerl | NoLibwwwPerl | MalformedInput |
+  MalformedOutput | UnknownError
 
 type prover_config =
   {exec: string * string,
@@ -72,6 +70,10 @@
                (Path.variable "ISABELLE_HOME_USER" ::
                 map Path.basic ["etc", "components"])))) ^
     " on a line of its own."
+  | string_for_failure OldVampire =
+    "Isabelle requires a more recent version of Vampire. To install it, follow \
+    \the instructions from the Sledgehammer manual (\"isabelle doc\
+    \ sledgehammer\")."
   | string_for_failure NoPerl = "Perl" ^ missing_message_tail
   | string_for_failure NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail
@@ -143,6 +145,7 @@
    max_new_relevant_facts_per_iter = 60 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
+
 val e = ("e", e_config)
 
 
@@ -169,8 +172,10 @@
    max_new_relevant_facts_per_iter = 35 (* FIXME *),
    prefers_theory_relevant = true,
    explicit_forall = true}
+
 val spass = ("spass", spass_config)
 
+
 (* Vampire *)
 
 val vampire_config : prover_config =
@@ -189,12 +194,15 @@
       (IncompleteUnprovable, "CANNOT PROVE"),
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
-      (OutOfResources, "Refutation not found")],
+      (OutOfResources, "Refutation not found"),
+      (OldVampire, "input_file")],
    max_new_relevant_facts_per_iter = 50 (* FIXME *),
    prefers_theory_relevant = false,
    explicit_forall = false}
+
 val vampire = ("vampire", vampire_config)
 
+
 (* Remote prover invocation via SystemOnTPTP *)
 
 val systems = Synchronized.var "atp_systems" ([] : string list)
@@ -236,13 +244,15 @@
    explicit_forall = true}
 
 val remote_name = prefix "remote_"
-
 fun remote_prover (name, config) atp_prefix =
   (remote_name name, remote_config atp_prefix config)
 
 val remote_e = remote_prover e "EP---"
 val remote_vampire = remote_prover vampire "Vampire---9"
 
+
+(* Setup *)
+
 fun is_installed ({exec, required_execs, ...} : prover_config) =
   forall (curry (op <>) "" o getenv o fst) (exec :: required_execs)
 fun maybe_remote (name, config) =