diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-22 10:23:14 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-01-26 14:20:52 +0100 |
commit | ea17a2a371d0d791f439e0a4c6610819ecb6f9b6 (patch) | |
tree | e7a91131f773efedbbcdb79d035b6c6d443b1e55 /lib/spawn.mli | |
parent | 26b6134c3cd333d7fc78c665be5fd1394a546395 (diff) |
Spawn: managed processes
The Spawn and Spawned modules factor the operation of spawning
a process. Both synchronous and asynchronous channels are supported.
Both threaded and glib like main loop models are supported. Still,
not all combinations are truly tested not equipped with a decent API:
only async + glib and sync + thread are, since these are the models we
use for coqide<->coqtop and coqtop<->worker respectively.
Diffstat (limited to 'lib/spawn.mli')
-rw-r--r-- | lib/spawn.mli | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/lib/spawn.mli b/lib/spawn.mli new file mode 100644 index 000000000..1554e0a1e --- /dev/null +++ b/lib/spawn.mli @@ -0,0 +1,88 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \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 + + (* Installs a callback, called every [sec] seconds. If the returned value + * is true the process is killed *) + val kill_if : handle -> sec:int -> (unit -> bool) -> unit +end + +(* Abstraction to work with both threads and main loop models *) +module type Timer = sig + + val add_timeout : sec:int -> (unit -> bool) -> unit +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 + + include Timer +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 : Timer) : 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 |