package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

doc/coq-core.perf/Perf/index.html

Module PerfSource

Global CPU instruction counter.

Sourceval init : unit -> unit

init () initialises, resets to 0, and starts the instruction counter. In case of an error, the Failure exception is raised, and the counter state is fully re-initialised so that init may be called again. Initialization is required prior to calling the drop and peek functions.

Sourceval drop : unit -> unit

drop () undoes the effect of init, and frees all resources used by the internal state of the instruction counter. Note that the counter must have been initialised before calling drop, otherwise Failure is raised.

Sourceval peek : unit -> Int64.t

peek () reads the value of the instruction counter, which corresponds to the number of instructions run by the CPU since the last (successful) call to init. Note that Failure is raised in case of an error, including if the function is called while the counter is not initialised.

OCaml

Innovation. Community. Security.