# HG changeset patch
# User blanchet
# Date 1337592712 -7200
# Node ID 9cb132898ac84a4646ad0e317710fe38c0cba80b
# Parent  fafbb2607366fb98c60b57182747e6dfbb73d78d
invite users to upgrade their SPASS (so we can get rid of old code)

diff -r fafbb2607366 -r 9cb132898ac8 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 21 11:31:52 2012 +0200
@@ -24,6 +24,7 @@
     TimedOut |
     Inappropriate |
     OutOfResources |
+    OldSPASS |
     NoPerl |
     NoLibwwwPerl |
     MalformedInput |
@@ -80,6 +81,7 @@
   TimedOut |
   Inappropriate |
   OutOfResources |
+  OldSPASS |
   NoPerl |
   NoLibwwwPerl |
   MalformedInput |
@@ -131,6 +133,15 @@
   | string_for_failure Inappropriate =
     "The generated problem lies outside the prover's scope."
   | string_for_failure OutOfResources = "The prover ran out of resources."
+  | string_for_failure OldSPASS =
+    "The version of SPASS you are using is obsolete. Please upgrade to \
+    \SPASS 3.8ds. To install it, download and extract the package \
+    \\"http://www21.in.tum.de/~blanchet/spass-3.8ds.tar.gz\" and add the \
+    \\"spass-3.8ds\" directory's absolute path to " ^
+    quote (Path.implode (Path.expand (Path.appends
+               (Path.variable "ISABELLE_HOME_USER" ::
+                map Path.basic ["etc", "components"])))) ^
+    " on a line of its own."
   | string_for_failure NoPerl = "Perl" ^ missing_message_tail
   | string_for_failure NoLibwwwPerl =
     "The Perl module \"libwww-perl\"" ^ missing_message_tail
diff -r fafbb2607366 -r 9cb132898ac8 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon May 21 11:31:52 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon May 21 11:31:52 2012 +0200
@@ -374,7 +374,9 @@
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      known_perl_failures @
-     [(GaveUp, "SPASS beiseite: Completion found"),
+     [(OldSPASS, "SPASS V 3.5"),
+      (OldSPASS, "SPASS V 3.7"),
+      (GaveUp, "SPASS beiseite: Completion found"),
       (TimedOut, "SPASS beiseite: Ran out of time"),
       (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
       (MalformedInput, "Undefined symbol"),