isabelle: comparison src/HOL/Tools/ATP/watcher.ML

equal deleted inserted replaced

-:bd946fbc7c2b
+:2edb384bf61f
 TextIO.flushOut toWatcherStr)
 |   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,probfile)::args) =
 let
 val dfg_dir = File.tmp_path (Path.basic "dfg");
 (* need to check here if the directory exists and, if not, create it*)
-val  outfile = TextIO.openAppend("thmstring_in_watcher");
+val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic"thmstring_in_watcher")));
 val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
 val _ =  TextIO.closeOut outfile
 val dfg_create =if File.exists dfg_dir
 then
 ()
 val (settings, rest) =  takeUntil "*" rest []
 val settings = getSettings settings []
 val (file, rest) =  takeUntil "*" rest []
 val file = implode file
-val  outfile = TextIO.openOut("sep_comms");
+val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "sep_comms")));
 val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
 val _ =  TextIO.closeOut outfile
 in
 (prover,thmstring,goalstring, proverCmd, settings, file)
 (*  Set up a Watcher Process         *)
 (*************************************)
-fun setupWatcher (the_goal) = let
+fun setupWatcher () = let
 (** pipes for communication between parent and watcher **)
 val p1 = Posix.IO.pipe ()
 val p2 = Posix.IO.pipe ()
 	  fun closep () = (
 Posix.IO.close (#outfd p1);
 		      val oldchildout = #outfd p2
 		      val toParent = Posix.FileSys.wordToFD 0w1
 val fromParentIOD = Posix.FileSys.fdToIOD fromParent
 val fromParentStr = openInFD ("_exec_in_parent", fromParent)
 val toParentStr = openOutFD ("_exec_out_parent", toParent)
-val goalstr = string_of_thm (the_goal)
+(*val goalstr = string_of_thm (the_goal)
-val  outfile = TextIO.openOut("goal_in_watcher");
+val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));
 val _ = TextIO.output (outfile,goalstr )
-val _ =  TextIO.closeOut outfile
+val _ =  TextIO.closeOut outfile*)
 fun killChildren [] = ()
 |      killChildren  (childPid::children) = (killChild childPid; killChildren children)
 val childIncoming = pollChildInput childInput
 val parentID = Posix.ProcEnv.getppid()
 val prover = cmdProver childProc
 val thmstring = cmdThm childProc
 val goalstring = cmdGoal childProc
-val  outfile = TextIO.openOut("child_comms");
+val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));
 val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
 val _ =  TextIO.closeOut outfile
 in
 if (isSome childIncoming)
 then
 (* check here for prover label on child*)
-let val  outfile = TextIO.openOut("child_incoming");
+let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));
 val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
 val _ =  TextIO.closeOut outfile
 val childDone = (case prover of
 (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd)     ) )
 in
 (**********************************************)
 (childProc::(checkChildren (otherChildren, toParentStr)))
 end
 else
-let val  outfile = TextIO.openAppend("child_incoming");
+let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));
 val _ = TextIO.output (outfile,"No child output " )
 val _ =  TextIO.closeOut outfile
 in
 (childProc::(checkChildren (otherChildren, toParentStr)))
 end
 (**********************************************************)
 (* Start a watcher and set up signal handlers             *)
 (**********************************************************)
 fun killWatcher pid= killChild pid;
-fun createWatcher (the_goal) = let val mychild = childInfo (setupWatcher(the_goal))
+fun createWatcher () = let val mychild = childInfo (setupWatcher())
 			   val streams =snd mychild
 val childin = fst streams
 val childout = snd streams
 val childpid = fst mychild
 (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
 getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )
 (* fun spass_proofHandler (n:int) = (
 let val (reconstr, thmstring, goalstring) = getSpassInput childin
-val  outfile = TextIO.openOut("foo_signal");
+val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
 val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring))
 val _ =  TextIO.closeOut outfile
 in
 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
 (*
 fun spass_proofHandler (n:int) = (
-let  val  outfile = TextIO.openOut("foo_signal1");
+let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
 val _ = TextIO.output (outfile, ("In signal handler now\n"))
 val _ =  TextIO.closeOut outfile
 val (reconstr, thmstring, goalstring) = getSpassInput childin
-val  outfile = TextIO.openOut("foo_signal");
+val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
 val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^"  "^thmstring^goalstring))
 val _ =  TextIO.closeOut outfile
 in
 if ( (substring (reconstr, 0,1))= "[")
 (*killWatcher childpid; *) reap (childpid,childin, childout);()
 end )
 *)
 fun spass_proofHandler (n:int) = (
-let  val  outfile = TextIO.openOut("foo_signal1");
+let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
 val _ = TextIO.output (outfile, ("In signal handler now\n"))
 val _ =  TextIO.closeOut outfile
 val (reconstr, thmstring, goalstring) = getSpassInput childin
-val  outfile = TextIO.openAppend("foo_signal");
+val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
 val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
 val _ =  TextIO.closeOut outfile
 in          (* if a proof has been found and sent back as a reconstruction proof *)
 if ( (substring (reconstr, 0,1))= "[")
 goals_being_watched := ((!goals_being_watched) - 1);
 if ((!goals_being_watched) = 0)
 then
-(let val  outfile = TextIO.openOut("foo_reap_found");
+(let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
 val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
 val _ =  TextIO.closeOut outfile
 in
 reap (childpid,childin, childout); ()
 end)
 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("foo_reap_comp");
+(let val  outfile = TextIO.openOut(File.sysify_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
 reap (childpid,childin, childout); ()
 end )
 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("foo_reap_comp");
+(let val  outfile = TextIO.openOut(File.sysify_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
 reap (childpid,childin, childout); ()
 end )

changeset 15658	2edb384bf61f
parent 15652	a9d65894962e
child 15681	b667c22edb36