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.17.0.0.17.3.tbz
sha256=bab246d97c66e06f7a65808a24a295bf288a2b7e07cc45ab4a1e8fc24a1ea3f6
sha512=33dfa7cb9857e30861ef4dc6bd1654799e6fd45d53d7ad9f79755920c1961e67f98f650db1e6dc288f0f1fe744fac28878ec03cce062cae78ae64bdd98614991

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