diff options
Diffstat (limited to 'lib/spawn.mli')
-rw-r--r-- | lib/spawn.mli | 81 |
1 files changed, 81 insertions, 0 deletions
diff --git a/lib/spawn.mli b/lib/spawn.mli new file mode 100644 index 00000000..8022573b --- /dev/null +++ b/lib/spawn.mli @@ -0,0 +1,81 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* This module implements spawning/killing managed processes with a + * synchronous or asynchronous comunication channel that works with + * threads or with a glib like main loop model. + * + * This module requires no threads and no main loop model. It takes care + * of using the fastest communication channel given the underlying OS and + * the requested kind of communication. + * + * The spawned process must use the Spawned module to init its communication + * channels. + *) + +(* This is the control panel for managed processes *) +module type Control = sig + type handle + + val kill : handle -> unit + val stats : handle -> Gc.stat + val wait : handle -> Unix.process_status + val unixpid : handle -> int + + (* What is used in debug messages *) + val uid : handle -> string + + val is_alive : handle -> bool +end + +(* Abstraction to work with both threads and main loop models *) +module type Empty = sig end + +module type MainLoopModel = sig + type async_chan + type condition + type watch_id + + val add_watch : callback:(condition list -> bool) -> async_chan -> watch_id + val remove_watch : watch_id -> unit + val read_all : async_chan -> string + val async_chan_of_file : Unix.file_descr -> async_chan + val async_chan_of_socket : Unix.file_descr -> async_chan +end + +(* spawn a process and read its output asynchronously *) +module Async(ML : MainLoopModel) : sig + type process + + (* If the returned value is false the callback is never called again and + * the process is killed *) + type callback = ML.condition list -> read_all:(unit -> string) -> bool + + val spawn : + ?prefer_sock:bool -> ?env:string array -> string -> string array -> + callback -> process * out_channel + + include Control with type handle = process +end + +(* spawn a process and read its output synchronously *) +module Sync(T : Empty) : sig + type process + + val spawn : + ?prefer_sock:bool -> ?env:string array -> string -> string array -> + process * in_channel * out_channel + + include Control with type handle = process +end + +(* This is exported to separate the Spawned module, that for simplicity assumes + * Threads so it is in a separate file *) +type req = ReqDie | ReqStats | Hello of int * int +val proto_version : int +type resp = RespStats of Gc.stat |