package coq-serapi

  1. Overview
  2. Docs
Serialization library and protocol for machine interaction with the Coq proof assistant

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (38)

Authors

  1. E
    Emilio Jesús Gallego Arias
  2. K
    Karl Palmskog
  3. C
    Clément Pit-Claudel
  4. K
    Kaiyu Yang

Maintainers

  1. E
    e@x80.org

Sources

coq-serapi-8.16.0.0.16.3.tbz
sha256=66137df53e01398a26e9e51056af7439997bcf562fbe4503946fe89e0c5df443
sha512=5c71f7acd4537c33853122d9c526e61f35d2934504c77ce95196f8d595f1c619a680fccd46ba9deb69b509eeb936984056380b18b65fae617ae1cce704df90a1

doc/coq-serapi.sertop_v8_12/Sertop/Sertop_init/index.html

Module Sertop.Sertop_initSource

Sourcetype async_flags = {
  1. enable_async : string option;
  2. deep_edits : bool;
  3. async_workers : int;
  4. error_recovery : bool;
}

SerAPI flags for asynchronous processing

Sourceval process_stm_flags : async_flags -> Stm.AsyncOpts.stm_opt

process_stm_flags flags transforms SerAPI flags into Coq flags

Sourcetype coq_opts = {
  1. fb_handler : Format.formatter -> Feedback.feedback -> unit;
    (*

    callback to handle async feedback

    *)
  2. plugin_load : (string list -> unit) option;
    (*

    callback to load findlib plugins

    *)
  3. debug : bool;
    (*

    Enable Coq Debug mode

    *)
  4. set_impredicative_set : bool;
    (*

    Enable -impredicative-set option in Coq (default=false)

    *)
  5. allow_sprop : bool;
    (*

    allow using the proof irrelevant SProp sort (default=true)

    *)
  6. indices_matter : bool;
    (*

    Levels of indices (and nonuniform parameters) contribute to the level of inductives

    *)
  7. ml_path : string list;
  8. vo_path : Loadpath.vo_path list;
    (*

    From -R and -Q options usually

    *)
}
Sourceval coq_init : coq_opts -> Format.formatter -> unit

coq_init opts Initialize Coq. This doesn't create a Proof Document.

Sourceval update_fb_handler : pp_feed:(Format.formatter -> Feedback.feedback -> unit) -> Format.formatter -> unit