package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.lib/NewProfile/index.html

Module `NewProfile`Source

Sourcemodule MiniJson : sig ... end

Sourcemodule Counters : sig ... end

Source

val profile : 
  string ->
  ?args:(unit -> (string * MiniJson.t) list) ->
  (unit -> 'a) ->
  unit ->
  'a

Profile the given function.

args is called only if profiling is active, it is used to produce additional annotations.

Sourceval is_profiling : unit -> bool

Sourcetype settings = {

output : Format.formatter;
fname : string;

}

Sourceval init : settings -> unit

Profiling must not be active. Activates profiling with a fresh state.

Sourceval finish : unit -> unit

Profiling must be active. Deactivates profiling.

Sourcetype accu

Profiling state accumulator.

Sourceval pause : unit -> accu option

Returns None if profiling is inactive. Deactivates profiling if it is active, returning the current state.

Sourceval resume : accu -> unit

Profiling must not be active. Activates profiling with the given state.

Sourcetype sums = (float * int) CString.Map.t

Timings for sub-events: for each event, how long it took and how many times it was called.

Sourceval empty_sums : sums

Sourceval sums_union : sums -> sums -> sums

Sourceval with_profiling : (unit -> 'a) -> MiniJson.t list * sums * 'a

Runs the given function with profiling active and returns the produced events and sum times of subevents.

Sourceval insert_results : MiniJson.t list -> sums -> unit

Profiling must be active. Outputs the given events and includes the sum times in the current event.

Sourceval pptime : Format.formatter -> float -> unit

Pretty print a time given in seconds using smaller units as needed.

Custom outputs

Sourceval format_header : Format.formatter -> unit

Output header for profile files

Sourceval format_footer : Format.formatter -> unit

Output footer for profile files and flushes the formatter.