--- a/doc-src/Sledgehammer/sledgehammer.tex Thu Jul 29 09:57:10 2010 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Jul 29 12:07:09 2010 +0200
@@ -147,7 +147,12 @@
Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
\texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
-\texttt{SPASS}, or \texttt{vampire} executable.
+\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
+with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0%
+\footnote{Following the rewrite of Vampire, the counter for version numbers was
+reset to 0; hence the new Vampire 1.0 is more recent than Vampire 11.5.}%
+. Since the ATPs' output formats are neither documented nor stable, other
+versions of the ATPs might or might not work well with Sledgehammer.
\end{enum}
To check whether E and SPASS are installed, follow the example in
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jul 29 09:57:10 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Jul 29 12:07:09 2010 +0200
@@ -9,7 +9,8 @@
sig
datatype failure =
Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
- OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
+ OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
+ MalformedOutput | UnknownError
type prover_config =
{executable: string * string,
@@ -21,6 +22,9 @@
prefers_theory_relevant: bool,
explicit_forall: bool}
+ val string_for_failure : failure -> string
+ val known_failure_in_output :
+ string -> (failure * string) list -> failure option
val add_prover: string * prover_config -> theory -> theory
val get_prover: theory -> string -> prover_config
val available_atps: theory -> unit
@@ -35,8 +39,9 @@
(* prover configuration *)
datatype failure =
- Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
- OldSpass | MalformedInput | MalformedOutput | UnknownError
+ Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
+ OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
+ MalformedOutput | UnknownError
type prover_config =
{executable: string * string,
@@ -48,6 +53,41 @@
prefers_theory_relevant: bool,
explicit_forall: bool}
+val missing_message_tail =
+ " appears to be missing. You will need to install it if you want to run \
+ \ATPs remotely."
+
+fun string_for_failure Unprovable = "The ATP problem is unprovable."
+ | string_for_failure IncompleteUnprovable =
+ "The ATP cannot prove the problem."
+ | string_for_failure CantConnect = "Can't connect to remote ATP."
+ | string_for_failure TimedOut = "Timed out."
+ | string_for_failure OutOfResources = "The ATP ran out of resources."
+ | string_for_failure OldSpass =
+ "Warning: Isabelle requires a more recent version of SPASS with \
+ \support for the TPTP syntax. To install it, download and extract the \
+ \package \"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and \
+ \add the \"spass-3.7\" 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
+ | string_for_failure MalformedInput =
+ "Internal Isabelle error: The ATP problem is malformed. Please report \
+ \this to the Isabelle developers."
+ | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
+ | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
+
+fun known_failure_in_output output =
+ find_first (fn (_, pattern) => String.isSubstring pattern output)
+ #> Option.map fst
+
+val known_perl_failures =
+ [(NoPerl, "env: perl"),
+ (NoLibwwwPerl, "Can't locate HTTP")]
(* named provers *)
@@ -118,6 +158,7 @@
|> not complete ? prefix "-SOS=1 ",
proof_delims = [("Here is a proof", "Formulae used in the proof")],
known_failures =
+ known_perl_failures @
[(IncompleteUnprovable, "SPASS beiseite: Completion found"),
(TimedOut, "SPASS beiseite: Ran out of time"),
(OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
@@ -154,14 +195,15 @@
(* Remote prover invocation via SystemOnTPTP *)
-val systems = Synchronized.var "atp_systems" ([]: string list)
+val systems = Synchronized.var "atp_systems" ([] : string list)
fun get_systems () =
- case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w" of
+ case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
(answer, 0) => split_lines answer
| (answer, _) =>
- error ("Failed to get available systems at SystemOnTPTP:\n" ^
- perhaps (try (unsuffix "\n")) answer)
+ error (case known_failure_in_output answer known_perl_failures of
+ SOME failure => string_for_failure failure
+ | NONE => perhaps (try (unsuffix "\n")) answer ^ ".")
fun refresh_systems_on_tptp () =
Synchronized.change systems (fn _ => get_systems ())
@@ -175,11 +217,6 @@
NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
| SOME sys => sys);
-val remote_known_failures =
- [(CantConnect, "HTTP-Error"),
- (TimedOut, "says Timeout"),
- (MalformedOutput, "Remote script could not extract proof")]
-
fun remote_config atp_prefix
({proof_delims, known_failures, max_new_relevant_facts_per_iter,
prefers_theory_relevant, explicit_forall, ...} : prover_config)
@@ -190,7 +227,10 @@
" -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
the_system atp_prefix,
proof_delims = insert (op =) tstp_proof_delims proof_delims,
- known_failures = remote_known_failures @ known_failures,
+ known_failures =
+ known_failures @ known_perl_failures @
+ [(CantConnect, "HTTP-Error"),
+ (TimedOut, "says Timeout")],
max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
prefers_theory_relevant = prefers_theory_relevant,
explicit_forall = explicit_forall}
--- a/src/HOL/Tools/ATP/scripts/remote_atp Thu Jul 29 09:57:10 2010 +0200
+++ b/src/HOL/Tools/ATP/scripts/remote_atp Thu Jul 29 12:07:09 2010 +0200
@@ -2,6 +2,7 @@
#
# Wrapper for custom remote provers on SystemOnTPTP
# Author: Fabian Immler, TU Muenchen
+# Author: Jasmin Blanchette, TU Muenchen
#
use warnings;
@@ -28,14 +29,14 @@
#----Usage
sub usage() {
- print("Usage: remote_atp [<options>] <File name>\n");
- print(" <options> are ...\n");
- print(" -h - print this help\n");
- print(" -w - list available ATP systems\n");
- print(" -s<system> - specified system to use\n");
- print(" -t<timelimit> - CPU time limit for system\n");
- print(" -c<command> - custom command for system\n");
- print(" <File name> - TPTP problem file\n");
+ print("Usage: remote_atp [<options>] <file_name>\n");
+ print("Options:\n");
+ print(" -h print this help\n");
+ print(" -w list available ATPs\n");
+ print(" -s<system> ATP to use\n");
+ print(" -t<time_limit> CPU time limit for ATP\n");
+ print(" -c<command> custom ATP invocation command\n");
+ print(" <file_name> TPTP problem file\n");
exit(0);
}
if (exists($Options{'h'})) {
@@ -95,13 +96,15 @@
#catch errors / failure
if(!$Response->is_success) {
- print "HTTP-Error: " . $Response->message . "\n";
+ my $message = $Response->message;
+ $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
+ print $message . "\n";
exit(-1);
} elsif (exists($Options{'w'})) {
print $Response->content;
exit (0);
} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
- print "Specified System $1 does not exist\n";
+ print "The ATP \"$1\" is not available at SystemOnTPTP\n";
exit(-1);
} else {
print $Response->content;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 09:57:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 12:07:09 2010 +0200
@@ -148,42 +148,17 @@
fun extract_proof_and_outcome complete res_code proof_delims known_failures
output =
- case map_filter (fn (failure, pattern) =>
- if String.isSubstring pattern output then SOME failure
- else NONE) known_failures of
- [] => (case extract_proof proof_delims output of
- "" => ("", SOME UnknownError)
+ case known_failure_in_output output known_failures of
+ NONE => (case extract_proof proof_delims output of
+ "" => ("", SOME MalformedOutput)
| proof => if res_code = 0 then (proof, NONE)
else ("", SOME UnknownError))
- | (failure :: _) =>
+ | SOME failure =>
("", SOME (if failure = IncompleteUnprovable andalso complete then
Unprovable
else
failure))
-fun string_for_failure Unprovable = "The ATP problem is unprovable."
- | string_for_failure IncompleteUnprovable =
- "The ATP cannot prove the problem."
- | string_for_failure CantConnect = "Can't connect to remote ATP."
- | string_for_failure TimedOut = "Timed out."
- | string_for_failure OutOfResources = "The ATP ran out of resources."
- | string_for_failure OldSpass =
- (* FIXME: Change the error message below to point to the Isabelle download
- page once the package is there. *)
- "Warning: Sledgehammer requires a more recent version of SPASS with \
- \support for the TPTP syntax. To install it, download and untar the \
- \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
- \\"spass-3.7\" directory's full path to \"" ^
- 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 MalformedInput =
- "Internal Sledgehammer error: The ATP problem is malformed. Please report \
- \this to the Isabelle developers."
- | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
- | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
-
(* Clause preparation *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 09:57:10 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 12:07:09 2010 +0200
@@ -66,8 +66,7 @@
| mk_anot phi = AConn (ANot, [phi])
fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
-val index_in_shape : int -> int list list -> int =
- find_index o exists o curry (op =)
+fun index_in_shape x = find_index (exists (curry (op =) x))
fun is_axiom_clause_number thm_names num =
num > 0 andalso num <= Vector.length thm_names andalso
Vector.sub (thm_names, num - 1) <> ""
@@ -133,7 +132,8 @@
which can be hard to disambiguate from function application in an LL(1)
parser. As a workaround, we extend the TPTP term syntax with such detritus
and ignore it. *)
-val parse_vampire_detritus = scan_integer |-- $$ ":" --| scan_integer >> K []
+fun parse_vampire_detritus x =
+ (scan_integer |-- $$ ":" --| scan_integer >> K []) x
fun parse_term pool x =
((scan_dollar_name >> repair_name pool)