src/HOL/Tools/ATP/watcher.sig
author quigley
Wed, 20 Apr 2005 18:01:50 +0200
changeset 15782 a1863ea9052b
parent 15658 2edb384bf61f
child 15789 4cb16144c81b
permissions -rw-r--r--
Corrected the problem with the ATP directory.


(*  Title:      Watcher.ML
    Author:     Claire Quigley
    Copyright   2004  University of Cambridge
*)

(***************************************************************************)
(*  The watcher process starts a Spass process when it receives a        *)
(*  message from Isabelle                                                  *)
(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
(*  and removes dead processes.  Also possible to kill all the vampire     *)
(*  processes currently running.                                           *)
(***************************************************************************)


signature WATCHER =
  sig

(*****************************************************************************************)
(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
(*  callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list             *)
(*****************************************************************************************)

val callResProvers : TextIO.outstream *(string* string*string *string*string*string*string*string*string) list -> unit



(************************************************************************)
(* Send message to watcher to kill currently running resolution provers *)
(************************************************************************)

val callSlayer : TextIO.outstream -> unit



(**********************************************************)
(* Start a watcher and set up signal handlers             *)
(**********************************************************)

val createWatcher : Thm.thm -> TextIO.instream * TextIO.outstream * Posix.Process.pid



(**********************************************************)
(* Kill watcher process                                   *)
(**********************************************************)

val killWatcher : (Posix.Process.pid) -> unit


end