package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install

dune-project
 Dependency

Authors

Maintainers

Sources

rocq-9.1.1.tar.gz
sha256=35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759

doc/rocq-runtime.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.