# HG changeset patch # User blanchet # Date 1280398029 -7200 # Node ID 81ead4aaba2d3876309803086737e39584b093a0 # Parent a9b52497661caf90455271655a7b4995e690235d# Parent 9cb8f5432dfcad303df790bf3dd18fbdc8bee721 merged diff -r a9b52497661c -r 81ead4aaba2d doc-src/Sledgehammer/sledgehammer.tex --- 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 diff -r a9b52497661c -r 81ead4aaba2d src/HOL/Tools/ATP/atp_systems.ML --- 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} diff -r a9b52497661c -r 81ead4aaba2d src/HOL/Tools/ATP/scripts/remote_atp --- 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 [] \n"); - print(" are ...\n"); - print(" -h - print this help\n"); - print(" -w - list available ATP systems\n"); - print(" -s - specified system to use\n"); - print(" -t - CPU time limit for system\n"); - print(" -c - custom command for system\n"); - print(" - TPTP problem file\n"); + print("Usage: remote_atp [] \n"); + print("Options:\n"); + print(" -h print this help\n"); + print(" -w list available ATPs\n"); + print(" -s ATP to use\n"); + print(" -t CPU time limit for ATP\n"); + print(" -c custom ATP invocation command\n"); + print(" 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; diff -r a9b52497661c -r 81ead4aaba2d src/HOL/Tools/Sledgehammer/sledgehammer.ML --- 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 *) diff -r a9b52497661c -r 81ead4aaba2d src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- 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)