376 ) |
368 ) |
377 (***********************************************************) |
369 (***********************************************************) |
378 (****** fork a watcher process and get it set up and going *) |
370 (****** fork a watcher process and get it set up and going *) |
379 (***********************************************************) |
371 (***********************************************************) |
380 fun startWatcher (procList) = |
372 fun startWatcher (procList) = |
381 (case Posix.Process.fork() (***************************************) |
373 (case Posix.Process.fork() (***************************************) |
382 of SOME pid => pid (* parent - i.e. main Isabelle process *) |
374 of SOME pid => pid (* parent - i.e. main Isabelle process *) |
383 (***************************************) |
375 (***************************************) |
384 |
376 |
385 (*************************) |
377 (*************************) |
386 | NONE => let (* child - i.e. watcher *) |
378 | NONE => let (* child - i.e. watcher *) |
387 val oldchildin = #infd p1 (*************************) |
379 val oldchildin = #infd p1 (*************************) |
388 val fromParent = Posix.FileSys.wordToFD 0w0 |
380 val fromParent = Posix.FileSys.wordToFD 0w0 |
389 val oldchildout = #outfd p2 |
381 val oldchildout = #outfd p2 |
390 val toParent = Posix.FileSys.wordToFD 0w1 |
382 val toParent = Posix.FileSys.wordToFD 0w1 |
391 val fromParentIOD = Posix.FileSys.fdToIOD fromParent |
383 val fromParentIOD = Posix.FileSys.fdToIOD fromParent |
392 val fromParentStr = openInFD ("_exec_in_parent", fromParent) |
384 val fromParentStr = openInFD ("_exec_in_parent", fromParent) |
393 val toParentStr = openOutFD ("_exec_out_parent", toParent) |
385 val toParentStr = openOutFD ("_exec_out_parent", toParent) |
394 val sign = sign_of_thm thm |
386 val sign = sign_of_thm thm |
395 val prems = prems_of thm |
387 val prems = prems_of thm |
396 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) |
388 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) |
397 val _ = (warning ("subgoals forked to startWatcher: "^prems_string)); |
389 val _ = (warning ("subgoals forked to startWatcher: "^prems_string)); |
398 (* tracing *) |
390 (* tracing *) |
399 (*val tenth_ax = fst( Array.sub(clause_arr, 1)) |
391 (*val tenth_ax = fst( Array.sub(clause_arr, 1)) |
400 val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab) |
392 val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab) |
401 val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) |
393 val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) |
402 val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax)) |
394 val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax)) |
403 val _ = (warning ("tenth axiom in table in watcher is: "^clause_str)) |
395 val _ = (warning ("tenth axiom in table in watcher is: "^clause_str)) |
404 val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) ) |
396 val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) ) |
405 *) |
397 *) |
406 (*val goalstr = string_of_thm (the_goal) |
398 (*val goalstr = string_of_thm (the_goal) |
407 val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher"))); |
399 val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "goal_in_watcher"))); |
408 val _ = TextIO.output (outfile,goalstr ) |
400 val _ = TextIO.output (outfile,goalstr ) |
409 val _ = TextIO.closeOut outfile*) |
401 val _ = TextIO.closeOut outfile*) |
410 fun killChildren [] = () |
402 fun killChildren [] = () |
411 | killChildren (child_handle::children) = (killChild child_handle; killChildren children) |
403 | killChildren (child_handle::children) = (killChild child_handle; killChildren children) |
412 |
404 |
413 (*************************************************************) |
405 (*************************************************************) |
414 (* take an instream and poll its underlying reader for input *) |
406 (* take an instream and poll its underlying reader for input *) |
415 (*************************************************************) |
407 (*************************************************************) |
416 |
408 |
417 fun pollParentInput () = |
409 fun pollParentInput () = |
418 let val pd = OS.IO.pollDesc (fromParentIOD) |
410 let val pd = OS.IO.pollDesc (fromParentIOD) |
419 in |
411 in |
420 if (isSome pd ) then |
412 if (isSome pd ) then |
421 let val pd' = OS.IO.pollIn (valOf pd) |
413 let val pd' = OS.IO.pollIn (valOf pd) |
422 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) |
414 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) |
423 val _ = File.append (File.tmp_path (Path.basic "parent_poll")) |
415 val _ = File.append (File.tmp_path (Path.basic "parent_poll")) |
424 ("In parent_poll\n") |
416 ("In parent_poll\n") |
|
417 in |
|
418 if null pdl |
|
419 then |
|
420 NONE |
|
421 else if (OS.IO.isIn (hd pdl)) |
|
422 then SOME (getCmds (toParentStr, fromParentStr, [])) |
|
423 else NONE |
|
424 end |
|
425 else NONE |
|
426 end |
|
427 |
|
428 fun pollChildInput (fromStr) = |
|
429 let val _ = File.append (File.tmp_path (Path.basic "child_poll")) |
|
430 ("In child_poll\n") |
|
431 val iod = getInIoDesc fromStr |
|
432 in |
|
433 if isSome iod |
|
434 then |
|
435 let val pd = OS.IO.pollDesc (valOf iod) |
|
436 in |
|
437 if (isSome pd ) then |
|
438 let val pd' = OS.IO.pollIn (valOf pd) |
|
439 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) |
|
440 in |
|
441 if null pdl |
|
442 then |
|
443 ( File.append (File.tmp_path (Path.basic "child_poll_res")) |
|
444 ("Null pdl \n");NONE) |
|
445 else if (OS.IO.isIn (hd pdl)) |
|
446 then |
|
447 (let val inval = (TextIO.inputLine fromStr) |
|
448 val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n") |
|
449 in |
|
450 SOME inval |
|
451 end) |
|
452 else |
|
453 ( File.append (File.tmp_path (Path.basic "child_poll_res")) |
|
454 ("Null pdl \n");NONE) |
|
455 end |
|
456 else NONE |
|
457 end |
|
458 else NONE |
|
459 end |
|
460 |
|
461 |
|
462 (****************************************************************************) |
|
463 (* Check all vampire processes currently running for output *) |
|
464 (****************************************************************************) |
|
465 (*********************************) |
|
466 fun checkChildren ([], toParentStr) = [] (*** no children to check ********) |
|
467 (*********************************) |
|
468 | checkChildren ((childProc::otherChildren), toParentStr) = |
|
469 let val _ = File.append (File.tmp_path (Path.basic "child_check")) |
|
470 ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n") |
|
471 val (childInput,childOutput) = cmdstreamsOf childProc |
|
472 val child_handle= cmdchildHandle childProc |
|
473 (* childCmd is the .dfg file that the problem is in *) |
|
474 val childCmd = fst(snd (cmdchildInfo childProc)) |
|
475 val _ = File.append (File.tmp_path (Path.basic "child_command")) |
|
476 (childCmd^"\n") |
|
477 (* now get the number of the subgoal from the filename *) |
|
478 val sg_num = (*if (!SpassComm.spass ) |
|
479 then |
|
480 int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd))) |
|
481 else*) |
|
482 int_of_string(hd (rev(explode childCmd))) |
|
483 |
|
484 val childIncoming = pollChildInput childInput |
|
485 val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) |
|
486 ("finished polling child \n") |
|
487 val parentID = Posix.ProcEnv.getppid() |
|
488 val prover = cmdProver childProc |
|
489 val thmstring = cmdThm childProc |
|
490 val sign = sign_of_thm thm |
|
491 val prems = prems_of thm |
|
492 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) |
|
493 val _ = warning("subgoals forked to checkChildren: "^prems_string) |
|
494 val goalstring = cmdGoal childProc |
|
495 val _ = File.append (File.tmp_path (Path.basic "child_comms")) |
|
496 (prover^thmstring^goalstring^childCmd^"\n") |
|
497 in |
|
498 if (isSome childIncoming) |
|
499 then |
|
500 (* check here for prover label on child*) |
|
501 let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) |
|
502 ("subgoals forked to checkChildren:"^ |
|
503 prems_string^prover^thmstring^goalstring^childCmd) |
|
504 val childDone = (case prover of |
|
505 "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) |
|
506 |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) |
|
507 in |
|
508 if childDone (**********************************************) |
|
509 then (* child has found a proof and transferred it *) |
|
510 (* Remove this child and go on to check others*) |
|
511 (**********************************************) |
|
512 (Unix.reap child_handle; |
|
513 checkChildren(otherChildren, toParentStr)) |
|
514 else |
|
515 (**********************************************) |
|
516 (* Keep this child and go on to check others *) |
|
517 (**********************************************) |
|
518 (childProc::(checkChildren (otherChildren, toParentStr))) |
|
519 end |
|
520 else |
|
521 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output "; |
|
522 childProc::(checkChildren (otherChildren, toParentStr))) |
|
523 end |
|
524 |
|
525 |
|
526 (********************************************************************) |
|
527 (* call resolution processes *) |
|
528 (* settings should be a list of strings *) |
|
529 (* e.g. ["-t 300", "-m 100000"] (TextIO.input instr)^ *) |
|
530 (* takes list of (string, string, string list, string)list proclist *) |
|
531 (********************************************************************) |
|
532 |
|
533 |
|
534 (*** add subgoal id num to this *) |
|
535 fun execCmds [] procList = procList |
|
536 | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child")) ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) |
|
537 in |
|
538 if (prover = "spass") |
|
539 then |
|
540 let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = |
|
541 (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) |
|
542 val (instr, outstr) = Unix.streamsOf childhandle |
|
543 val newProcList = (((CMDPROC{ |
|
544 prover = prover, |
|
545 cmd = file, |
|
546 thmstring = thmstring, |
|
547 goalstring = goalstring, |
|
548 proc_handle = childhandle, |
|
549 instr = instr, |
|
550 outstr = outstr })::procList)) |
|
551 val _ = File.append (File.tmp_path (Path.basic "exec_child")) |
|
552 ("\nexecuting command for goal:\n"^ |
|
553 goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) |
|
554 in |
|
555 Posix.Process.sleep (Time.fromSeconds 1); |
|
556 execCmds cmds newProcList |
|
557 end |
|
558 else |
|
559 let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = |
|
560 (Unix.execute(proverCmd, (settings@[file]))) |
|
561 val (instr, outstr) = Unix.streamsOf childhandle |
|
562 |
|
563 val newProcList = (CMDPROC{ |
|
564 prover = prover, |
|
565 cmd = file, |
|
566 thmstring = thmstring, |
|
567 goalstring = goalstring, |
|
568 proc_handle = childhandle, |
|
569 instr = instr, |
|
570 outstr = outstr }) :: procList |
|
571 |
|
572 val _ = File.append (File.tmp_path (Path.basic "exec_child")) |
|
573 ("executing command for goal:\n"^ |
|
574 goalstring^proverCmd^(concat settings)^file^ |
|
575 " at "^(Date.toString(Date.fromTimeLocal(Time.now())))) |
|
576 in |
|
577 Posix.Process.sleep (Time.fromSeconds 1); |
|
578 execCmds cmds newProcList |
|
579 end |
|
580 end |
|
581 |
|
582 |
|
583 (****************************************) |
|
584 (* call resolution processes remotely *) |
|
585 (* settings should be a list of strings *) |
|
586 (* e.g. ["-t 300", "-m 100000"] *) |
|
587 (****************************************) |
|
588 |
|
589 (* fun execRemoteCmds [] procList = procList |
|
590 | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList = |
|
591 let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList) |
|
592 in |
|
593 execRemoteCmds cmds newProcList |
|
594 end |
|
595 *) |
|
596 |
|
597 fun printList (outStr, []) = () |
|
598 | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs)) |
|
599 |
|
600 |
|
601 (**********************************************) |
|
602 (* Watcher Loop *) |
|
603 (**********************************************) |
|
604 |
|
605 fun keepWatching (toParentStr, fromParentStr,procList) = |
|
606 let fun loop (procList) = |
|
607 let val _ = Posix.Process.sleep (Time.fromMilliseconds 200) |
|
608 val cmdsFromIsa = pollParentInput () |
|
609 fun killchildHandler (n:int) = |
|
610 (TextIO.output(toParentStr, "Killing child proof processes!\n"); |
|
611 TextIO.flushOut toParentStr; |
|
612 killChildren (map (cmdchildHandle) procList); |
|
613 ()) |
|
614 in |
|
615 (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) |
|
616 (**********************************) |
|
617 if (isSome cmdsFromIsa) |
|
618 then (* deal with input from Isabelle *) |
|
619 if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" ) |
|
620 then |
|
621 let val child_handles = map cmdchildHandle procList |
425 in |
622 in |
426 if null pdl |
623 killChildren child_handles; |
427 then |
624 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) |
428 NONE |
625 loop ([]) |
429 else if (OS.IO.isIn (hd pdl)) |
|
430 then SOME (getCmds (toParentStr, fromParentStr, [])) |
|
431 else NONE |
|
432 end |
626 end |
433 else NONE |
627 else |
|
628 if ((length procList)<10) (********************) |
|
629 then (* Execute locally *) |
|
630 let |
|
631 val newProcList = execCmds (valOf cmdsFromIsa) procList |
|
632 val parentID = Posix.ProcEnv.getppid() |
|
633 val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ") |
|
634 val newProcList' =checkChildren (newProcList, toParentStr) |
|
635 |
|
636 val _ = warning("off to keep watching...") |
|
637 val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ") |
|
638 in |
|
639 loop (newProcList') |
|
640 end |
|
641 else (* Execute remotely *) |
|
642 (* (actually not remote for now )*) |
|
643 let |
|
644 val newProcList = execCmds (valOf cmdsFromIsa) procList |
|
645 val parentID = Posix.ProcEnv.getppid() |
|
646 val newProcList' =checkChildren (newProcList, toParentStr) |
|
647 in |
|
648 loop (newProcList') |
|
649 end |
|
650 else (* No new input from Isabelle *) |
|
651 let val newProcList = checkChildren ((procList), toParentStr) |
|
652 in |
|
653 (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n "); |
|
654 loop (newProcList) |
|
655 end |
434 end |
656 end |
435 |
657 in |
436 fun pollChildInput (fromStr) = |
658 loop (procList) |
437 let val _ = File.append (File.tmp_path (Path.basic "child_poll")) |
659 end |
438 ("In child_poll\n") |
660 |
439 val iod = getInIoDesc fromStr |
661 |
440 in |
662 in |
441 if isSome iod |
663 (***************************) |
442 then |
664 (*** Sort out pipes ********) |
443 let val pd = OS.IO.pollDesc (valOf iod) |
665 (***************************) |
444 in |
666 |
445 if (isSome pd ) then |
667 Posix.IO.close (#outfd p1); |
446 let val pd' = OS.IO.pollIn (valOf pd) |
668 Posix.IO.close (#infd p2); |
447 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) |
669 Posix.IO.dup2{old = oldchildin, new = fromParent}; |
448 in |
670 Posix.IO.close oldchildin; |
449 if null pdl |
671 Posix.IO.dup2{old = oldchildout, new = toParent}; |
450 then |
672 Posix.IO.close oldchildout; |
451 ( File.append (File.tmp_path (Path.basic "child_poll_res")) |
673 |
452 ("Null pdl \n");NONE) |
674 (***************************) |
453 else if (OS.IO.isIn (hd pdl)) |
675 (* start the watcher loop *) |
454 then |
676 (***************************) |
455 (let val inval = (TextIO.inputLine fromStr) |
677 keepWatching (toParentStr, fromParentStr, procList); |
456 val _ = File.append (File.tmp_path (Path.basic "child_poll_res")) (inval^"\n") |
|
457 in |
|
458 SOME inval |
|
459 end) |
|
460 else |
|
461 ( File.append (File.tmp_path (Path.basic "child_poll_res")) |
|
462 ("Null pdl \n");NONE) |
|
463 end |
|
464 else NONE |
|
465 end |
|
466 else NONE |
|
467 end |
|
468 |
|
469 |
|
470 (****************************************************************************) |
678 (****************************************************************************) |
471 (* Check all vampire processes currently running for output *) |
679 (* fake return value - actually want the watcher to loop until killed *) |
472 (****************************************************************************) |
680 (****************************************************************************) |
473 (*********************************) |
681 Posix.Process.wordToPid 0w0 |
474 fun checkChildren ([], toParentStr) = [] (*** no children to check ********) |
682 end); |
475 (*********************************) |
683 (* end case *) |
476 | checkChildren ((childProc::otherChildren), toParentStr) = |
|
477 let val _ = File.append (File.tmp_path (Path.basic "child_check")) |
|
478 ("In check child, length of queue:"^(string_of_int (length (childProc::otherChildren)))^"\n") |
|
479 val (childInput,childOutput) = cmdstreamsOf childProc |
|
480 val child_handle= cmdchildHandle childProc |
|
481 (* childCmd is the .dfg file that the problem is in *) |
|
482 val childCmd = fst(snd (cmdchildInfo childProc)) |
|
483 val _ = File.append (File.tmp_path (Path.basic "child_command")) |
|
484 (childCmd^"\n") |
|
485 (* now get the number of the subgoal from the filename *) |
|
486 val sg_num = (*if (!SpassComm.spass ) |
|
487 then |
|
488 int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd))) |
|
489 else*) |
|
490 int_of_string(hd (rev(explode childCmd))) |
|
491 |
|
492 val childIncoming = pollChildInput childInput |
|
493 val _ = File.append (File.tmp_path (Path.basic "child_check_polled")) |
|
494 ("finished polling child \n") |
|
495 val parentID = Posix.ProcEnv.getppid() |
|
496 val prover = cmdProver childProc |
|
497 val thmstring = cmdThm childProc |
|
498 val sign = sign_of_thm thm |
|
499 val prems = prems_of thm |
|
500 val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) |
|
501 val _ = warning("subgoals forked to checkChildren: "^prems_string) |
|
502 val goalstring = cmdGoal childProc |
|
503 val _ = File.append (File.tmp_path (Path.basic "child_comms")) |
|
504 (prover^thmstring^goalstring^childCmd^"\n") |
|
505 in |
|
506 if (isSome childIncoming) |
|
507 then |
|
508 (* check here for prover label on child*) |
|
509 let val _ = File.write (File.tmp_path (Path.basic "child_incoming")) |
|
510 ("subgoals forked to checkChildren:"^ |
|
511 prems_string^prover^thmstring^goalstring^childCmd) |
|
512 val childDone = (case prover of |
|
513 "vampire" => (VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) |
|
514 |"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses) ) ) |
|
515 in |
|
516 if childDone (**********************************************) |
|
517 then (* child has found a proof and transferred it *) |
|
518 (* Remove this child and go on to check others*) |
|
519 (**********************************************) |
|
520 (Unix.reap child_handle; |
|
521 checkChildren(otherChildren, toParentStr)) |
|
522 else |
|
523 (**********************************************) |
|
524 (* Keep this child and go on to check others *) |
|
525 (**********************************************) |
|
526 (childProc::(checkChildren (otherChildren, toParentStr))) |
|
527 end |
|
528 else |
|
529 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output "; |
|
530 childProc::(checkChildren (otherChildren, toParentStr))) |
|
531 end |
|
532 |
|
533 |
|
534 (********************************************************************) |
|
535 (* call resolution processes *) |
|
536 (* settings should be a list of strings *) |
|
537 (* e.g. ["-t 300", "-m 100000"] (TextIO.input instr)^ *) |
|
538 (* takes list of (string, string, string list, string)list proclist *) |
|
539 (********************************************************************) |
|
540 |
|
541 |
|
542 (*** add subgoal id num to this *) |
|
543 fun execCmds [] procList = procList |
|
544 | execCmds ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList = let val _ = File.append (File.tmp_path (Path.basic "pre_exec_child")) ("\nAbout to execute command for goal:\n"^goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) |
|
545 in |
|
546 if (prover = "spass") |
|
547 then |
|
548 let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = |
|
549 (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file]))) |
|
550 val (instr, outstr) = Unix.streamsOf childhandle |
|
551 val newProcList = (((CMDPROC{ |
|
552 prover = prover, |
|
553 cmd = file, |
|
554 thmstring = thmstring, |
|
555 goalstring = goalstring, |
|
556 proc_handle = childhandle, |
|
557 instr = instr, |
|
558 outstr = outstr })::procList)) |
|
559 val _ = File.append (File.tmp_path (Path.basic "exec_child")) |
|
560 ("\nexecuting command for goal:\n"^ |
|
561 goalstring^proverCmd^(concat settings)^file^" at "^(Date.toString(Date.fromTimeLocal(Time.now())))) |
|
562 in |
|
563 Posix.Process.sleep (Time.fromSeconds 1);execCmds cmds newProcList |
|
564 end |
|
565 else |
|
566 let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc = |
|
567 (Unix.execute(proverCmd, (settings@[file]))) |
|
568 val (instr, outstr) = Unix.streamsOf childhandle |
|
569 |
|
570 val newProcList = (CMDPROC{ |
|
571 prover = prover, |
|
572 cmd = file, |
|
573 thmstring = thmstring, |
|
574 goalstring = goalstring, |
|
575 proc_handle = childhandle, |
|
576 instr = instr, |
|
577 outstr = outstr }) :: procList |
|
578 |
|
579 val _ = File.append (File.tmp_path (Path.basic "exec_child")) |
|
580 ("executing command for goal:\n"^ |
|
581 goalstring^proverCmd^(concat settings)^file^ |
|
582 " at "^(Date.toString(Date.fromTimeLocal(Time.now())))) |
|
583 in |
|
584 Posix.Process.sleep (Time.fromSeconds 1); execCmds cmds newProcList |
|
585 end |
|
586 end |
|
587 |
|
588 |
|
589 (****************************************) |
|
590 (* call resolution processes remotely *) |
|
591 (* settings should be a list of strings *) |
|
592 (* e.g. ["-t 300", "-m 100000"] *) |
|
593 (****************************************) |
|
594 |
|
595 (* fun execRemoteCmds [] procList = procList |
|
596 | execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList = |
|
597 let val newProcList = mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList) |
|
598 in |
|
599 execRemoteCmds cmds newProcList |
|
600 end |
|
601 *) |
|
602 |
|
603 fun printList (outStr, []) = () |
|
604 | printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs)) |
|
605 |
|
606 |
|
607 (**********************************************) |
|
608 (* Watcher Loop *) |
|
609 (**********************************************) |
|
610 |
|
611 fun keepWatching (toParentStr, fromParentStr,procList) = |
|
612 let fun loop (procList) = |
|
613 let val cmdsFromIsa = pollParentInput () |
|
614 fun killchildHandler (n:int) = |
|
615 (TextIO.output(toParentStr, "Killing child proof processes!\n"); |
|
616 TextIO.flushOut toParentStr; |
|
617 killChildren (map (cmdchildHandle) procList); |
|
618 ()) |
|
619 in |
|
620 (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*) |
|
621 (**********************************) |
|
622 if (isSome cmdsFromIsa) |
|
623 then (* deal with input from Isabelle *) |
|
624 if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" ) |
|
625 then |
|
626 let val child_handles = map cmdchildHandle procList |
|
627 in |
|
628 killChildren child_handles; |
|
629 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*) |
|
630 loop ([]) |
|
631 end |
|
632 else |
|
633 if ((length procList)<10) (********************) |
|
634 then (* Execute locally *) |
|
635 let |
|
636 val newProcList = execCmds (valOf cmdsFromIsa) procList |
|
637 val parentID = Posix.ProcEnv.getppid() |
|
638 val _ = (File.append (File.tmp_path (Path.basic "prekeep_watch")) "Just execed a child\n ") |
|
639 val newProcList' =checkChildren (newProcList, toParentStr) |
|
640 |
|
641 val _ = warning("off to keep watching...") |
|
642 val _ = (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching...\n ") |
|
643 in |
|
644 (*Posix.Process.sleep (Time.fromSeconds 1);*) |
|
645 loop (newProcList') |
|
646 end |
|
647 else (* Execute remotely *) |
|
648 (* (actually not remote for now )*) |
|
649 let |
|
650 val newProcList = execCmds (valOf cmdsFromIsa) procList |
|
651 val parentID = Posix.ProcEnv.getppid() |
|
652 val newProcList' =checkChildren (newProcList, toParentStr) |
|
653 in |
|
654 (*Posix.Process.sleep (Time.fromSeconds 1);*) |
|
655 loop (newProcList') |
|
656 end |
|
657 else (* No new input from Isabelle *) |
|
658 let val newProcList = checkChildren ((procList), toParentStr) |
|
659 in |
|
660 (*Posix.Process.sleep (Time.fromSeconds 1);*) |
|
661 (File.append (File.tmp_path (Path.basic "keep_watch")) "Off to keep watching.2..\n "); |
|
662 loop (newProcList) |
|
663 end |
|
664 end |
|
665 in |
|
666 loop (procList) |
|
667 end |
|
668 |
|
669 |
|
670 in |
|
671 (***************************) |
|
672 (*** Sort out pipes ********) |
|
673 (***************************) |
|
674 |
|
675 Posix.IO.close (#outfd p1); |
|
676 Posix.IO.close (#infd p2); |
|
677 Posix.IO.dup2{old = oldchildin, new = fromParent}; |
|
678 Posix.IO.close oldchildin; |
|
679 Posix.IO.dup2{old = oldchildout, new = toParent}; |
|
680 Posix.IO.close oldchildout; |
|
681 |
|
682 (***************************) |
|
683 (* start the watcher loop *) |
|
684 (***************************) |
|
685 keepWatching (toParentStr, fromParentStr, procList); |
|
686 (****************************************************************************) |
|
687 (* fake return value - actually want the watcher to loop until killed *) |
|
688 (****************************************************************************) |
|
689 Posix.Process.wordToPid 0w0 |
|
690 end); |
|
691 (* end case *) |
|
692 |
684 |
693 |
685 |
694 val _ = TextIO.flushOut TextIO.stdOut |
686 val _ = TextIO.flushOut TextIO.stdOut |
695 |
687 |
696 (*******************************) |
688 (*******************************) |