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.0.tbz
sha256=fe717f2aa1394434ca3cd9f02a4227e512fb2517c01d4f2726d71f4e3a18756d
sha512=c070d3ebb7f76df7929b04ddb68d4d28751e8991fdb870f56a64168389ff217e75e118317dc8069a8acf98ac88c523d2211fd91fdc777f916d3184b56d235a7c

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