package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Global control of Coq.

exception Timeout

Used to convert signals to exceptions

val enable_thread_delay : bool Stdlib.ref

Will periodically call Thread.delay if set to true

val interrupt : bool Stdlib.ref

Coq interruption: set the following boolean reference to interrupt Coq (it eventually raises Break, simulating a Ctrl-C)

val check_for_interrupt : unit -> unit

Use this function as a potential yield function. If interrupt has been set, il will raise Sys.Break.

val timeout : float -> ('a -> 'b) -> 'a -> 'b option

timeout n f x tries to compute Some (f x), and if it fails to do so before n seconds, returns None instead.

type timeout = {
  1. timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option;
}

Set a particular timeout function; warning, this is an internal API and it is scheduled to go away.

val set_timeout : timeout -> unit
val protect_sigalrm : ('a -> 'b) -> 'a -> 'b

protect_sigalrm f x computes f x, but if SIGALRM is received during that computation, the signal handler is executed only once the computation is terminated. Otherwise said, it makes the execution of f atomic w.r.t. handling of SIGALRM.

This is useful for example to prevent the implementation of `Timeout` to interrupt I/O routines, generating ill-formed output.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct