package coq-core

  1. Overview
  2. Docs
package coq-core
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

    *)
}

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).

type add_focus =
  1. | NewAddTip
  2. | Unfocus of Stateid.t
val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> bool -> Vernacexpr.vernac_control -> doc * Stateid.t * add_focus
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;
}
type edit_focus =
  1. | NewTip
  2. | Focus of focus
val edit_at : doc:doc -> Stateid.t -> doc * edit_focus
val observe : doc:doc -> Stateid.t -> unit
val finish : doc:doc -> Vernacstate.t
val wait : doc:doc -> unit
val stop_worker : string -> unit
val join : doc:doc -> unit
val snapshot_vio : create_vos:bool -> doc:doc -> output_native_objects:bool -> Names.DirPath.t -> string -> unit
val reset_task_queue : unit -> unit
type document
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 : Evar.t list;
  3. recovery_command : Vernacexpr.vernac_control option;
}
type block_classification =
  1. | ValidBlock of recovery_action
  2. | Leaks
type dynamic_block_error_recovery = doc -> static_block_declaration -> block_classification
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) -> unit
val unreachable_state_hook : (doc:doc -> Stateid.t -> Exninfo.iexn -> unit) -> unit
val state_ready_hook : (doc:doc -> Stateid.t -> unit) -> unit
val forward_feedback_hook : (Feedback.feedback -> unit) -> unit
val document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) -> unit

User adds a sentence to the document (after parsing)

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

User edits a sentence in the document

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

User requests evaluation of a sentence

val get_doc : Feedback.doc_id -> doc
type state =
  1. | Valid of Vernacstate.t option
  2. | Expired
  3. | Error of exn
val state_of_id : doc:doc -> Stateid.t -> state
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

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