src/HOL/Tools/ATP/watcher.sig
author paulson
Thu Apr 21 15:05:24 2005 +0200 (2005-04-21)
changeset 15789 4cb16144c81b
parent 15782 a1863ea9052b
child 15919 b30a35432f5a
permissions -rw-r--r--
added hearder lines and deleted some redundant material
paulson@15789
     1
(*  ID:         $Id$
quigley@15642
     2
    Author:     Claire Quigley
quigley@15642
     3
    Copyright   2004  University of Cambridge
quigley@15642
     4
*)
quigley@15642
     5
quigley@15642
     6
(***************************************************************************)
quigley@15642
     7
(*  The watcher process starts a Spass process when it receives a        *)
quigley@15642
     8
(*  message from Isabelle                                                  *)
quigley@15642
     9
(*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
quigley@15642
    10
(*  and removes dead processes.  Also possible to kill all the vampire     *)
quigley@15642
    11
(*  processes currently running.                                           *)
quigley@15642
    12
(***************************************************************************)
quigley@15642
    13
quigley@15642
    14
quigley@15642
    15
signature WATCHER =
paulson@15789
    16
sig
quigley@15642
    17
quigley@15642
    18
(*****************************************************************************************)
quigley@15642
    19
(*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
quigley@15642
    20
(*  callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list             *)
quigley@15642
    21
(*****************************************************************************************)
quigley@15642
    22
quigley@15782
    23
val callResProvers : TextIO.outstream *(string* string*string *string*string*string*string*string*string) list -> unit
quigley@15642
    24
quigley@15642
    25
quigley@15642
    26
quigley@15642
    27
(************************************************************************)
quigley@15642
    28
(* Send message to watcher to kill currently running resolution provers *)
quigley@15642
    29
(************************************************************************)
quigley@15642
    30
quigley@15642
    31
val callSlayer : TextIO.outstream -> unit
quigley@15642
    32
quigley@15642
    33
quigley@15642
    34
quigley@15642
    35
(**********************************************************)
quigley@15642
    36
(* Start a watcher and set up signal handlers             *)
quigley@15642
    37
(**********************************************************)
quigley@15642
    38
quigley@15782
    39
val createWatcher : Thm.thm -> TextIO.instream * TextIO.outstream * Posix.Process.pid
quigley@15642
    40
quigley@15642
    41
quigley@15642
    42
quigley@15642
    43
(**********************************************************)
quigley@15642
    44
(* Kill watcher process                                   *)
quigley@15642
    45
(**********************************************************)
quigley@15642
    46
quigley@15642
    47
val killWatcher : (Posix.Process.pid) -> unit
quigley@15642
    48
quigley@15642
    49
quigley@15642
    50
end