# HG changeset patch # User paulson # Date 1117119007 -7200 # Node ID 9169bdf930f8a1e6ef14ac373c22d192db005dd3 # Parent f084ba24de29f521a01255c2df27bbd0e32482ec trying to set up portable calling sequences for SPASS and tptp2X diff -r f084ba24de29 -r 9169bdf930f8 src/HOL/Tools/ATP/modUnix.ML --- a/src/HOL/Tools/ATP/modUnix.ML Thu May 26 10:05:28 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,280 +0,0 @@ -(* ID: $Id$ - Author: Claire Quigley - Copyright 2004 University of Cambridge -*) - -(****************************************************************) -(****** Slightly modified version of sml Unix structure *********) -(****************************************************************) - - -structure modUnix: MODUNIX = - struct - -type signal = Posix.Signal.signal -datatype exit_status = datatype Posix.Process.exit_status - -val fromStatus = Posix.Process.fromStatus - - -fun reap(pid, instr, outstr) = - let - val u = TextIO.closeIn instr; - val u = TextIO.closeOut outstr; - - val (_, status) = - Posix.Process.waitpid(Posix.Process.W_CHILD pid, []) - in - status - end - -fun fdReader (name : string, fd : Posix.IO.file_desc) = - Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd }; - -fun fdWriter (name, fd) = - Posix.IO.mkTextWriter { - appendMode = false, - initBlkMode = true, - name = name, - chunkSize=4096, - fd = fd - }; - -fun openOutFD (name, fd) = - TextIO.mkOutstream ( - TextIO.StreamIO.mkOutstream ( - fdWriter (name, fd), IO.BLOCK_BUF)); - -fun openInFD (name, fd) = - TextIO.mkInstream ( - TextIO.StreamIO.mkInstream ( - fdReader (name, fd), "")); - - - - - -(*****************************************) -(* The result of calling createWatcher *) -(*****************************************) - -datatype proc = PROC of { - pid : Posix.Process.pid, - instr : TextIO.instream, - outstr : TextIO.outstream - }; - - - -(*****************************************) -(* The result of calling executeToList *) -(*****************************************) - -datatype cmdproc = CMDPROC of { - prover: string, (* Name of the resolution prover used, e.g. Vampire, SPASS *) - cmd: string, (* The file containing the goal for res prover to prove *) - thmstring: string, (* string representation of subgoal after negation, skolemization*) - goalstring: string, (* string representation of subgoal*) - pid : Posix.Process.pid, - instr : TextIO.instream, (* Input stream to child process *) - outstr : TextIO.outstream (* Output stream from child process *) - }; - - - -fun killChild pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill); - -fun childInfo (PROC{pid,instr,outstr}) = ((pid, (instr,outstr))); - -fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr); - -fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr); - -fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover,(cmd,(pid, (instr,outstr)))); - -fun cmdchildPid (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (pid); - -fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (prover); - -fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (thmstring); - -fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,pid,instr,outstr}) = (goalstring); -(***************************************************************************) -(* Takes a command - e.g. 'vampire', a list of arguments for the command, *) -(* and a list of currently running processes. Creates a new process for *) -(* cmd and argv and adds it to procList *) -(***************************************************************************) - - - - -fun mySshExecuteToList (cmd, argv, procList) = let - val p1 = Posix.IO.pipe () - val p2 = Posix.IO.pipe () - val prover = hd argv - val thmstring = hd(tl argv) - val goalstring = hd(tl(tl argv)) - val argv = tl (tl argv) - - (* Turn the arguments into a single string. Perhaps we should quote the - arguments. *) - fun convArgs [] = [] - | convArgs [s] = [s] - | convArgs (hd::tl) = hd :: " " :: convArgs tl - val cmd_args = concat(convArgs(cmd :: argv)) - - fun closep () = ( - Posix.IO.close (#outfd p1); - Posix.IO.close (#infd p1); - Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p2) - ) - fun startChild () =(case Posix.Process.fork() - of SOME pid => pid (* parent *) - | NONE => let - val oldchildin = #infd p1 - val newchildin = Posix.FileSys.wordToFD 0w0 - val oldchildout = #outfd p2 - val newchildout = Posix.FileSys.wordToFD 0w1 - (*val args = (["shep"]@([cmd]@argv)) - val newcmd = "/usr/bin/ssh"*) - - in - Posix.IO.close (#outfd p1); - Posix.IO.close (#infd p2); - Posix.IO.dup2{old = oldchildin, new = newchildin}; - Posix.IO.close oldchildin; - Posix.IO.dup2{old = oldchildout, new = newchildout}; - Posix.IO.close oldchildout; - (* Run the command. *) - (* Run this as a shell command. The command and arguments have - to be a single argument. *) - Posix.Process.exec("/bin/sh", ["sh", "-c", cmd_args]) - (*Posix.Process.exec(newcmd, args)*) - end - (* end case *)) - val _ = TextIO.flushOut TextIO.stdOut - val pid = (startChild ()) handle ex => (closep(); raise ex) - val instr = openInFD ("_exec_in", #infd p2) - val outstr = openOutFD ("_exec_out", #outfd p1) - val cmd = hd (rev argv) - in - (* close the child-side fds *) - Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p1); - (* set the fds close on exec *) - Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - (((CMDPROC{ - prover = prover, - cmd = cmd, - thmstring = thmstring, - goalstring = goalstring, - pid = pid, - instr = instr, - outstr = outstr - })::procList)) - end; - - -fun myexecuteInEnv (cmd, argv, env) = let - val p1 = Posix.IO.pipe () - val p2 = Posix.IO.pipe () - fun closep () = ( - Posix.IO.close (#outfd p1); - Posix.IO.close (#infd p1); - Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p2) - ) - fun startChild () =(case Posix.Process.fork() - of SOME pid => pid (* parent *) - | NONE => let - val oldchildin = #infd p1 - val newchildin = Posix.FileSys.wordToFD 0w0 - val oldchildout = #outfd p2 - val newchildout = Posix.FileSys.wordToFD 0w1 - in - Posix.IO.close (#outfd p1); - Posix.IO.close (#infd p2); - Posix.IO.dup2{old = oldchildin, new = newchildin}; - Posix.IO.close oldchildin; - Posix.IO.dup2{old = oldchildout, new = newchildout}; - Posix.IO.close oldchildout; - Posix.Process.exece(cmd, argv, env) - end - (* end case *)) - val _ = TextIO.flushOut TextIO.stdOut - val pid = (startChild ()) handle ex => (closep(); raise ex) - val instr = openInFD ("_exec_in", #infd p2) - val outstr = openOutFD ("_exec_out", #outfd p1) - in - (* close the child-side fds *) - Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p1); - (* set the fds close on exec *) - Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - PROC{pid = pid, - instr = instr, - outstr = outstr - } - end; - - - - -fun myexecuteToList (cmd, argv, procList) = let - val p1 = Posix.IO.pipe () - val p2 = Posix.IO.pipe () - val prover = hd argv - val thmstring = hd(tl argv) - val goalstring = hd(tl(tl argv)) - val argv = tl (tl (tl(argv))) - - fun closep () = ( - Posix.IO.close (#outfd p1); - Posix.IO.close (#infd p1); - Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p2) - ) - fun startChild () =(case Posix.Process.fork() - of SOME pid => pid (* parent *) - | NONE => let - val oldchildin = #infd p1 - val newchildin = Posix.FileSys.wordToFD 0w0 - val oldchildout = #outfd p2 - val newchildout = Posix.FileSys.wordToFD 0w1 - in - Posix.IO.close (#outfd p1); - Posix.IO.close (#infd p2); - Posix.IO.dup2{old = oldchildin, new = newchildin}; - Posix.IO.close oldchildin; - Posix.IO.dup2{old = oldchildout, new = newchildout}; - Posix.IO.close oldchildout; - Posix.Process.exec(cmd, argv) - end - (* end case *)) - val _ = TextIO.flushOut TextIO.stdOut - val pid = (startChild ()) handle ex => (closep(); raise ex) - val instr = openInFD ("_exec_in", #infd p2) - val outstr = openOutFD ("_exec_out", #outfd p1) - val cmd = hd (rev argv) - in - (* close the child-side fds *) - Posix.IO.close (#outfd p2); - Posix.IO.close (#infd p1); - (* set the fds close on exec *) - Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); - (((CMDPROC{ - prover = prover, - cmd = cmd, - thmstring = thmstring, - goalstring = goalstring, - pid = pid, - instr = instr, - outstr = outstr - })::procList)) - end; - -end; diff -r f084ba24de29 -r 9169bdf930f8 src/HOL/Tools/ATP/spassshell --- a/src/HOL/Tools/ATP/spassshell Thu May 26 10:05:28 2005 +0200 +++ b/src/HOL/Tools/ATP/spassshell Thu May 26 16:50:07 2005 +0200 @@ -1,4 +1,4 @@ -`isatool getenv -b SPASS_HOME` $* |testoutput.py +`isatool getenv -b SPASS_HOME`/SPASS $* |testoutput.py #$SPASS_HOME $* |testoutput.py diff -r f084ba24de29 -r 9169bdf930f8 src/HOL/Tools/ATP/testoutput.py --- a/src/HOL/Tools/ATP/testoutput.py Thu May 26 10:05:28 2005 +0200 +++ b/src/HOL/Tools/ATP/testoutput.py Thu May 26 16:50:07 2005 +0200 @@ -3,15 +3,6 @@ import string import sys -f = open ("/tmp/args", "w") -for x in sys.argv: - f.write("%s " % x) -f.write("\n") -f.close() - -#f = open ("/home/clq20/scratch/13354/dfg/spassprooflist", "r") -#f = open ("/home/clq20/testoutput.py", "r") - mode = 0 try: while 1: @@ -29,25 +20,5 @@ pass #f.close() - - - sys.exit() -for i in range(0, 50): - print "blah gibberish nonsense" - -print """Here is a proof with depth 1, length 9 : -2[0:Inp] || v_P(tconst_fun(typ__Ha,tconst_bool),v_x)* -> v_P(tconst_fun(typ__Ha,tconst_bool),U)*. -3[0:Inp] || v_P(tconst_fun(typ__Ha,tconst_bool),U)*+ -> v_P(tconst_fun(typ__Ha,tconst_bool),v_x)*. -4[0:Inp] || -> v_P(tconst_fun(typ__Ha,tconst_bool),U)* v_P(tconst_fun(typ__Ha,tconst_bool),v_xa)*. -5[0:Inp] || v_P(tconst_fun(typ__Ha,tconst_bool),v_xb)* v_P(tconst_fun(typ__Ha,tconst_bool),U)* -> . -6[0:Con:4.0] || -> v_P(tconst_fun(typ__Ha,tconst_bool),v_xa)*. -7[0:Con:5.1] || v_P(tconst_fun(typ__Ha,tconst_bool),v_xb)* -> . -8[0:Res:6.0,3.0] || -> v_P(tconst_fun(typ__Ha,tconst_bool),v_x)*. -9[0:MRR:2.0,8.0] || -> v_P(tconst_fun(typ__Ha,tconst_bool),U)*. -10[0:UnC:9.0,7.0] || -> . -Formulae used in the proof : - ---------------------------SPASS-STOP------------------------------ -""" diff -r f084ba24de29 -r 9169bdf930f8 src/HOL/Tools/ATP/watcher.ML --- a/src/HOL/Tools/ATP/watcher.ML Thu May 26 10:05:28 2005 +0200 +++ b/src/HOL/Tools/ATP/watcher.ML Thu May 26 16:50:07 2005 +0200 @@ -15,8 +15,7 @@ (*use "Proof_Transfer"; use "VampireCommunication"; -use "SpassCommunication"; -use "modUnix";*) +use "SpassCommunication";*) (*use "/homes/clq20/Jia_Code/TransStartIsar";*) @@ -137,12 +136,9 @@ fun getCmd cmdStr = let val backList = ((rev(explode cmdStr))) in - if (String.isPrefix "\n" (implode backList )) - then - (implode (rev ((tl backList)))) - else - (cmdStr) + then (implode (rev ((tl backList)))) + else cmdStr end (********************************************************************************) @@ -150,16 +146,12 @@ (********************************************************************************) fun callResProver (toWatcherStr, arg) = (sendOutput (toWatcherStr, arg^"\n"); - TextIO.flushOut toWatcherStr - - ) + TextIO.flushOut toWatcherStr) (*****************************************************************************************) (* Send request to Watcher for multiple provers to be called for filenames in arg *) (*****************************************************************************************) - - (* need to modify to send over hyps file too *) fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n"); TextIO.flushOut toWatcherStr) @@ -177,14 +169,14 @@ (*** only include problem and clasimp for the moment, not sure how to refer to ***) (*** hyps/local axioms just now ***) val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)]) - val dfg_create =if File.exists dfg_dir - then - ((warning("dfg dir exists"));()) - else - File.mkdir dfg_dir; + val dfg_create = if File.exists dfg_dir + then warning("dfg dir exists") + else File.mkdir dfg_dir; val dfg_path = File.sysify_path dfg_dir; - val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path]) + val exec_tptp2x = + Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", + ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]) (*val _ = Posix.Process.wait ()*) (*val _ =Unix.reap exec_tptp2x*) val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg" @@ -192,16 +184,20 @@ in goals_being_watched := (!goals_being_watched) + 1; Posix.Process.sleep(Time.fromSeconds 1); - (warning ("probfile is: "^probfile)); + (warning ("probfile is: "^probfile)); (warning("dfg file is: "^newfile)); (warning ("wholefile is: "^(File.sysify_path wholefile))); - sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n")); + sendOutput (toWatcherStr, + prover ^ "*" ^ thmstring ^ "*" ^ goalstring ^ "*" ^ proverCmd ^ + "*" ^ settings ^ "*" ^ newfile ^ "\n"); (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*) TextIO.flushOut toWatcherStr; - Unix.reap exec_tptp2x; - - callResProvers (toWatcherStr,args) - + Unix.reap exec_tptp2x; + if File.exists + (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg"))) + then callResProvers (toWatcherStr, args) + else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^ + " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path) end (* fun callResProversStr (toWatcherStr, []) = "End of calls\n" diff -r f084ba24de29 -r 9169bdf930f8 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu May 26 10:05:28 2005 +0200 +++ b/src/HOL/Tools/res_atp.ML Thu May 26 16:50:07 2005 +0200 @@ -144,67 +144,66 @@ (* should be modified to allow other provers to be called *) (*********************************************************************) -fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = let - val thmstring = Meson.concat_with_and (map string_of_thm thms) - val thm_no = length thms - val _ = warning ("number of thms is : "^(string_of_int thm_no)) - val _ = warning ("thmstring in call_res is: "^thmstring) - - val goalstr = Sign.string_of_term sign sg_term - val goalproofstring = proofstring goalstr - val no_returns =List.filter not_newline ( goalproofstring) - val goalstring = implode no_returns - val _ = warning ("goalstring in call_res is: "^goalstring) - - (*val prob_file =File.tmp_path (Path.basic newprobfile); *) - (*val _ =( warning ("calling make_clauses ")) - val clauses = make_clauses thms - val _ =( warning ("called make_clauses "))*) - (*val _ = tptp_inputs clauses prob_file*) - val thmstring = Meson.concat_with_and (map string_of_thm thms) - - val goalstr = Sign.string_of_term sign sg_term - val goalproofstring = proofstring goalstr - val no_returns =List.filter not_newline ( goalproofstring) - val goalstring = implode no_returns - - val thmproofstring = proofstring ( thmstring) - val no_returns =List.filter not_newline ( thmproofstring) - val thmstr = implode no_returns - - val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n) - val axfile = (File.sysify_path axiom_file) - val hypsfile = (File.sysify_path hyps_file) - val clasimpfile = (File.sysify_path clasimp_file) - val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile"))) - val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring); - val _ = TextIO.flushOut outfile; - val _ = TextIO.closeOut outfile - val spass_home = getenv "SPASS_HOME" - in - (* without paramodulation *) - (warning ("goalstring in call_res_tac is: "^goalstring)); - (warning ("prob file in cal_res_tac is: "^probfile)); - (* Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,(*spass_home*), - "-DocProof", - clasimpfile, axfile, hypsfile, probfile)]);*) - - Watcher.callResProvers(childout, - [("spass",thmstr,goalstring(*,spass_home*),"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/spassshell", - "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", - clasimpfile, axfile, hypsfile, probfile)]); - - (* with paramodulation *) - (*Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,spass_home, - "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", - prob_path)]); *) - (* Watcher.callResProvers(childout, - [("spass",thmstr,goalstring,spass_home, - "-DocProof", prob_path)]);*) - dummy_tac - end +fun call_resolve_tac sign thms sg_term (childin, childout,pid) n = + let val thmstring = Meson.concat_with_and (map string_of_thm thms) + val thm_no = length thms + val _ = warning ("number of thms is : "^(string_of_int thm_no)) + val _ = warning ("thmstring in call_res is: "^thmstring) + + val goalstr = Sign.string_of_term sign sg_term + val goalproofstring = proofstring goalstr + val no_returns =List.filter not_newline ( goalproofstring) + val goalstring = implode no_returns + val _ = warning ("goalstring in call_res is: "^goalstring) + + (*val prob_file =File.tmp_path (Path.basic newprobfile); *) + (*val _ =( warning ("calling make_clauses ")) + val clauses = make_clauses thms + val _ =( warning ("called make_clauses "))*) + (*val _ = tptp_inputs clauses prob_file*) + val thmstring = Meson.concat_with_and (map string_of_thm thms) + + val goalstr = Sign.string_of_term sign sg_term + val goalproofstring = proofstring goalstr + val no_returns =List.filter not_newline ( goalproofstring) + val goalstring = implode no_returns + + val thmproofstring = proofstring ( thmstring) + val no_returns =List.filter not_newline ( thmproofstring) + val thmstr = implode no_returns + + val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n) + val axfile = (File.sysify_path axiom_file) + val hypsfile = (File.sysify_path hyps_file) + val clasimpfile = (File.sysify_path clasimp_file) + val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "hellofile"))) + val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring); + val _ = TextIO.flushOut outfile; + val _ = TextIO.closeOut outfile + in + (* without paramodulation *) + (warning ("goalstring in call_res_tac is: "^goalstring)); + (warning ("prob file in cal_res_tac is: "^probfile)); + (* Watcher.callResProvers(childout, + [("spass",thmstr,goalstring,*spass_home*, + "-DocProof", + clasimpfile, axfile, hypsfile, probfile)]);*) + Watcher.callResProvers(childout, + [("spass", thmstr, goalstring (*,spass_home*), + getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell", + "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", + clasimpfile, axfile, hypsfile, probfile)]); + + (* with paramodulation *) + (*Watcher.callResProvers(childout, + [("spass",thmstr,goalstring,spass_home, + "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", + prob_path)]); *) + (* Watcher.callResProvers(childout, + [("spass",thmstr,goalstring,spass_home, + "-DocProof", prob_path)]);*) + dummy_tac + end (**********************************************************) (* write out the current subgoal as a tptp file, probN, *)