package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

state-transaction-machine interface

module AsyncOpts : sig ... end
type stm_doc_type =
  1. | VoDoc of string
  2. | VioDoc of string
  3. | Interactive of Coqargs.top

The STM document type stm_doc_type determines some properties such as what uncompleted proofs are allowed and what gets recorded to aux files.

type stm_init_options = {
  1. doc_type : stm_doc_type;
    (*

    The STM does set some internal flags differently depending on the specified doc_type. This distinction should disappear at some some point.

    *)
  2. injections : Coqargs.injection_command list;
    (*

    Injects Require and Set/Unset commands before the initial state is ready

    *)
  3. stm_options : AsyncOpts.stm_opt;
    (*

    Low-level STM options

    *)
}

STM initialization options:

type doc

The type of a STM document

val init_process : AsyncOpts.stm_opt -> unit

init_process performs some low-level initialization, call early

val init_core : unit -> unit

init_core snapshorts the initial system state

val new_doc : stm_init_options -> doc * Stateid.t

new_doc opt Creates a new document with options opt

val parse_sentence : doc:doc -> Stateid.t -> entry:(Pvernac.proof_mode option -> 'a Pcoq.Entry.t) -> Pcoq.Parsable.t -> 'a

parse_sentence sid entry pa Reads a sentence from pa with parsing state sid and non terminal entry. entry receives in input the current proof mode. sid should be associated with a valid parsing state (which may not be the case if an error was raised at parsing time).

val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> bool -> Vernacexpr.vernac_control -> doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
val get_prev_proof : doc:doc -> Stateid.t -> Proof.t option
val get_proof : doc:doc -> Stateid.t -> Proof.t option
val query : doc:doc -> at:Stateid.t -> route:Feedback.route_id -> Pcoq.Parsable.t -> unit
type focus = {
  1. start : Stateid.t;
  2. stop : Stateid.t;
  3. tip : Stateid.t;
}
val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ]
val observe : doc:doc -> Stateid.t -> doc
val finish : doc:doc -> doc
val wait : doc:doc -> doc
val stop_worker : string -> unit
val join : doc:doc -> doc
val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> Names.DirPath.t -> string -> doc
val reset_task_queue : unit -> unit
type tasks
val check_task : string -> tasks -> int -> bool
val info_tasks : tasks -> (string * float * int) list
val get_current_state : doc:doc -> Stateid.t
val get_ldir : doc:doc -> Names.DirPath.t
val get_ast : doc:doc -> Stateid.t -> Vernacexpr.vernac_control option
val set_compilation_hints : string -> unit
val set_perspective : doc:doc -> Stateid.t list -> unit

workers **************************************************************** *

document structure customization *************************************** *

type static_block_declaration = {
  1. block_start : Stateid.t;
  2. block_stop : Stateid.t;
  3. dynamic_switch : Stateid.t;
  4. carry_on_data : DynBlockData.t;
}
type document_node = {
  1. indentation : int;
  2. ast : Vernacexpr.vernac_control;
  3. id : Stateid.t;
}
type document_view = {
  1. entry_point : document_node;
  2. prev_node : document_node -> document_node option;
}
type static_block_detection = document_view -> static_block_declaration option
type recovery_action = {
  1. base_state : Stateid.t;
  2. goals_to_admit : Goal.goal list;
  3. recovery_command : Vernacexpr.vernac_control option;
}
type dynamic_block_error_recovery = doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
val register_proof_block_delimiter : Vernacextend.proof_block_name -> static_block_detection -> dynamic_block_error_recovery -> unit

customization ********************************************************** *

val state_computed_hook : (doc:doc -> Stateid.t -> in_cache:bool -> unit) Hook.t
val unreachable_state_hook : (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) Hook.t
val state_ready_hook : (doc:doc -> Stateid.t -> unit) Hook.t
val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t
val document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) Hook.t

User adds a sentence to the document (after parsing)

val document_edit_hook : (Stateid.t -> unit) Hook.t

User edits a sentence in the document

val sentence_exec_hook : (Stateid.t -> unit) Hook.t

User requests evaluation of a sentence

val get_doc : Feedback.doc_id -> doc
val state_of_id : doc:doc -> Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ]
val current_proof_depth : doc:doc -> int
val get_all_proof_names : doc:doc -> Names.Id.t list
val stm_debug : bool Stdlib.ref

Enable STM debugging

type document
val backup : unit -> document
val restore : document -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct