package coq

  1. Overview
  2. Docs
Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

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

Module InterfaceSource

* Declarative part of the interface of CoqIDE calls to Coq

* Generic structures

Sourcetype raw = bool
Sourcetype verbose = bool
Sourcetype goal = {
  1. goal_id : string;
    (*

    Unique goal identifier

    *)
  2. goal_hyp : Pp.t list;
    (*

    List of hypotheses

    *)
  3. goal_ccl : Pp.t;
    (*

    Goal conclusion

    *)
  4. goal_name : string option;
    (*

    User-level goal name

    *)
}

The type of coqtop goals

Sourcetype evar = {
  1. evar_info : string;
    (*

    A string describing an evar: type, number, environment

    *)
}
Sourcetype status = {
  1. status_path : string list;
    (*

    Module path of the current proof

    *)
  2. status_proofname : string option;
    (*

    Current proof name. None if no focused proof is in progress

    *)
  3. status_allproofs : string list;
    (*

    List of all pending proofs. Order is not significant

    *)
  4. status_proofnum : int;
    (*

    An id describing the state of the current proof.

    *)
}
Sourcetype 'a pre_goals = {
  1. fg_goals : 'a list;
    (*

    List of the focused goals

    *)
  2. bg_goals : ('a list * 'a list) list;
    (*

    Zipper representing the unfocused background goals

    *)
  3. shelved_goals : 'a list;
    (*

    List of the goals on the shelf.

    *)
  4. given_up_goals : 'a list;
    (*

    List of the goals that have been given up

    *)
}
Sourcetype goals = goal pre_goals
Sourcetype hint = (string * string) list

A list of tactics applicable and their appearance

Sourcetype option_name = string list
Sourcetype option_value =
  1. | BoolValue of bool
  2. | IntValue of int option
  3. | StringValue of string
  4. | StringOptValue of string option
Sourcetype option_state = {
  1. opt_sync : bool;
    (*

    Whether an option is synchronous

    *)
  2. opt_depr : bool;
    (*

    Whether an option is deprecated

    *)
  3. opt_value : option_value;
    (*

    The current value of the option

    *)
}

Summary of an option status

Sourcetype search_constraint =
  1. | Name_Pattern of string
    (*

    Whether the name satisfies a regexp (uses Ocaml Str syntax)

    *)
  2. | Type_Pattern of string
    (*

    Whether the object type satisfies a pattern

    *)
  3. | SubType_Pattern of string
    (*

    Whether some subtype of object type satisfies a pattern

    *)
  4. | In_Module of string list
    (*

    Whether the object pertains to a module

    *)
  5. | Include_Blacklist
    (*

    Bypass the Search blacklist

    *)
Sourcetype search_flags = (search_constraint * bool) list

A list of search constraints; the boolean flag is set to false whenever the flag should be negated.

Sourcetype 'a coq_object = {
  1. coq_object_prefix : string list;
  2. coq_object_qualid : string list;
  3. coq_object_object : 'a;
}

A named object in Coq. coq_object_qualid is the shortest path defined for the user. coq_object_prefix is the missing part to recover the fully qualified name, i.e fully_qualified = coq_object_prefix + coq_object_qualid. coq_object_object is the actual content of the object.

Sourcetype coq_info = {
  1. coqtop_version : string;
  2. protocol_version : string;
  3. release_date : string;
  4. compile_date : string;
}
Sourcetype db_continue_opt =
  1. | StepIn
  2. | StepOver
  3. | StepOut
  4. | Continue
  5. | Interrupt

Calls result

Sourcetype location = (int * int) option
Sourcetype state_id = Stateid.t
Sourcetype route_id = Feedback.route_id
Sourcetype edit_id = int
Sourcetype 'a value =
  1. | Good of 'a
  2. | Fail of state_id * location * Pp.t
Sourcetype ('a, 'b) union = ('a, 'b) Util.union
Sourcetype add_sty = (((string * edit_id) * (state_id * verbose)) * int) * (int * int)

add ((((s,eid),(sid,v)), bp), (line_nb, bol_pos) adds the phrase s with edit id eid on top of the current edit position (that is asserted to be sid). v set to true indicates "verbose". The response (id,rc) is the new state id assigned to the phrase. rc is Inl if the new state id is the tip of the edit point, or Inr tip if the new phrase closes a focus and tip is the new edit tip. bp, line_nb and bol_pos are the Loc.t values for the phrase in the buffer, needed to return the correct location for s to the debugger

Sourcetype add_rty = state_id * (unit, state_id) union
Sourcetype edit_at_sty = state_id

edit_at id declares the user wants to edit just after id. The response is Inl if the document has been rewound to that point, Inr (start,(stop,tip)) if id is in a zone that can be focused. In that case the zone is delimited by start and stop while tip is the new document tip. Edits made by subsequent add are always performed on top of id.

Sourcetype edit_at_rty = (unit, state_id * (state_id * state_id)) union
Sourcetype query_sty = route_id * (string * state_id)

query s id executes s at state id.

query used to reply with the contents of Coq's console output, and has been deprecated in favor of sending the query answers as feedback. It will be removed in a future version of the protocol.

Sourcetype query_rty = unit
Sourcetype goals_sty = unit

Fetching the list of current goals. Return None if no proof is in progress, Some gl otherwise.

Sourcetype goals_rty = goals option
Sourcetype evars_sty = unit

Retrieve the list of uninstantiated evars in the current proof. None if no proof is in progress.

Sourcetype evars_rty = evar list option
Sourcetype hints_sty = unit

Retrieving the tactics applicable to the current goal. None if there is no proof in progress.

Sourcetype hints_rty = (hint list * hint) option
Sourcetype status_sty = bool

The status, for instance "Ready in SomeSection, proving Foo", the input boolean (if true) forces the evaluation of all unevaluated statements

Sourcetype status_rty = status
Sourcetype search_sty = search_flags

Search for objects satisfying the given search flags.

Sourcetype search_rty = string coq_object list
Sourcetype proof_diff_sty = string * Stateid.t

Diffs between the proof term at a given stateid and the previous one

Sourcetype proof_diff_rty = Pp.t
Sourcetype db_cmd_sty = string

A debugger command

Sourcetype db_cmd_rty = unit
Sourcetype db_upd_bpts_sty = ((string * int) * bool) list

update one or more breakpoints in the specified file

Sourcetype db_upd_bpts_rty = unit
Sourcetype db_continue_sty = db_continue_opt

continue execution (in various ways)

Sourcetype db_continue_rty = unit
Sourcetype db_stack_sty = unit

fetch the stack

Sourcetype db_stack_rty = (string * (string * int list) option) list
Sourcetype db_vars_sty = int

fetch variable names and values for a stack frame

Sourcetype db_vars_rty = (string * Pp.t) list
Sourcetype db_configd_sty = unit

indicate debugger config is complete

Sourcetype db_configd_rty = unit
Sourcetype get_options_sty = unit

Retrieve the list of options of the current toplevel

Sourcetype get_options_rty = (option_name * option_state) list
Sourcetype set_options_sty = (option_name * option_value) list

Set the options to the given values. Warning: this is not atomic, so whenever the call fails, the option state can be messed up... This is the caller duty to check that everything is correct.

Sourcetype set_options_rty = unit
Sourcetype mkcases_sty = string

Create a "match" template for a given inductive type. For each branch of the match, we list the constructor name followed by enough pattern variables.

Sourcetype mkcases_rty = string list list
Sourcetype quit_sty = unit

Quit gracefully the interpreter.

Sourcetype quit_rty = unit
Sourcetype init_sty = string option
Sourcetype init_rty = state_id
Sourcetype about_sty = unit
Sourcetype about_rty = coq_info
Sourcetype handle_exn_sty = Exninfo.iexn
Sourcetype handle_exn_rty = state_id * location * Pp.t
Sourcetype interp_sty = (raw * verbose) * string
Sourcetype interp_rty = state_id * (string, string) Util.union
Sourcetype stop_worker_sty = string
Sourcetype stop_worker_rty = unit
Sourcetype print_ast_sty = state_id
Sourcetype print_ast_rty = Xml_datatype.xml
Sourcetype annotate_sty = string
Sourcetype annotate_rty = Xml_datatype.xml
Sourcetype wait_sty = unit
Sourcetype wait_rty = unit
Sourcetype handler = {
  1. add : add_sty -> add_rty;
  2. edit_at : edit_at_sty -> edit_at_rty;
  3. query : query_sty -> query_rty;
  4. goals : goals_sty -> goals_rty;
  5. evars : evars_sty -> evars_rty;
  6. hints : hints_sty -> hints_rty;
  7. status : status_sty -> status_rty;
  8. search : search_sty -> search_rty;
  9. get_options : get_options_sty -> get_options_rty;
  10. set_options : set_options_sty -> set_options_rty;
  11. mkcases : mkcases_sty -> mkcases_rty;
  12. about : about_sty -> about_rty;
  13. stop_worker : stop_worker_sty -> stop_worker_rty;
  14. print_ast : print_ast_sty -> print_ast_rty;
  15. annotate : annotate_sty -> annotate_rty;
  16. proof_diff : proof_diff_sty -> proof_diff_rty;
  17. db_cmd : db_cmd_sty -> db_cmd_rty;
  18. db_upd_bpts : db_upd_bpts_sty -> db_upd_bpts_rty;
  19. db_continue : db_continue_sty -> db_continue_rty;
  20. db_stack : db_stack_sty -> db_stack_rty;
  21. db_vars : db_vars_sty -> db_vars_rty;
  22. db_configd : db_configd_sty -> db_configd_rty;
  23. handle_exn : handle_exn_sty -> handle_exn_rty;
  24. init : init_sty -> init_rty;
  25. quit : quit_sty -> quit_rty;
  26. wait : wait_sty -> wait_rty;
  27. interp : interp_sty -> interp_rty;
}
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