package coqide-server

  1. Overview
  2. Docs
The Rocq Prover, XML protocol server

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (11)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/coqide-server.protocol/Xmlprotocol/index.html

Module XmlprotocolSource

* Applicative part of the interface of RocqIDE calls to Rocq

Sourcetype 'a call
Sourcetype unknown_call =
  1. | Unknown : 'a call -> unknown_call
Sourceval abstract_eval_call : Interface.handler -> 'a call -> bool * 'a Interface.value

* Protocol version

Sourceval protocol_version : string
Sourcetype msg_format =
  1. | Richpp of {
    1. width : int;
    2. depth : int;
    }
  2. | Ppcmds

By default, we still output messages in Richpp so we are compatible with 8.6, however, 8.7 aware clients will want to set this to Ppcmds

* XML data marshalling

Sourceval of_call : 'a call -> Xml_datatype.xml
Sourceval of_answer : msg_format -> 'a call -> 'a Interface.value -> Xml_datatype.xml
Sourceval to_answer : 'a call -> Xml_datatype.xml -> 'a Interface.value
Sourceval document : (Xml_datatype.xml -> string) -> unit

* Debug printing

Sourceval pr_call : 'a call -> string
Sourceval pr_value : 'a Interface.value -> string
Sourceval pr_full_value : 'a call -> 'a Interface.value -> string
Sourcetype msg_type =
  1. | Feedback
  2. | LtacDebugInfo
  3. | Other

Classification of messages handled by different mechanisms

* Serialization of feedback

Sourceval of_ltac_debug_answer : tag:string -> Pp.t -> Xml_datatype.xml

* Serialization of debugger output

Sourceval to_ltac_debug_answer : Xml_datatype.xml -> string * Pp.t
Sourceval of_vars : (string * Pp.t) list -> Xml_datatype.xml

* reply for db_vars message

Sourceval of_stack : (string * (string * int list) option) list -> Xml_datatype.xml

* reply for db_stack message