# HG changeset patch # User immler@in.tum.de # Date 1232463957 -3600 # Node ID 479a2fce65e6249108d7bdd5bdbc8b3303c0b71b # Parent 1f007b7b8ad3b7cf5a52d84924b6f8c020d1c064 modified remote script; modified handling of errors diff -r 1f007b7b8ad3 -r 479a2fce65e6 contrib/SystemOnTPTP/remote --- a/contrib/SystemOnTPTP/remote Mon Jan 19 20:24:10 2009 +0100 +++ b/contrib/SystemOnTPTP/remote Tue Jan 20 16:05:57 2009 +0100 @@ -3,86 +3,137 @@ # Wrapper for custom remote provers on SystemOnTPTP # Author: Fabian Immler, TU Muenchen # -# Usage: ./remote prover timelimit problemfile -# -# where prover should be the name of the System from http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP -# tested and working with the standard settings: -# -# ./remote Vampire---9.0 timelimit file -# ./remote SPASS---3.01 timelimit file -# ./remote EP---1.0 timelimit file use warnings; use strict; - use Getopt::Std; use HTTP::Request::Common; -use LWP::UserAgent; +use LWP; -# address of proof-server my $SystemOnTPTPFormReplyURL = "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply"; -if(scalar(@ARGV) != 3) { - print "usage: "; - exit -1; -} -my $prover = shift(@ARGV); -my $timelimit = shift(@ARGV); -my $problem = [shift(@ARGV)]; - -# fill in form +# default parameters my %URLParameters = ( "NoHTML" => 1, "QuietFlag" => "-q01", "X2TPTP" => "-S", "SubmitButton" => "RunSelectedSystems", "ProblemSource" => "UPLOAD", - "UPLOADProblem" => $problem, - "System___$prover" => "$prover", - "TimeLimit___$prover" => "$timelimit", -); + ); + +# check connection +my $TestAgent = LWP::UserAgent->new; +$TestAgent->timeout(5); +my $TestRequest = GET($SystemOnTPTPFormReplyURL); +my $TestResponse = $TestAgent->request($TestRequest); +if(! $TestResponse->is_success) { + print "HTTP-Error: " . $TestResponse->message . "\n"; + exit(-1); +} + +#----Get format and transform options if specified +my %Options; +getopts("hws:t:c:",\%Options); + +#----Usage +if (exists($Options{'h'})) { + print("Usage: remote []\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"); + exit(0); +} + +#----What systems flag +if (exists($Options{'w'})) { + $URLParameters{"SubmitButton"} = "ListSystems"; + delete($URLParameters{"ProblemSource"}); +} +#----Selected system +my $System; +if (exists($Options{'s'})) { + $System = $Options{'s'}; +} else { + # use Vampire as default + $System = "Vampire---9.0"; +} +$URLParameters{"System___$System"} = $System; + +#----Time limit +if (exists($Options{'t'})) { + $URLParameters{"TimeLimit___$System"} = $Options{'t'}; +} +#----Custom command +if (exists($Options{'c'})) { + $URLParameters{"Command___$System"} = $Options{'c'}; +} + +#----Get single file name +if (exists($URLParameters{"ProblemSource"})) { + if (scalar(@ARGV) >= 1) { + $URLParameters{"UPLOADProblem"} = [shift(@ARGV)]; + } else { +die("Missing problem file"); + } +} # Query Server my $Agent = LWP::UserAgent->new; +if (exists($Options{'t'})) { + # give server more time to respond + $Agent->timeout($Options{'t'} * 2 + 10); +} my $Request = POST($SystemOnTPTPFormReplyURL, Content_Type => 'form-data',Content => \%URLParameters); my $Response = $Agent->request($Request); - -#catch errors, let isabelle/watcher know -if($Response->is_success && $Response->content !~ /NO SOLUTION OUTPUT BY SYSTEM/ -&& $Response->content =~ m/%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/){ - # convert to isabelle-friendly format - my @lines = split( /%\s*Result\s*:\s*Unsatisfiable.*?\n%\s*Output\s*:\s*.*?Refutation.*?\n/, $Response->content); - @lines = split( /\n/, $lines[1]); my $extract = ""; - my $inproof = 0 > 1; - my $ende = 0 > 1; + +#catch errors / failure +if(! $Response->is_success){ + print "HTTP-Error: " . $Response->message . "\n"; + exit(-1); +} elsif (exists($Options{'w'})) { + print $Response->content; + exit (0); +} elsif ($Response->content =~ /NO SOLUTION OUTPUT BY SYSTEM/){ + if ($Response->content =~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) { + print "No Solution Output\nResult: $1\nOutput: $2\n"; + } else { + print "No Solution Output\n"; + } + exit(-1); +} elsif ($Response->content =~ /ERROR: Could not form TPTP format derivation/) { + print "Could not form TPTP format derivation\n"; + exit(-1); +} elsif ($Response->content =~ /WARNING: (\S*) does not exist/) { + print "Specified System $1 does not exist\n"; + exit(-1); +} elsif ($Response->content =~ /^\s*$/) { + print "Empty response (specified bad system? Inappropriate problem file format?)\n"; + exit(-1); +} elsif ($Response->content !~ /%\s*Result\s*:(.*)\n%\s*Output\s*:(.*)\n%/) { + print "Bad response: \n".$Response->content; + exit(-1); +} else { + my @lines = split( /\n/, $Response->content); + my $extract = ""; foreach my $line (@lines){ - if(! $ende){ - #ignore comments - if(! $inproof){ - if ($line !~ /^%/ && !($line eq "")) { - $extract .= "$line"; - $inproof = 1; - } - } else { - if ($line !~ /^%/) { - $extract .= "$line"; - } else { - $ende = 1; - } - } + #ignore comments + if ($line !~ /^%/ && !($line eq "")) { + $extract .= "$line"; } } - # insert newlines after '.' + # insert newlines after ').' $extract =~ s/\s//g; $extract =~ s/\)\.cnf/\)\.\ncnf/g; + + # orientation for res_reconstruct.ML print "# SZS output start CNFRefutation.\n"; print "$extract\n"; print "# SZS output end CNFRefutation.\n"; -} else { - print "HTTP-Request: " . $Response->message; - print "\nResponse: " . $Response->content; - print "\nCANNOT PROVE: \n"; - print $Response->content; + exit(0); } diff -r 1f007b7b8ad3 -r 479a2fce65e6 src/HOL/ATP_Linkup.thy --- a/src/HOL/ATP_Linkup.thy Mon Jan 19 20:24:10 2009 +0100 +++ b/src/HOL/ATP_Linkup.thy Tue Jan 20 16:05:57 2009 +0100 @@ -112,12 +112,12 @@ setup {* AtpManager.add_prover "spass_no_tc" (AtpWrapper.spass_opts 40 false) *} text {* remote provers via SystemOnTPTP *} -setup {* AtpManager.add_prover "remote_vamp9" - (AtpWrapper.remote_prover "Vampire---9.0" 90) *} +setup {* AtpManager.add_prover "remote_vampire" + (AtpWrapper.remote_prover "-s Vampire---9.0 -t 100") *} setup {* AtpManager.add_prover "remote_spass" - (AtpWrapper.remote_prover "SPASS---3.01" 90) *} + (AtpWrapper.remote_prover "-s SPASS---3.01 -t 100") *} setup {* AtpManager.add_prover "remote_e" - (AtpWrapper.remote_prover "EP---1.0" 90) *} + (AtpWrapper.remote_prover "-s EP---1.0 -t 100") *} diff -r 1f007b7b8ad3 -r 479a2fce65e6 src/HOL/Tools/atp_manager.ML --- a/src/HOL/Tools/atp_manager.ML Mon Jan 19 20:24:10 2009 +0100 +++ b/src/HOL/Tools/atp_manager.ML Tue Jan 20 16:05:57 2009 +0100 @@ -35,9 +35,9 @@ local -val atps = ref "e"; +val atps = ref "e remote_e remore_vampire remote_spass"; val max_atps = ref 5; (* ~1 means infinite number of atps *) -val timeout = ref 60; +val timeout = ref 100; in diff -r 1f007b7b8ad3 -r 479a2fce65e6 src/HOL/Tools/atp_wrapper.ML --- a/src/HOL/Tools/atp_wrapper.ML Mon Jan 19 20:24:10 2009 +0100 +++ b/src/HOL/Tools/atp_wrapper.ML Tue Jan 20 16:05:57 2009 +0100 @@ -12,7 +12,7 @@ val external_prover: ((int -> Path.T) -> Proof.context * thm list * thm -> string list * ResHolClause.axiom_name Vector.vector list) -> Path.T * string -> - (string * int -> bool) -> + (string -> string option) -> (string * string vector * Proof.context * thm * int -> string) -> AtpManager.prover val tptp_prover_opts_full: int -> bool -> bool -> Path.T * string -> AtpManager.prover @@ -30,8 +30,8 @@ val eprover_full: AtpManager.prover val spass_opts: int -> bool -> AtpManager.prover val spass: AtpManager.prover - val remote_prover_opts: int -> bool -> string -> int -> AtpManager.prover - val remote_prover: string -> int -> AtpManager.prover + val remote_prover_opts: int -> bool -> string -> AtpManager.prover + val remote_prover: string -> AtpManager.prover end; structure AtpWrapper: ATP_WRAPPER = @@ -47,7 +47,7 @@ (* basic template *) -fun external_prover write_problem_files (cmd, args) check_success produce_answer subgoalno state = +fun external_prover write_problem_files (cmd, args) find_failure produce_answer subgoalno state = let (* path to unique problem file *) val destdir' = ! destdir @@ -70,19 +70,18 @@ if File.exists cmd then File.shell_path cmd ^ " " ^ args else error ("Bad executable: " ^ Path.implode cmd) val (proof, rc) = system_out (cmdline ^ " " ^ nth filenames (subgoalno - 1)) - val _ = - if rc <> 0 then - warning ("Sledgehammer prover exited with return code " ^ string_of_int rc ^ "\n" ^ cmdline) - else () (* remove *temporary* files *) val _ = if destdir' = "" then List.app OS.FileSys.remove filenames else () - - val success = check_success (proof, rc) + + (* check for success and print out some information on failure *) + val failure = find_failure proof + val success = (rc = 0) andalso (not (isSome failure)) val message = - if success - then "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) - else "Failed." + if isSome failure then "Could not prove: " ^ the failure + else if rc <> 0 + then "Exited with return code " ^ string_of_int rc ^ ": " ^ proof + else "Try this command: " ^ produce_answer (proof, thm_names, ctxt, goal, subgoalno) in (success, message) end; @@ -95,7 +94,7 @@ external_prover (ResAtp.write_problem_files ResHolClause.tptp_write_file max_new theory_const) command - ResReconstruct.check_success_e_vamp_spass + ResReconstruct.find_failure_e_vamp_spass (if full then ResReconstruct.structured_proof else ResReconstruct.lemma_list_tstp); (*arbitrary ATP with TPTP input/output and problemfile as last argument*) @@ -148,7 +147,7 @@ fun spass_opts max_new theory_const = external_prover (ResAtp.write_problem_files ResHolClause.dfg_write_file max_new theory_const) (Path.explode "$SPASS_HOME/SPASS", "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof") - ResReconstruct.check_success_e_vamp_spass + ResReconstruct.find_failure_e_vamp_spass ResReconstruct.lemma_list_dfg; val spass = spass_opts 40 true; @@ -156,9 +155,9 @@ (* remote prover invocation via SystemOnTPTP *) -fun remote_prover_opts max_new theory_const name timelimit = +fun remote_prover_opts max_new theory_const args = tptp_prover_opts max_new theory_const - (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", name ^ " " ^ (string_of_int timelimit)); + (Path.explode "$ISABELLE_HOME/contrib/SystemOnTPTP/remote", args); val remote_prover = remote_prover_opts 60 false; diff -r 1f007b7b8ad3 -r 479a2fce65e6 src/HOL/Tools/res_reconstruct.ML --- a/src/HOL/Tools/res_reconstruct.ML Mon Jan 19 20:24:10 2009 +0100 +++ b/src/HOL/Tools/res_reconstruct.ML Tue Jan 20 16:05:57 2009 +0100 @@ -15,7 +15,7 @@ val strip_prefix: string -> string -> string option val setup: Context.theory -> Context.theory (* extracting lemma list*) - val check_success_e_vamp_spass: string * int -> bool + val find_failure_e_vamp_spass: string -> string option val lemma_list_dfg: string * string vector * Proof.context * Thm.thm * int -> string val lemma_list_tstp: string * string vector * Proof.context * Thm.thm * int -> string (* structured proofs *) @@ -463,10 +463,9 @@ val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; val failure_strings_SPASS = ["SPASS beiseite: Completion found.","SPASS beiseite: Ran out of time.", "SPASS beiseite: Maximal number of loops exceeded."]; - fun check_success_e_vamp_spass (proof, rc) = - not (exists (fn s => String.isSubstring s proof) - (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS)) - andalso (rc = 0); + fun find_failure_e_vamp_spass proof = + hd (map (fn s => if String.isSubstring s proof then SOME s else NONE) + (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS)); (*=== EXTRACTING PROOF-TEXT === *)