package rocq-runtime

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

Install

dune-project
 Dependency

Authors

Maintainers

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

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.