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

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.1.1.tar.gz
sha256=35cd03fc4193969b1cce01190340e5c129c1ba8f02242a9e6dff4b83be118759

doc/rocq-runtime.stm/Stm/AsyncOpts/index.html

Module Stm.AsyncOptsSource

Sourcetype cache =
  1. | Force
Sourcetype async_proofs =
  1. | APoff
  2. | APonLazy
  3. | APon
Sourcetype tac_error_filter =
  1. | FNone
  2. | FOnly of string list
  3. | FAll
Sourcetype stm_opt = {
  1. spawn_args : string list;
  2. async_proofs_n_workers : int;
  3. async_proofs_n_tacworkers : int;
  4. async_proofs_cache : cache option;
  5. async_proofs_mode : async_proofs;
  6. async_proofs_private_flags : string option;
  7. async_proofs_never_reopen_branch : bool;
  8. async_proofs_tac_error_resilience : tac_error_filter;
  9. async_proofs_cmd_error_resilience : bool;
  10. async_proofs_delegation_threshold : float;
  11. async_proofs_worker_priority : CoqworkmgrApi.priority;
}
Sourceval default_opts : spawn_args:string list -> stm_opt