package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type level =
  1. | Debug
  2. | Info
  3. | Notice
  4. | Warning
  5. | Error
type doc_id = int

Document unique identifier for serialization

type route_id = int

Coq "semantic" infos obtained during execution

val default_route : route_id
type feedback_content =
  1. | Processed
  2. | Incomplete
  3. | Complete
  4. | ProcessingIn of string
  5. | InProgress of int
  6. | WorkerStatus of string * string
  7. | AddedAxiom
  8. | GlobRef of Loc.t * string * string * string * string
  9. | GlobDef of Loc.t * string * string * string
  10. | FileDependency of string option * string
  11. | FileLoaded of string * string
  12. | Custom of Loc.t option * string * Xml_datatype.xml
  13. | Message of level * Loc.t option * Pp.t
type feedback = {
  1. doc_id : doc_id;
  2. span_id : Stateid.t;
  3. route : route_id;
  4. contents : feedback_content;
}
Feedback sent, even asynchronously, to the user interface
val add_feeder : (feedback -> unit) -> int

add_feeder f adds a feeder listiner f, returning its id

val del_feeder : int -> unit

del_feeder fid removes the feeder with id fid

val feedback : ?did:doc_id -> ?id:Stateid.t -> ?route:route_id -> feedback_content -> unit

feedback ?did ?sid ?route fb produces feedback fb, with route and did, sid set appropiatedly, if absent, it will use the defaults set by set_id_for_feedback

val set_id_for_feedback : ?route:route_id -> doc_id -> Stateid.t -> unit

set_id_for_feedback route id Set the defaults for feedback

output functions
val msg_info : ?loc:Loc.t -> Pp.t -> unit

Message that displays information, usually in verbose mode, such as Foobar is defined

val msg_notice : ?loc:Loc.t -> Pp.t -> unit

Message that should be displayed, such as Print Foo or Show Bar.

val msg_warning : ?loc:Loc.t -> Pp.t -> unit

Message indicating that something went wrong, but without serious consequences.

val msg_debug : ?loc:Loc.t -> Pp.t -> unit

For debugging purposes

val console_feedback_listener : Stdlib.Format.formatter -> feedback -> unit

Helper for tools willing to print to the feedback system

val warn_no_listeners : bool Stdlib.ref

The library will print a warning to the console if no listener is available by default; ML-clients willing to use Coq without a feedback handler should set this to false.

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