1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex Thu Jul 29 09:57:10 2010 +0200
1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex Thu Jul 29 12:07:09 2010 +0200
1.3 @@ -147,7 +147,12 @@
1.4 Vampire executable from somewhere (e.g., \url{http://www.vprover.org/}),
1.5 set the environment variable \texttt{E\_HOME}, \texttt{SPASS\_HOME}, or
1.6 \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{eproof},
1.7 -\texttt{SPASS}, or \texttt{vampire} executable.
1.8 +\texttt{SPASS}, or \texttt{vampire} executable. Sledgehammer has been tested
1.9 +with E 1.0 and 1.2, SPASS 3.5 and 3.7, and Vampire 1.0%
1.10 +\footnote{Following the rewrite of Vampire, the counter for version numbers was
1.11 +reset to 0; hence the new Vampire 1.0 is more recent than Vampire 11.5.}%
1.12 +. Since the ATPs' output formats are neither documented nor stable, other
1.13 +versions of the ATPs might or might not work well with Sledgehammer.
1.14 \end{enum}
1.15
1.16 To check whether E and SPASS are installed, follow the example in
2.1 --- a/src/HOL/Tools/ATP/atp_systems.ML Thu Jul 29 09:57:10 2010 +0200
2.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML Thu Jul 29 12:07:09 2010 +0200
2.3 @@ -9,7 +9,8 @@
2.4 sig
2.5 datatype failure =
2.6 Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
2.7 - OutOfResources | OldSpass | MalformedInput | MalformedOutput | UnknownError
2.8 + OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
2.9 + MalformedOutput | UnknownError
2.10
2.11 type prover_config =
2.12 {executable: string * string,
2.13 @@ -21,6 +22,9 @@
2.14 prefers_theory_relevant: bool,
2.15 explicit_forall: bool}
2.16
2.17 + val string_for_failure : failure -> string
2.18 + val known_failure_in_output :
2.19 + string -> (failure * string) list -> failure option
2.20 val add_prover: string * prover_config -> theory -> theory
2.21 val get_prover: theory -> string -> prover_config
2.22 val available_atps: theory -> unit
2.23 @@ -35,8 +39,9 @@
2.24 (* prover configuration *)
2.25
2.26 datatype failure =
2.27 - Unprovable | IncompleteUnprovable | CantConnect | TimedOut | OutOfResources |
2.28 - OldSpass | MalformedInput | MalformedOutput | UnknownError
2.29 + Unprovable | IncompleteUnprovable | CantConnect | TimedOut |
2.30 + OutOfResources | OldSpass | NoPerl | NoLibwwwPerl | MalformedInput |
2.31 + MalformedOutput | UnknownError
2.32
2.33 type prover_config =
2.34 {executable: string * string,
2.35 @@ -48,6 +53,41 @@
2.36 prefers_theory_relevant: bool,
2.37 explicit_forall: bool}
2.38
2.39 +val missing_message_tail =
2.40 + " appears to be missing. You will need to install it if you want to run \
2.41 + \ATPs remotely."
2.42 +
2.43 +fun string_for_failure Unprovable = "The ATP problem is unprovable."
2.44 + | string_for_failure IncompleteUnprovable =
2.45 + "The ATP cannot prove the problem."
2.46 + | string_for_failure CantConnect = "Can't connect to remote ATP."
2.47 + | string_for_failure TimedOut = "Timed out."
2.48 + | string_for_failure OutOfResources = "The ATP ran out of resources."
2.49 + | string_for_failure OldSpass =
2.50 + "Warning: Isabelle requires a more recent version of SPASS with \
2.51 + \support for the TPTP syntax. To install it, download and extract the \
2.52 + \package \"http://isabelle.in.tum.de/dist/contrib/spass-3.7.tar.gz\" and \
2.53 + \add the \"spass-3.7\" directory's absolute path to " ^
2.54 + quote (Path.implode (Path.expand (Path.appends
2.55 + (Path.variable "ISABELLE_HOME_USER" ::
2.56 + map Path.basic ["etc", "components"])))) ^
2.57 + " on a line of its own."
2.58 + | string_for_failure NoPerl = "Perl" ^ missing_message_tail
2.59 + | string_for_failure NoLibwwwPerl =
2.60 + "The Perl module \"libwww-perl\"" ^ missing_message_tail
2.61 + | string_for_failure MalformedInput =
2.62 + "Internal Isabelle error: The ATP problem is malformed. Please report \
2.63 + \this to the Isabelle developers."
2.64 + | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
2.65 + | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
2.66 +
2.67 +fun known_failure_in_output output =
2.68 + find_first (fn (_, pattern) => String.isSubstring pattern output)
2.69 + #> Option.map fst
2.70 +
2.71 +val known_perl_failures =
2.72 + [(NoPerl, "env: perl"),
2.73 + (NoLibwwwPerl, "Can't locate HTTP")]
2.74
2.75 (* named provers *)
2.76
2.77 @@ -118,6 +158,7 @@
2.78 |> not complete ? prefix "-SOS=1 ",
2.79 proof_delims = [("Here is a proof", "Formulae used in the proof")],
2.80 known_failures =
2.81 + known_perl_failures @
2.82 [(IncompleteUnprovable, "SPASS beiseite: Completion found"),
2.83 (TimedOut, "SPASS beiseite: Ran out of time"),
2.84 (OutOfResources, "SPASS beiseite: Maximal number of loops exceeded"),
2.85 @@ -154,14 +195,15 @@
2.86
2.87 (* Remote prover invocation via SystemOnTPTP *)
2.88
2.89 -val systems = Synchronized.var "atp_systems" ([]: string list)
2.90 +val systems = Synchronized.var "atp_systems" ([] : string list)
2.91
2.92 fun get_systems () =
2.93 - case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w" of
2.94 + case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w 2>&1" of
2.95 (answer, 0) => split_lines answer
2.96 | (answer, _) =>
2.97 - error ("Failed to get available systems at SystemOnTPTP:\n" ^
2.98 - perhaps (try (unsuffix "\n")) answer)
2.99 + error (case known_failure_in_output answer known_perl_failures of
2.100 + SOME failure => string_for_failure failure
2.101 + | NONE => perhaps (try (unsuffix "\n")) answer ^ ".")
2.102
2.103 fun refresh_systems_on_tptp () =
2.104 Synchronized.change systems (fn _ => get_systems ())
2.105 @@ -175,11 +217,6 @@
2.106 NONE => error ("System " ^ quote prefix ^ " not available at SystemOnTPTP.")
2.107 | SOME sys => sys);
2.108
2.109 -val remote_known_failures =
2.110 - [(CantConnect, "HTTP-Error"),
2.111 - (TimedOut, "says Timeout"),
2.112 - (MalformedOutput, "Remote script could not extract proof")]
2.113 -
2.114 fun remote_config atp_prefix
2.115 ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
2.116 prefers_theory_relevant, explicit_forall, ...} : prover_config)
2.117 @@ -190,7 +227,10 @@
2.118 " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
2.119 the_system atp_prefix,
2.120 proof_delims = insert (op =) tstp_proof_delims proof_delims,
2.121 - known_failures = remote_known_failures @ known_failures,
2.122 + known_failures =
2.123 + known_failures @ known_perl_failures @
2.124 + [(CantConnect, "HTTP-Error"),
2.125 + (TimedOut, "says Timeout")],
2.126 max_new_relevant_facts_per_iter = max_new_relevant_facts_per_iter,
2.127 prefers_theory_relevant = prefers_theory_relevant,
2.128 explicit_forall = explicit_forall}
3.1 --- a/src/HOL/Tools/ATP/scripts/remote_atp Thu Jul 29 09:57:10 2010 +0200
3.2 +++ b/src/HOL/Tools/ATP/scripts/remote_atp Thu Jul 29 12:07:09 2010 +0200
3.3 @@ -2,6 +2,7 @@
3.4 #
3.5 # Wrapper for custom remote provers on SystemOnTPTP
3.6 # Author: Fabian Immler, TU Muenchen
3.7 +# Author: Jasmin Blanchette, TU Muenchen
3.8 #
3.9
3.10 use warnings;
3.11 @@ -28,14 +29,14 @@
3.12
3.13 #----Usage
3.14 sub usage() {
3.15 - print("Usage: remote_atp [<options>] <File name>\n");
3.16 - print(" <options> are ...\n");
3.17 - print(" -h - print this help\n");
3.18 - print(" -w - list available ATP systems\n");
3.19 - print(" -s<system> - specified system to use\n");
3.20 - print(" -t<timelimit> - CPU time limit for system\n");
3.21 - print(" -c<command> - custom command for system\n");
3.22 - print(" <File name> - TPTP problem file\n");
3.23 + print("Usage: remote_atp [<options>] <file_name>\n");
3.24 + print("Options:\n");
3.25 + print(" -h print this help\n");
3.26 + print(" -w list available ATPs\n");
3.27 + print(" -s<system> ATP to use\n");
3.28 + print(" -t<time_limit> CPU time limit for ATP\n");
3.29 + print(" -c<command> custom ATP invocation command\n");
3.30 + print(" <file_name> TPTP problem file\n");
3.31 exit(0);
3.32 }
3.33 if (exists($Options{'h'})) {
3.34 @@ -95,13 +96,15 @@
3.35
3.36 #catch errors / failure
3.37 if(!$Response->is_success) {
3.38 - print "HTTP-Error: " . $Response->message . "\n";
3.39 + my $message = $Response->message;
3.40 + $message =~ s/ \(Bad hostname ['"][^'"]*['"]\)//;
3.41 + print $message . "\n";
3.42 exit(-1);
3.43 } elsif (exists($Options{'w'})) {
3.44 print $Response->content;
3.45 exit (0);
3.46 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
3.47 - print "Specified System $1 does not exist\n";
3.48 + print "The ATP \"$1\" is not available at SystemOnTPTP\n";
3.49 exit(-1);
3.50 } else {
3.51 print $Response->content;
4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 09:57:10 2010 +0200
4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Jul 29 12:07:09 2010 +0200
4.3 @@ -148,42 +148,17 @@
4.4
4.5 fun extract_proof_and_outcome complete res_code proof_delims known_failures
4.6 output =
4.7 - case map_filter (fn (failure, pattern) =>
4.8 - if String.isSubstring pattern output then SOME failure
4.9 - else NONE) known_failures of
4.10 - [] => (case extract_proof proof_delims output of
4.11 - "" => ("", SOME UnknownError)
4.12 + case known_failure_in_output output known_failures of
4.13 + NONE => (case extract_proof proof_delims output of
4.14 + "" => ("", SOME MalformedOutput)
4.15 | proof => if res_code = 0 then (proof, NONE)
4.16 else ("", SOME UnknownError))
4.17 - | (failure :: _) =>
4.18 + | SOME failure =>
4.19 ("", SOME (if failure = IncompleteUnprovable andalso complete then
4.20 Unprovable
4.21 else
4.22 failure))
4.23
4.24 -fun string_for_failure Unprovable = "The ATP problem is unprovable."
4.25 - | string_for_failure IncompleteUnprovable =
4.26 - "The ATP cannot prove the problem."
4.27 - | string_for_failure CantConnect = "Can't connect to remote ATP."
4.28 - | string_for_failure TimedOut = "Timed out."
4.29 - | string_for_failure OutOfResources = "The ATP ran out of resources."
4.30 - | string_for_failure OldSpass =
4.31 - (* FIXME: Change the error message below to point to the Isabelle download
4.32 - page once the package is there. *)
4.33 - "Warning: Sledgehammer requires a more recent version of SPASS with \
4.34 - \support for the TPTP syntax. To install it, download and untar the \
4.35 - \package \"http://isabelle.in.tum.de/~blanchet/spass-3.7.tgz\" and add the \
4.36 - \\"spass-3.7\" directory's full path to \"" ^
4.37 - Path.implode (Path.expand (Path.appends
4.38 - (Path.variable "ISABELLE_HOME_USER" ::
4.39 - map Path.basic ["etc", "components"]))) ^
4.40 - "\" on a line of its own."
4.41 - | string_for_failure MalformedInput =
4.42 - "Internal Sledgehammer error: The ATP problem is malformed. Please report \
4.43 - \this to the Isabelle developers."
4.44 - | string_for_failure MalformedOutput = "Error: The ATP output is malformed."
4.45 - | string_for_failure UnknownError = "Error: An unknown ATP error occurred."
4.46 -
4.47
4.48 (* Clause preparation *)
4.49
5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 09:57:10 2010 +0200
5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Jul 29 12:07:09 2010 +0200
5.3 @@ -66,8 +66,7 @@
5.4 | mk_anot phi = AConn (ANot, [phi])
5.5 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
5.6
5.7 -val index_in_shape : int -> int list list -> int =
5.8 - find_index o exists o curry (op =)
5.9 +fun index_in_shape x = find_index (exists (curry (op =) x))
5.10 fun is_axiom_clause_number thm_names num =
5.11 num > 0 andalso num <= Vector.length thm_names andalso
5.12 Vector.sub (thm_names, num - 1) <> ""
5.13 @@ -133,7 +132,8 @@
5.14 which can be hard to disambiguate from function application in an LL(1)
5.15 parser. As a workaround, we extend the TPTP term syntax with such detritus
5.16 and ignore it. *)
5.17 -val parse_vampire_detritus = scan_integer |-- $$ ":" --| scan_integer >> K []
5.18 +fun parse_vampire_detritus x =
5.19 + (scan_integer |-- $$ ":" --| scan_integer >> K []) x
5.20
5.21 fun parse_term pool x =
5.22 ((scan_dollar_name >> repair_name pool)