package coq-core

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

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

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.