# HG changeset patch # User quigley # Date 1120485116 -7200 # Node ID 96bdc59afc0570cd171d5cf43bb3edff7f63ce7e # Parent bf2cd93cc245b9d7ab34cd508805a36d2957bf97 Streamlined the signal handler in watcher.ML diff -r bf2cd93cc245 -r 96bdc59afc05 src/HOL/Tools/ATP/VampCommunication.ML --- a/src/HOL/Tools/ATP/VampCommunication.ML Mon Jul 04 15:15:55 2005 +0200 +++ b/src/HOL/Tools/ATP/VampCommunication.ML Mon Jul 04 15:51:56 2005 +0200 @@ -184,16 +184,36 @@ Posix.Process.sleep(Time.fromSeconds 1); true end) - else if (thisLine = "% Proof not found.\n") + else if (thisLine = "% Proof not found. Time limit expired.\n") then - ( - Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); - TextIO.output (toParent,childCmd^"\n" ); - TextIO.flushOut toParent; - TextIO.output (toParent, thisLine); - TextIO.flushOut toParent; + (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_proof"))); (* val _ = Posix.Process.sleep(Time.fromSeconds 3 );*) + val _ = TextIO.output (outfile, (thisLine)) + + val _ = TextIO.closeOut outfile + in - true) + TextIO.output (toParent,childCmd^"\n" ); + TextIO.flushOut toParent; + TextIO.output (vamp_proof_file, (thisLine)); + TextIO.flushOut vamp_proof_file; + TextIO.closeOut vamp_proof_file; + (*TextIO.output (toParent, thisLine); + TextIO.flushOut toParent; + TextIO.output (toParent, "bar\n"); + TextIO.flushOut toParent;*) + + TextIO.output (toParent, thisLine^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, thmstring^"\n"); + TextIO.flushOut toParent; + TextIO.output (toParent, goalstring^"\n"); + TextIO.flushOut toParent; + Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); + (* Attempt to prevent several signals from turning up simultaneously *) + Posix.Process.sleep(Time.fromSeconds 1); + true + end + ) else (TextIO.output (vamp_proof_file, (thisLine)); @@ -238,7 +258,7 @@ (reconstr, thmstring, goalstring) end ) - else if (thisLine = "% Proof not found.\n") + else if (thisLine = "% Proof not found. Time limit expired.\n") then ( let val reconstr = thisLine diff -r bf2cd93cc245 -r 96bdc59afc05 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Mon Jul 04 15:15:55 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Mon Jul 04 15:51:56 2005 +0200 @@ -165,8 +165,8 @@ (prover^thmstring^goalstring^proverCmd^settings^ clasimpfile^hypsfile^probfile) in sendOutput (toWatcherStr, - (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^ - settings^"*"^clasimpfile^"*"^hypsfile^"*"^probfile^"\n")); + (prover^"$"^thmstring^"$"^goalstring^"$"^proverCmd^"$"^ + settings^"$"^clasimpfile^"$"^hypsfile^"$"^probfile^"\n")); goals_being_watched := (!goals_being_watched) + 1; TextIO.flushOut toWatcherStr; callResProvers (toWatcherStr,args) @@ -213,33 +213,33 @@ let val outfile = TextIO.openAppend(*("sep_field")*)(File.platform_path(File.tmp_path (Path.basic "sep_field"))) val _ = TextIO.output (outfile,("In separateFields, str is: "^(implode str)^"\n\n") ) val _ = TextIO.closeOut outfile - val (prover, rest) = takeUntil "*" str [] + val (prover, rest) = takeUntil "$" str [] val prover = implode prover - val (thmstring, rest) = takeUntil "*" rest [] + val (thmstring, rest) = takeUntil "$" rest [] val thmstring = implode thmstring - val (goalstring, rest) = takeUntil "*" rest [] + val (goalstring, rest) = takeUntil "$" rest [] val goalstring = implode goalstring - val (proverCmd, rest ) = takeUntil "*" rest [] + val (proverCmd, rest ) = takeUntil "$" rest [] val proverCmd = implode proverCmd - val (settings, rest) = takeUntil "*" rest [] + val (settings, rest) = takeUntil "$" rest [] val settings = getSettings settings [] - val (clasimpfile, rest ) = takeUntil "*" rest [] + val (clasimpfile, rest ) = takeUntil "$" rest [] val clasimpfile = implode clasimpfile - val (hypsfile, rest ) = takeUntil "*" rest [] + val (hypsfile, rest ) = takeUntil "$" rest [] val hypsfile = implode hypsfile - val (file, rest) = takeUntil "*" rest [] + val (file, rest) = takeUntil "$" rest [] val file = implode file val _ = File.append (File.tmp_path (Path.basic "sep_comms")) ("Sep comms are: "^(implode str)^"**"^ - prover^thmstring^goalstring^proverCmd^clasimpfile^hypsfile^file^"\n\n") + prover^" thmstring: "^thmstring^"\n goalstr: "^goalstring^" \n provercmd: "^proverCmd^" \n clasimp "^clasimpfile^" \n hyps "^hypsfile^"\n prob "^file^"\n\n") in (prover,thmstring,goalstring, proverCmd, settings, clasimpfile, hypsfile, file) end @@ -289,6 +289,7 @@ val newfile = if !SpassComm.spass then dfg_path^"/ax_prob"^"_"^(probID)^".dfg" + else (File.platform_path wholefile) val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher")) @@ -813,6 +814,8 @@ VampComm.getVampInput childin; Pretty.writeln(Pretty.str (oct_char "361"));() ) + + fun spass_proofHandler (n) = ( let val outfile = TextIO.openAppend(File.platform_path(File.tmp_path (Path.basic "foo_signal1"))); val _ = TextIO.output (outfile, ("In signal handler now\n")) @@ -844,9 +847,8 @@ else () ) - (* if there's no proof, but a message from Spass *) - else if ((substring (reconstr, 0,5))= "SPASS") - then + (* if there's no proof, but a some sort of message from Spass *) + else ( goals_being_watched := (!goals_being_watched) -1; Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); @@ -862,67 +864,7 @@ end ) else () - ) - (* print out a list of rules used from clasimpset*) - else if ((substring (reconstr, 0,5))= "Rules") - then - ( - goals_being_watched := (!goals_being_watched) -1; - Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^reconstr)); - Pretty.writeln(Pretty.str (oct_char "361")); - if (!goals_being_watched = 0) - then - (let val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "foo_reap_comp"))); - val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) - val _ = TextIO.closeOut outfile - in - killWatcher (childpid); reapWatcher (childpid,childin, childout);() - end ) - else - () - ) - - (* if proof translation failed *) - else if ((substring (reconstr, 0,5)) = "Proof") - then - ( - goals_being_watched := (!goals_being_watched) -1; - Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str (goalstring^(Recon_Transfer.restore_linebreaks reconstr))); - Pretty.writeln(Pretty.str (oct_char "361")); - if (!goals_being_watched = 0) - then - (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp"))); - val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) - val _ = TextIO.closeOut outfile - in - killWatcher (childpid); reapWatcher (childpid,childin, childout); () - end ) - else - ( ) - ) - - - else (* add something here ?*) - ( - goals_being_watched := (!goals_being_watched) -1; - Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")]))); - Pretty.writeln(Pretty.str ("Ran out of options in handler")); - Pretty.writeln(Pretty.str (oct_char "361")); - if (!goals_being_watched = 0) - then - (let val outfile = TextIO.openOut(File.platform_path (File.tmp_path (Path.basic "foo_reap_comp"))); - val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")) - val _ = TextIO.closeOut outfile - in - killWatcher (childpid); reapWatcher (childpid,childin, childout); () - end ) - else - ( ) - ) - - + ) end) diff -r bf2cd93cc245 -r 96bdc59afc05 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Mon Jul 04 15:15:55 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Mon Jul 04 15:51:56 2005 +0200 @@ -48,7 +48,6 @@ (*val spass = ref true;*) val custom_spass = ref ["Auto=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub","-DocProof","-TimeLimit=60"]; - val vampire = ref false; val trace_res = ref false; @@ -209,7 +208,7 @@ else let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vkernel" in - ([("vampire", thmstr, goalstring, vampire, "-t 300%-m 100000", + ([("vampire", thmstr, goalstring, vampire, "-t 60%-m 100000", clasimpfile, axfile, hypsfile, probfile)] @ (make_atp_list xs sign (n+1))) end