package rocq-runtime

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

Install 

dune-project
 Dependency

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

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.vernac/VernacControl/index.html

Module VernacControlSource

Sourcetype 'state control_entry

Partially interpreted control flags.

Sourcetype 'state control_entries = 'state control_entry list
Sourceval from_syntax : Vernacexpr.control_flag list -> unit control_entries

Translate from syntax and add default timeout.

Sourcetype ('st0, 'st) with_local_state = {
  1. with_local_state : 'a. 'st0 -> (unit -> 'a) -> 'st * 'a;
}

with_local_state state0 f should run f with state0 installed, capture the state produced by running f and revert the global state afterwards.

Sourceval trivial_state : (unit, unit) with_local_state
Sourceval under_control : loc:Loc.t option -> with_local_state:('state0, 'state) with_local_state -> 'state0 control_entries -> noop:'b -> (unit -> 'b) -> 'state control_entries * 'b

under_control ~loc ~with_local_state control ~noop f runs f () in the context given by the control.

If the control cause execution to end with no more work to be done and no error (eg Fail when f raised an exception) then noop is returned.

Sourceval after_last_phase : loc:Loc.t option -> _ control_entries -> bool

Print any final messages (eg from Time) and raise final exceptions (eg from Fail when the command did not fail). The returned boolean tells if we should be noop (Fail where the command failed or Succeed where it succeeded).