package rocq-runtime
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.vernac/ComTactic/index.html
Module ComTacticSource
Tactic interpreters have to register their interpretation function
val 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.
val solve :
pstate:Declare.Proof.t ->
Goal_select.t ->
info:int option ->
interpretable ->
with_end_tac:bool ->
Declare.Proof.tEntry 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.
type parallel_solver =
pstate:Declare.Proof.t ->
info:int option ->
interpretable ->
abstract:bool ->
with_end_tac:bool ->
Declare.Proof.tpar: 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.
Entry point when the goal selector is par:
By default par: is implemented with all: (sequential). The STM and LSP document manager provide "more parallel" implementations