162 |
162 |
163 (* need to modify to send over hyps file too *) |
163 (* need to modify to send over hyps file too *) |
164 fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n"); |
164 fun callResProvers (toWatcherStr, []) = (sendOutput (toWatcherStr, "End of calls\n"); |
165 TextIO.flushOut toWatcherStr) |
165 TextIO.flushOut toWatcherStr) |
166 | callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) = |
166 | callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) = |
167 let val dfg_dir = File.tmp_path (Path.basic "dfg"); |
167 let val dfg_dir = File.tmp_path (Path.basic "dfg"); |
168 (*** need to check here if the directory exists and, if not, create it***) |
168 (*** need to check here if the directory exists and, if not, create it***) |
169 val outfile = TextIO.openAppend(File.sysify_path |
169 val outfile = TextIO.openAppend(File.sysify_path |
170 (File.tmp_path (Path.basic"thmstring_in_watcher"))); val _ = TextIO.output (outfile, |
170 (File.tmp_path (Path.basic"thmstring_in_watcher"))); |
171 (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")) |
171 val _ = TextIO.output (outfile, |
172 val _ = TextIO.closeOut outfile |
172 (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")) |
173 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) |
173 val _ = TextIO.closeOut outfile |
174 val probID = last(explode probfile) |
174 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***) |
175 val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) |
175 val probID = ReconOrderClauses.last(explode probfile) |
176 (*** only include problem and clasimp for the moment, not sure how to refer to ***) |
176 val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID)) |
177 (*** hyps/local axioms just now ***) |
177 (*** only include problem and clasimp for the moment, not sure how to refer to ***) |
178 val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)]) |
178 (*** hyps/local axioms just now ***) |
179 val dfg_create =if File.exists dfg_dir |
179 val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile, ">", (File.sysify_path wholefile)]) |
180 then |
180 val dfg_create =if File.exists dfg_dir |
181 ((warning("dfg dir exists"));()) |
181 then |
182 else |
182 ((warning("dfg dir exists"));()) |
183 File.mkdir dfg_dir; |
183 else |
184 |
184 File.mkdir dfg_dir; |
185 val dfg_path = File.sysify_path dfg_dir; |
185 |
186 val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path]) |
186 val dfg_path = File.sysify_path dfg_dir; |
187 (*val _ = Posix.Process.wait ()*) |
187 val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X", ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path]) |
188 (*val _ =Unix.reap exec_tptp2x*) |
188 (*val _ = Posix.Process.wait ()*) |
189 val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg" |
189 (*val _ =Unix.reap exec_tptp2x*) |
190 |
190 val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg" |
191 in |
191 |
192 goals_being_watched := (!goals_being_watched) + 1; |
192 in |
193 Posix.Process.sleep(Time.fromSeconds 1); |
193 goals_being_watched := (!goals_being_watched) + 1; |
194 (warning ("probfile is: "^probfile)); |
194 Posix.Process.sleep(Time.fromSeconds 1); |
195 (warning("dfg file is: "^newfile)); |
195 (warning ("probfile is: "^probfile)); |
196 (warning ("wholefile is: "^(File.sysify_path wholefile))); |
196 (warning("dfg file is: "^newfile)); |
197 sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n")); |
197 (warning ("wholefile is: "^(File.sysify_path wholefile))); |
198 (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*) |
198 sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n")); |
199 TextIO.flushOut toWatcherStr; |
199 (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*) |
200 Unix.reap exec_tptp2x; |
200 TextIO.flushOut toWatcherStr; |
201 |
201 Unix.reap exec_tptp2x; |
202 callResProvers (toWatcherStr,args) |
202 |
203 |
203 callResProvers (toWatcherStr,args) |
204 end |
204 |
|
205 end |
205 (* |
206 (* |
206 fun callResProversStr (toWatcherStr, []) = "End of calls\n" |
207 fun callResProversStr (toWatcherStr, []) = "End of calls\n" |
207 |
208 |
208 | callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) = |
209 | callResProversStr (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile, probfile)::args) = |
209 ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n") |
210 ((prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^clasimpfile^"*"^axfile^"*"^hypsfile^"*"^probfile^"\n") |
325 (* Set up a Watcher Process *) |
326 (* Set up a Watcher Process *) |
326 (*************************************) |
327 (*************************************) |
327 |
328 |
328 |
329 |
329 |
330 |
330 fun setupWatcher (thm,clause_arr, num_of_clauses) = let |
331 fun setupWatcher (thm,clause_arr, num_of_clauses) = |
331 (** pipes for communication between parent and watcher **) |
332 let |
332 val p1 = Posix.IO.pipe () |
333 (** pipes for communication between parent and watcher **) |
333 val p2 = Posix.IO.pipe () |
334 val p1 = Posix.IO.pipe () |
334 fun closep () = ( |
335 val p2 = Posix.IO.pipe () |
335 Posix.IO.close (#outfd p1); |
336 fun closep () = ( |
336 Posix.IO.close (#infd p1); |
337 Posix.IO.close (#outfd p1); |
337 Posix.IO.close (#outfd p2); |
338 Posix.IO.close (#infd p1); |
338 Posix.IO.close (#infd p2) |
339 Posix.IO.close (#outfd p2); |
339 ) |
340 Posix.IO.close (#infd p2) |
340 (***********************************************************) |
341 ) |
341 (****** fork a watcher process and get it set up and going *) |
342 (***********************************************************) |
342 (***********************************************************) |
343 (****** fork a watcher process and get it set up and going *) |
343 fun startWatcher (procList) = |
344 (***********************************************************) |
344 (case Posix.Process.fork() (***************************************) |
345 fun startWatcher (procList) = |
345 of SOME pid => pid (* parent - i.e. main Isabelle process *) |
346 (case Posix.Process.fork() (***************************************) |
346 (***************************************) |
347 of SOME pid => pid (* parent - i.e. main Isabelle process *) |
347 |
348 (***************************************) |
348 (*************************) |
349 |
349 | NONE => let (* child - i.e. watcher *) |
350 (*************************) |
350 val oldchildin = #infd p1 (*************************) |
351 | NONE => let (* child - i.e. watcher *) |
351 val fromParent = Posix.FileSys.wordToFD 0w0 |
352 val oldchildin = #infd p1 (*************************) |
352 val oldchildout = #outfd p2 |
353 val fromParent = Posix.FileSys.wordToFD 0w0 |
353 val toParent = Posix.FileSys.wordToFD 0w1 |
354 val oldchildout = #outfd p2 |
354 val fromParentIOD = Posix.FileSys.fdToIOD fromParent |
355 val toParent = Posix.FileSys.wordToFD 0w1 |
355 val fromParentStr = openInFD ("_exec_in_parent", fromParent) |
356 val fromParentIOD = Posix.FileSys.fdToIOD fromParent |
356 val toParentStr = openOutFD ("_exec_out_parent", toParent) |
357 val fromParentStr = openInFD ("_exec_in_parent", fromParent) |
357 val sign = sign_of_thm thm |
358 val toParentStr = openOutFD ("_exec_out_parent", toParent) |
358 val prems = prems_of thm |
359 val sign = sign_of_thm thm |
359 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) |
360 val prems = prems_of thm |
360 val _ = (warning ("subgoals forked to startWatcher: "^prems_string)); |
361 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) |
361 (* tracing *) |
362 val _ = (warning ("subgoals forked to startWatcher: "^prems_string)); |
362 (*val tenth_ax = fst( Array.sub(clause_arr, 1)) |
363 (* tracing *) |
363 val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab) |
364 (*val tenth_ax = fst( Array.sub(clause_arr, 1)) |
364 val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) |
365 val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab) |
365 val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax)) |
366 val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) |
366 val _ = (warning ("tenth axiom in table in watcher is: "^clause_str)) |
367 val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax)) |
367 val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) ) |
368 val _ = (warning ("tenth axiom in table in watcher is: "^clause_str)) |
368 *) |
369 val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) ) |
369 (*val goalstr = string_of_thm (the_goal) |
370 *) |
370 val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher"))); |
371 (*val goalstr = string_of_thm (the_goal) |
371 val _ = TextIO.output (outfile,goalstr ) |
372 val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher"))); |
372 val _ = TextIO.closeOut outfile*) |
373 val _ = TextIO.output (outfile,goalstr ) |
373 fun killChildren [] = () |
374 val _ = TextIO.closeOut outfile*) |
374 | killChildren (child_handle::children) = (killChild child_handle; killChildren children) |
375 fun killChildren [] = () |
375 |
376 | killChildren (child_handle::children) = (killChild child_handle; killChildren children) |
376 |
377 |
377 |
378 |
378 (*************************************************************) |
379 |
379 (* take an instream and poll its underlying reader for input *) |
380 (*************************************************************) |
380 (*************************************************************) |
381 (* take an instream and poll its underlying reader for input *) |
381 |
382 (*************************************************************) |
382 fun pollParentInput () = |
383 |
383 |
384 fun pollParentInput () = |
384 let val pd = OS.IO.pollDesc (fromParentIOD) |
385 |
385 in |
386 let val pd = OS.IO.pollDesc (fromParentIOD) |
386 if (isSome pd ) then |
387 in |
387 let val pd' = OS.IO.pollIn (valOf pd) |
388 if (isSome pd ) then |
388 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) |
389 let val pd' = OS.IO.pollIn (valOf pd) |
389 in |
390 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) |
390 if null pdl |
391 in |
391 then |
392 if null pdl |
392 NONE |
393 then |
393 else if (OS.IO.isIn (hd pdl)) |
394 NONE |
394 then |
395 else if (OS.IO.isIn (hd pdl)) |
395 (SOME ( getCmds (toParentStr, fromParentStr, []))) |
396 then |
396 else |
397 (SOME ( getCmds (toParentStr, fromParentStr, []))) |
397 NONE |
398 else |
398 end |
399 NONE |
399 else |
400 end |
400 NONE |
401 else |
401 end |
402 NONE |
402 |
403 end |
403 |
404 |
404 |
405 |
405 fun pollChildInput (fromStr) = |
406 |
406 let val iod = getInIoDesc fromStr |
407 fun pollChildInput (fromStr) = |
407 in |
408 let val iod = getInIoDesc fromStr |
408 if isSome iod |
409 in |
409 then |
410 if isSome iod |
410 let val pd = OS.IO.pollDesc (valOf iod) |
411 then |
411 in |
412 let val pd = OS.IO.pollDesc (valOf iod) |
412 if (isSome pd ) then |
413 in |
413 let val pd' = OS.IO.pollIn (valOf pd) |
414 if (isSome pd ) then |
414 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) |
415 let val pd' = OS.IO.pollIn (valOf pd) |
415 in |
416 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) |
416 if null pdl |
417 in |
417 then |
418 if null pdl |
418 NONE |
419 then |
419 else if (OS.IO.isIn (hd pdl)) |
420 NONE |
420 then |
421 else if (OS.IO.isIn (hd pdl)) |
421 SOME (getCmd (TextIO.inputLine fromStr)) |
422 then |
422 else |
423 SOME (getCmd (TextIO.inputLine fromStr)) |
423 NONE |
424 else |
424 end |
425 NONE |
425 else |
426 end |
426 NONE |
427 else |
427 end |
428 NONE |
428 else |
429 end |
429 NONE |
430 else |
430 end |
431 NONE |
431 |
432 end |
432 |
433 |
433 (****************************************************************************) |
434 |
434 (* Check all vampire processes currently running for output *) |
435 (****************************************************************************) |
435 (****************************************************************************) |
436 (* Check all vampire processes currently running for output *) |
436 (*********************************) |
437 (****************************************************************************) |
437 fun checkChildren ([], toParentStr) = [] (*** no children to check ********) |
438 (*********************************) |
438 (*********************************) |
439 fun checkChildren ([], toParentStr) = [] (*** no children to check ********) |
439 | checkChildren ((childProc::otherChildren), toParentStr) = |
440 (*********************************) |
440 let val (childInput,childOutput) = cmdstreamsOf childProc |
441 | checkChildren ((childProc::otherChildren), toParentStr) = |
441 val child_handle= cmdchildHandle childProc |
442 let val (childInput,childOutput) = cmdstreamsOf childProc |
442 (* childCmd is the .dfg file that the problem is in *) |
443 val child_handle= cmdchildHandle childProc |
443 val childCmd = fst(snd (cmdchildInfo childProc)) |
444 (* childCmd is the .dfg file that the problem is in *) |
444 (* now get the number of the subgoal from the filename *) |
445 val childCmd = fst(snd (cmdchildInfo childProc)) |
445 val sg_num = int_of_string(get_nth 5 (rev(explode childCmd))) |
446 (* now get the number of the subgoal from the filename *) |
446 val childIncoming = pollChildInput childInput |
447 val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd))) |
447 val parentID = Posix.ProcEnv.getppid() |
448 val childIncoming = pollChildInput childInput |
448 val prover = cmdProver childProc |
449 val parentID = Posix.ProcEnv.getppid() |
449 val thmstring = cmdThm childProc |
450 val prover = cmdProver childProc |
450 val sign = sign_of_thm thm |
451 val thmstring = cmdThm childProc |
451 val prems = prems_of thm |
452 val sign = sign_of_thm thm |
452 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) |
453 val prems = prems_of thm |
453 val _ = (warning ("subgoals forked to checkChildren: "^prems_string)); |
454 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) |
454 val goalstring = cmdGoal childProc |
455 val _ = (warning ("subgoals forked to checkChildren: "^prems_string)); |
455 |
456 val goalstring = cmdGoal childProc |
456 val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms"))); |
457 |
457 val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) ) |
458 val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms"))); |
458 val _ = TextIO.closeOut outfile |
459 val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) ) |
459 in |
460 val _ = TextIO.closeOut outfile |
460 if (isSome childIncoming) |
461 in |
461 then |
462 if (isSome childIncoming) |
462 (* check here for prover label on child*) |
463 then |
463 |
464 (* check here for prover label on child*) |
464 let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); |
465 |
465 val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) ) |
466 let val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); |
466 val _ = TextIO.closeOut outfile |
467 val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) ) |
467 val childDone = (case prover of |
468 val _ = TextIO.closeOut outfile |
468 (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) |
469 val childDone = (case prover of |
469 in |
470 (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd) |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) |
470 if childDone (**********************************************) |
471 in |
471 then (* child has found a proof and transferred it *) |
472 if childDone (**********************************************) |
472 (**********************************************) |
473 then (* child has found a proof and transferred it *) |
473 |
474 (**********************************************) |
474 (**********************************************) |
475 |
475 (* Remove this child and go on to check others*) |
476 (**********************************************) |
476 (**********************************************) |
477 (* Remove this child and go on to check others*) |
477 ( Unix.reap child_handle; |
478 (**********************************************) |
478 checkChildren(otherChildren, toParentStr)) |
479 ( Unix.reap child_handle; |
479 else |
480 checkChildren(otherChildren, toParentStr)) |
480 (**********************************************) |
481 else |
481 (* Keep this child and go on to check others *) |
482 (**********************************************) |
482 (**********************************************) |
483 (* Keep this child and go on to check others *) |
483 |
484 (**********************************************) |
484 (childProc::(checkChildren (otherChildren, toParentStr))) |
485 |
485 end |
486 (childProc::(checkChildren (otherChildren, toParentStr))) |
486 else |
487 end |
487 let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); |
488 else |
488 val _ = TextIO.output (outfile,"No child output " ) |
489 let val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming"))); |
489 val _ = TextIO.closeOut outfile |
490 val _ = TextIO.output (outfile,"No child output " ) |
490 in |
491 val _ = TextIO.closeOut outfile |
491 (childProc::(checkChildren (otherChildren, toParentStr))) |
492 in |
492 end |
493 (childProc::(checkChildren (otherChildren, toParentStr))) |
493 end |
494 end |
494 |
495 end |
495 |
496 |
496 (********************************************************************) |
497 |
497 (* call resolution processes *) |
498 (********************************************************************) |
498 (* settings should be a list of strings *) |
499 (* call resolution processes *) |
499 (* e.g. ["-t 300", "-m 100000"] *) |
500 (* settings should be a list of strings *) |
500 (* takes list of (string, string, string list, string)list proclist *) |
501 (* e.g. ["-t 300", "-m 100000"] *) |
501 (********************************************************************) |
502 (* takes list of (string, string, string list, string)list proclist *) |
502 |
503 (********************************************************************) |
503 |
504 |
504 (*** add subgoal id num to this *) |
505 |
505 fun execCmds [] procList = procList |
506 (*** add subgoal id num to this *) |
506 | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = |
507 fun execCmds [] procList = procList |
507 if (prover = "spass") |
508 | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = |
508 then |
509 if (prover = "spass") |
509 let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) |
510 then |
510 val (instr, outstr)=Unix.streamsOf childhandle |
511 let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) |
511 val newProcList = (((CMDPROC{ |
512 val (instr, outstr)=Unix.streamsOf childhandle |
512 prover = prover, |
513 val newProcList = (((CMDPROC{ |
513 cmd = file, |
514 prover = prover, |
514 thmstring = thmstring, |
515 cmd = file, |
515 goalstring = goalstring, |
516 thmstring = thmstring, |
516 proc_handle = childhandle, |
517 goalstring = goalstring, |
517 instr = instr, |
518 proc_handle = childhandle, |
518 outstr = outstr })::procList)) |
519 instr = instr, |
519 val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child"))); |
520 outstr = outstr })::procList)) |
520 val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file ) |
521 val outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child"))); |
521 val _ = TextIO.closeOut outfile |
522 val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file ) |
522 in |
523 val _ = TextIO.closeOut outfile |
523 execCmds cmds newProcList |
524 in |
524 end |
525 execCmds cmds newProcList |
525 else |
526 end |
526 let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) |
527 else |
527 val (instr, outstr)=Unix.streamsOf childhandle |
528 let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) |
528 val newProcList = (((CMDPROC{ |
529 val (instr, outstr)=Unix.streamsOf childhandle |
529 prover = prover, |
530 val newProcList = (((CMDPROC{ |
530 cmd = file, |
531 prover = prover, |
531 thmstring = thmstring, |
532 cmd = file, |
532 goalstring = goalstring, |
533 thmstring = thmstring, |
533 proc_handle = childhandle, |
534 goalstring = goalstring, |
534 instr = instr, |
535 proc_handle = childhandle, |
535 outstr = outstr })::procList)) |
536 instr = instr, |
536 in |
537 outstr = outstr })::procList)) |
537 execCmds cmds newProcList |
538 in |
538 end |
539 execCmds cmds newProcList |
539 |
540 end |
540 |
541 |
541 |
542 |
542 (****************************************) |
543 |
543 (* call resolution processes remotely *) |
544 (****************************************) |
544 (* settings should be a list of strings *) |
545 (* call resolution processes remotely *) |
545 (* e.g. ["-t 300", "-m 100000"] *) |
546 (* settings should be a list of strings *) |
546 (****************************************) |
547 (* e.g. ["-t 300", "-m 100000"] *) |
547 |
548 (****************************************) |
548 (* fun execRemoteCmds [] procList = procList |
549 |
549 | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList = |
550 (* fun execRemoteCmds [] procList = procList |
550 let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList) |
551 | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList = |
551 in |
552 let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList) |
552 execRemoteCmds cmds newProcList |
553 in |
553 end |
554 execRemoteCmds cmds newProcList |
|
555 end |
554 *) |
556 *) |
555 |
557 |
556 fun printList (outStr, []) = () |
558 fun printList (outStr, []) = () |
557 | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs)) |
559 | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs)) |
558 |
560 |
559 |
561 |
560 (**********************************************) |
562 (**********************************************) |
561 (* Watcher Loop *) |
563 (* Watcher Loop *) |
562 (**********************************************) |
564 (**********************************************) |
563 |
565 |
564 |
566 |
565 |
567 |
566 |
568 |
567 fun keepWatching (toParentStr, fromParentStr,procList) = |
569 fun keepWatching (toParentStr, fromParentStr,procList) = |
568 let fun loop (procList) = |
570 let fun loop (procList) = |
569 ( |
571 ( |
570 let val cmdsFromIsa = pollParentInput () |
572 let val cmdsFromIsa = pollParentInput () |
571 fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n"); |
573 fun killchildHandler (n:int) = (TextIO.output(toParentStr, "Killing child proof processes!\n"); |
572 TextIO.flushOut toParentStr; |
574 TextIO.flushOut toParentStr; |
573 killChildren (map (cmdchildHandle) procList); |
575 killChildren (map (cmdchildHandle) procList); |
574 ()) |
576 ()) |
575 |
577 |
576 in |
578 in |
577 (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) |
579 (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) |
578 (**********************************) |
580 (**********************************) |
579 if (isSome cmdsFromIsa) then (* deal with input from Isabelle *) |
581 if (isSome cmdsFromIsa) then (* deal with input from Isabelle *) |
580 ( (**********************************) |
582 ( (**********************************) |
581 if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" ) |
583 if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" ) |
582 then |
584 then |
583 ( |
585 ( |
584 let val child_handles = map cmdchildHandle procList |
586 let val child_handles = map cmdchildHandle procList |
585 in |
587 in |
586 killChildren child_handles; |
588 killChildren child_handles; |
587 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([]) |
589 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) loop ([]) |
588 end |
590 end |
589 |
591 |
590 ) |
592 ) |
591 else |
593 else |
592 ( |
594 ( |
593 if ((length procList)<10) (********************) |
595 if ((length procList)<10) (********************) |
594 then (* Execute locally *) |
596 then (* Execute locally *) |
595 ( (********************) |
597 ( (********************) |
596 let |
598 let |
597 val newProcList = execCmds (valOf cmdsFromIsa) procList |
599 val newProcList = execCmds (valOf cmdsFromIsa) procList |
598 val parentID = Posix.ProcEnv.getppid() |
600 val parentID = Posix.ProcEnv.getppid() |
599 val newProcList' =checkChildren (newProcList, toParentStr) |
601 val newProcList' =checkChildren (newProcList, toParentStr) |
600 in |
602 in |
601 (*Posix.Process.sleep (Time.fromSeconds 1);*) |
603 (*Posix.Process.sleep (Time.fromSeconds 1);*) |
602 loop (newProcList') |
604 loop (newProcList') |
603 end |
605 end |
604 ) |
606 ) |
605 else (*********************************) |
607 else (*********************************) |
606 (* Execute remotely *) |
608 (* Execute remotely *) |
607 (* (actually not remote for now )*) |
609 (* (actually not remote for now )*) |
608 ( (*********************************) |
610 ( (*********************************) |
609 let |
611 let |
610 val newProcList = execCmds (valOf cmdsFromIsa) procList |
612 val newProcList = execCmds (valOf cmdsFromIsa) procList |
611 val parentID = Posix.ProcEnv.getppid() |
613 val parentID = Posix.ProcEnv.getppid() |
612 val newProcList' =checkChildren (newProcList, toParentStr) |
614 val newProcList' =checkChildren (newProcList, toParentStr) |
613 in |
615 in |
614 (*Posix.Process.sleep (Time.fromSeconds 1);*) |
616 (*Posix.Process.sleep (Time.fromSeconds 1);*) |
615 loop (newProcList') |
617 loop (newProcList') |
616 end |
618 end |
617 ) |
619 ) |
618 |
620 |
619 |
621 |
620 |
622 |
621 ) |
623 ) |
622 ) (******************************) |
624 ) (******************************) |
623 else (* No new input from Isabelle *) |
625 else (* No new input from Isabelle *) |
624 (******************************) |
626 (******************************) |
625 ( let val newProcList = checkChildren ((procList), toParentStr) |
627 ( let val newProcList = checkChildren ((procList), toParentStr) |
626 in |
628 in |
627 Posix.Process.sleep (Time.fromSeconds 1); |
629 Posix.Process.sleep (Time.fromSeconds 1); |
628 loop (newProcList) |
630 loop (newProcList) |
629 end |
631 end |
630 |
632 |
631 ) |
633 ) |
632 end) |
634 end) |
633 in |
635 in |
634 loop (procList) |
636 loop (procList) |
635 end |
637 end |
636 |
638 |
637 |
639 |
638 in |
640 in |
639 (***************************) |
641 (***************************) |
640 (*** Sort out pipes ********) |
642 (*** Sort out pipes ********) |
641 (***************************) |
643 (***************************) |
642 |
644 |
643 Posix.IO.close (#outfd p1); |
645 Posix.IO.close (#outfd p1); |
644 Posix.IO.close (#infd p2); |
646 Posix.IO.close (#infd p2); |
645 Posix.IO.dup2{old = oldchildin, new = fromParent}; |
647 Posix.IO.dup2{old = oldchildin, new = fromParent}; |
646 Posix.IO.close oldchildin; |
648 Posix.IO.close oldchildin; |
647 Posix.IO.dup2{old = oldchildout, new = toParent}; |
649 Posix.IO.dup2{old = oldchildout, new = toParent}; |
648 Posix.IO.close oldchildout; |
650 Posix.IO.close oldchildout; |
649 |
651 |
650 (***************************) |
652 (***************************) |
651 (* start the watcher loop *) |
653 (* start the watcher loop *) |
652 (***************************) |
654 (***************************) |
653 keepWatching (toParentStr, fromParentStr, procList); |
655 keepWatching (toParentStr, fromParentStr, procList); |
654 |
656 |
655 |
657 |
656 (****************************************************************************) |
658 (****************************************************************************) |
657 (* fake return value - actually want the watcher to loop until killed *) |
659 (* fake return value - actually want the watcher to loop until killed *) |
658 (****************************************************************************) |
660 (****************************************************************************) |
659 Posix.Process.wordToPid 0w0 |
661 Posix.Process.wordToPid 0w0 |
660 |
662 |
661 end); |
663 end); |
662 (* end case *) |
664 (* end case *) |
663 |
665 |
664 |
666 |
665 val _ = TextIO.flushOut TextIO.stdOut |
667 val _ = TextIO.flushOut TextIO.stdOut |
666 |
668 |
667 (*******************************) |
669 (*******************************) |
668 (*** set watcher going ********) |
670 (*** set watcher going ********) |
669 (*******************************) |
671 (*******************************) |
670 |
672 |
671 val procList = [] |
673 val procList = [] |
672 val pid = startWatcher (procList) |
674 val pid = startWatcher (procList) |
673 (**************************************************) |
675 (**************************************************) |
674 (* communication streams to watcher *) |
676 (* communication streams to watcher *) |
675 (**************************************************) |
677 (**************************************************) |
676 |
678 |
677 val instr = openInFD ("_exec_in", #infd p2) |
679 val instr = openInFD ("_exec_in", #infd p2) |
678 val outstr = openOutFD ("_exec_out", #outfd p1) |
680 val outstr = openOutFD ("_exec_out", #outfd p1) |
679 |
681 |
680 in |
682 in |
681 (*******************************) |
683 (*******************************) |
682 (* close the child-side fds *) |
684 (* close the child-side fds *) |
683 (*******************************) |
685 (*******************************) |
684 Posix.IO.close (#outfd p2); |
686 Posix.IO.close (#outfd p2); |
685 Posix.IO.close (#infd p1); |
687 Posix.IO.close (#infd p1); |
686 (* set the fds close on exec *) |
688 (* set the fds close on exec *) |
687 Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
689 Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
688 Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
690 Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]); |
689 |
691 |
690 (*******************************) |
692 (*******************************) |
691 (* return value *) |
693 (* return value *) |
692 (*******************************) |
694 (*******************************) |
693 PROC{pid = pid, |
695 PROC{pid = pid, |
694 instr = instr, |
696 instr = instr, |
695 outstr = outstr |
697 outstr = outstr |
696 } |
698 } |
697 end; |
699 end; |
698 |
700 |
699 |
701 |
700 |
702 |
701 (**********************************************************) |
703 (**********************************************************) |
702 (* Start a watcher and set up signal handlers *) |
704 (* Start a watcher and set up signal handlers *) |