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.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

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

Module ComTacticSource

Sourcetype interpretable

Tactic interpreters have to register their interpretation function

Sourcetype 'a tactic_interpreter = private
  1. | Interpreter of 'a -> interpretable
Sourceval register_tactic_interpreter : string -> ('a -> unit Proofview.tactic) -> 'a tactic_interpreter

'a should be marshallable if ever used with par:. Must be called no more than once per process with a particular string: make sure to use partial application.

Sourceval solve : pstate:Declare.Proof.t -> Goal_select.t -> info:int option -> interpretable -> with_end_tac:bool -> Declare.Proof.t

Entry point for toplevel tactic expression execution. It calls Proof.solve after having interpreted the tactic, and after the tactic runs it unfocus as much as needed to put a goal under focus.

Sourcetype parallel_solver = pstate:Declare.Proof.t -> info:int option -> interpretable -> abstract:bool -> with_end_tac:bool -> Declare.Proof.t

par: tac runs tac on all goals, possibly in parallel using a worker pool. If tac is abstract tac1, then abstract is passed explicitly to the solver and tac1 passed to worker since it is up to master to opacify the sub proofs produced by the workers.

Sourceval solve_parallel : parallel_solver

Entry point when the goal selector is par:

Sourceval set_par_implementation : parallel_solver -> unit

By default par: is implemented with all: (sequential). The STM and LSP document manager provide "more parallel" implementations