# HG changeset patch # User blanchet # Date 1280350887 -7200 # Node ID 685d1f0f75b37ba047c1010c61d33f2b4fc058bf # Parent ee7c3c0b0d13a336cb99440b4a878cd50d194f23 handle Perl and "libwww-perl" failures more gracefully, giving the user some clues about what goes on diff -r ee7c3c0b0d13 -r 685d1f0f75b3 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 28 22:18:35 2010 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Wed Jul 28 23:01:27 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,42 @@ 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 untar the \ + \package \"http://www.cl.cam.ac.uk/research/hvg/Isabelle/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, "HTTP")] (* named provers *) @@ -118,6 +159,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 +196,16 @@ (* 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) + (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 +219,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 +229,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 ee7c3c0b0d13 -r 685d1f0f75b3 src/HOL/Tools/ATP/scripts/remote_atp --- a/src/HOL/Tools/ATP/scripts/remote_atp Wed Jul 28 22:18:35 2010 +0200 +++ b/src/HOL/Tools/ATP/scripts/remote_atp Wed Jul 28 23:01:27 2010 +0200 @@ -101,7 +101,7 @@ print $Response->content; exit (0); } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { - print "Specified System $1 does not exist\n"; + print "Specified system $1 does not exist\n"; exit(-1); } else { print $Response->content; diff -r ee7c3c0b0d13 -r 685d1f0f75b3 src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 22:18:35 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed Jul 28 23:01:27 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 *)