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.18.0.0.18.1.tbz
sha256=3958ec27603e3f927a74f11d02d98390e8ecda942bb23f37ff6fa575b31a8158
sha512=d33f9340de6e1426a42192da3610a7636b0201baa166cf788926b866738ae299219439bc22112cc81591c565dd857f66e53a41a3cfe420844f31fb6077abe57b

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