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 (5)

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.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

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

Module FlagsSource

Global options of the system.

WARNING: don't add new entries to this file!

This file is own its way to deprecation in favor of a purely functional state, but meanwhile it will contain options that are truly global to the system such as debug

If you are thinking about adding a global flag, well, just don't. First of all, options make testins exponentially more expensive, due to the growth of flag combinations. So please make some effort in order for your idea to work in a configuration-free manner.

If you absolutely must pass an option to your new system, then do so as a functional argument so flags are exposed to unit testing. Then, register such parameters with the proper state-handling mechanism of the top-level subsystem of Rocq.

Command-line flags

Sourceval async_proofs_worker_id : string ref

Async-related flags

Sourceval async_proofs_is_worker : unit -> bool
Sourceval in_debugger : bool ref

Debug flags

Sourceval in_ml_toplevel : bool ref
Sourceval in_synterp_phase : bool option ref
Sourceval beautify : bool ref
Sourceval beautify_file : bool ref
Sourceval quiet : bool ref
Sourceval silently : ('a -> 'b) -> 'a -> 'b
Sourceval verbosely : ('a -> 'b) -> 'a -> 'b
Sourceval if_silent : ('a -> unit) -> 'a -> unit
Sourceval if_verbose : ('a -> unit) -> 'a -> unit
Sourceval with_modified_ref : 'c ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b

with_modified_ref r nf f x Temporarily modify a reference in the call to f x . Be very careful with these functions, it is very easy to fall in the typical problem with effects:

with_modified_ref r nf f x y != with_modified_ref r nf (f x) y

Sourceval with_option : bool ref -> ('a -> 'b) -> 'a -> 'b

Temporarily activate an option (to activate option o on f x y z, use with_option o (f x y) z)

Sourceval with_options : bool ref list -> ('a -> 'b) -> 'a -> 'b

As with_option, but on several flags.

Sourceval without_option : bool ref -> ('a -> 'b) -> 'a -> 'b

Temporarily deactivate an option

Sourceval test_mode : bool ref

Flag set when the test-suite is called.

  • display verbose information for Fail
  • print quickfix info in error printers