diff options
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 122 |
1 files changed, 72 insertions, 50 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 43a040822..041485237 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -27,82 +27,104 @@ val check_connection : string list -> unit (** * The structure describing a coqtop sub-process *) (** Liveness management of coqtop is automatic. Whenever a Coqtop dies abruptly, - this module is responsible for relaunching the whole process. The hook + this module is responsible for relaunching the whole process. The hook passed as an argument in coqtop construction will be called after such an - abrupt failure. In particular, it is NOT called when explicitely requesting + abrupt failure. In particular, it is NOT called when explicitely requesting coqtop to close or to reset. *) type coqtop type handle -(** Count of all active coqtops *) -val coqtop_zombies : unit -> int +(** * Coqtop tasks + + A task is a group of sequential calls to be perform on a coqtop. + If a task is already sent to coqtop, it is considered busy + ([is_computing] will answer [true]), and other task submission + will be rejected. + + A task is represented as a continuation, with a coqtop [handle] + as first argument, and a final inner continuation as 2nd argument. + This inner continuation should be runned at the end of the task. + Any exception occuring within the task will trigger a coqtop reset. +*) + +type void +type task = handle -> (unit->void) -> void + +(** Check if coqtop is computing, i.e. already has a current task *) +val is_computing : coqtop -> bool (** * Starting / signaling / ending a real coqtop sub-process *) -(** Create a coqtop process out of a hook and some command-line arguments. - The hook SHALL NOT use [grab] or its variants, otherwise you'll deadlock! *) -val spawn_coqtop : (handle -> unit) -> string list -> coqtop +(** Create a coqtop process with some command-line arguments. *) +val spawn_coqtop : string list -> coqtop -(** Interrupt the current computation of coqtop. Asynchronous. *) +(** Register a handler called when a coqtop dies (badly or on purpose) *) +type reset_kind = Planned | Unexpected +val set_reset_handler : coqtop -> (reset_kind -> task) -> unit + +(** Finish initializing a freshly spawned coqtop, by running a first task on it. + The task should run its inner continuation at the end. *) +val init_coqtop : coqtop -> task -> unit + +(** Interrupt the current computation of coqtop. *) val break_coqtop : coqtop -> unit (** Close coqtop. Subsequent requests will be discarded. Hook ignored. *) val close_coqtop : coqtop -> unit -(** Reset coqtop. Pending requests will be discarded. Default hook ignored, - provided one used instead. *) -val reset_coqtop : coqtop -> (handle -> unit) -> unit +(** Reset coqtop. Pending requests will be discarded. The reset handler + of coqtop will be called with [Planned] as first argument *) +val reset_coqtop : coqtop -> unit -(** Last resort against a reluctant coqtop (a.k.a. chainsaw massacre). - Asynchronous. *) -val kill_coqtop : coqtop -> unit +(** In win32, we'll use a different kill function than Unix.kill *) -(** * Coqtop commmunication *) +val killer : (int -> unit) ref +val soft_killer : (int -> unit) ref +val interrupter : (int -> unit) ref -(** Start a coqtop dialogue and ensure that there is no interfering process. - - If coqtop ever dies during the computation, this function restarts coqtop - and calls the restart hook with the fresh coqtop. - - If the argument function raises an exception, it is propagated. - - The request may be discarded if a [close_coqtop] or [reset_coqtop] occurs - before its completion. -*) -val grab : coqtop -> (handle -> unit) -> unit +(** [set_final_countdown] triggers an exit of coqide after + some last cycles for closing remaining coqtop zombies *) -(** As [grab], but applies the second callback if coqtop is already busy. Please - consider using [try_grab] instead of [grab] except if you REALLY want - something to happen. *) -val try_grab : coqtop -> (handle -> unit) -> (unit -> unit) -> unit +val final_countdown : unit -> unit -(** Check if coqtop is computing. Does not take any lock. *) -val is_computing : coqtop -> bool +(** * Coqtop commmunication *) -(** Check if coqtop is closed. Does not take any lock. *) -val is_closed : coqtop -> bool +(** Try to schedule a task on a coqtop. If coqtop is available, the task + callback is run (asynchronously), otherwise the [(unit->unit)] callback + is triggered. + - If coqtop ever dies during the computation, this function restarts coqtop + and calls the restart hook with the fresh coqtop. + - If the argument function raises an exception, a coqtop reset occurs. + - The task may be discarded if a [close_coqtop] or [reset_coqtop] occurs + before its completion. + - The task callback should run its inner continuation at the end. *) -(** In win32, we'll use a different kill function than Unix.kill *) +val try_grab : coqtop -> task -> (unit -> unit) -> unit -val killer : (int -> unit) ref -val interrupter : (int -> unit) ref +(** * Atomic calls to coqtop -(** * Calls to Coqtop, cf [Serialize] for more details *) + These atomic calls can be combined to form arbitrary multi-call tasks. + They correspond to the protocol calls (cf [Serialize] for more details). + Note that each call is asynchronous: it will return immediately, + but the inner callback will be executed later to handle the call answer + when this answer is available. + Except for interp, we use the default logger for any call. *) -type logger = Interface.message_level -> string -> unit -(** Except for interp, we use the default logger for any call. *) +type 'a atask = handle -> ('a Interface.value -> void) -> void -val interp : - handle -> logger -> ?raw:bool -> ?verbose:bool -> string -> string Interface.value -val rewind : handle -> int -> int Interface.value -val status : handle -> Interface.status Interface.value -val goals : handle -> Interface.goals option Interface.value -val evars : handle -> Interface.evar list option Interface.value -val hints : handle -> (Interface.hint list * Interface.hint) option Interface.value -val inloadpath : handle -> string -> bool Interface.value -val mkcases : handle -> string -> string list list Interface.value -val search : handle -> Interface.search_flags -> string Interface.coq_object list Interface.value +val interp : ?logger:Ideutils.logger -> ?raw:bool -> ?verbose:bool -> + string -> string atask +val rewind : int -> int atask +val status : Interface.status atask +val goals : Interface.goals option atask +val evars : Interface.evar list option atask +val hints : (Interface.hint list * Interface.hint) option atask +val inloadpath : string -> bool atask +val mkcases : string -> string list list atask +val search : Interface.search_flags -> string Interface.coq_object list atask -(** A specialized version of [raw_interp] dedicated to - set/unset options. *) +(** A specialized version of [raw_interp] dedicated to set/unset options. *) module PrintOpt : sig @@ -116,5 +138,5 @@ sig val universes : t val set_printing_width : int -> unit - val set : handle -> (t * bool) list -> unit + val set : (t * bool) list -> task end |