package coqide-server
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/coqide-server.protocol/Interface/index.html
Module Interface
* Declarative part of the interface of RocqIDE calls to Rocq
* Generic structures
type goal = {goal_id : string;(*Unique goal identifier
*)goal_hyp : Pp.t list;(*List of hypotheses
*)goal_ccl : Pp.t;(*Goal conclusion
*)goal_name : string option;(*User-level goal name
*)
}The type of rocqtop goals
type status = {status_path : string list;(*Module path of the current proof
*)status_proofname : string option;(*Current proof name.
*)Noneif no focused proof is in progressstatus_allproofs : string list;(*List of all pending proofs. Order is not significant
*)status_proofnum : int;(*An id describing the state of the current proof.
*)
}type option_state = {opt_sync : bool;(*Whether an option is synchronous
*)opt_depr : bool;(*Whether an option is deprecated
*)opt_value : option_value;(*The current value of the option
*)
}Summary of an option status
type search_constraint = | Name_Pattern of string(*Whether the name satisfies a regexp (uses Ocaml Str syntax)
*)| Type_Pattern of string(*Whether the object type satisfies a pattern
*)| SubType_Pattern of string(*Whether some subtype of object type satisfies a pattern
*)| In_Module of string list(*Whether the object pertains to a module
*)| Include_Blacklist(*Bypass the Search blacklist
*)
type search_flags = (search_constraint * bool) listA list of search constraints; the boolean flag is set to false whenever the flag should be negated.
A named object in Rocq. 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.
Calls result
type location = Loc.t optiontype state_id = Stateid.ttype route_id = Feedback.route_idtype ('a, 'b) union = ('a, 'b) Util.unionadd ((((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
type edit_at_sty = state_idedit_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.
query s id executes s at state id.
query used to reply with the contents of Rocq'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.
Fetching the list of current goals. Return None if no proof is in progress, Some gl otherwise.
type goals_rty = goals optiontype subgoals_sty = goal_flagsSame as above, but specific kind of goals can be retrieved by setting the flags.
type subgoals_rty = goals optionRetrieve the list of uninstantiated evars in the current proof. None if no proof is in progress.
type evars_rty = evar list optionRetrieving the tactics applicable to the current goal. None if there is no proof in progress.
The status, for instance "Ready in SomeSection, proving Foo", the input boolean (if true) forces the evaluation of all unevaluated statements
type status_rty = statustype search_sty = search_flagsSearch for objects satisfying the given search flags.
type search_rty = string coq_object listtype proof_diff_sty = string * Stateid.tDiffs between the proof term at a given stateid and the previous one
type proof_diff_rty = Pp.tupdate one or more breakpoints in the specified file
type db_continue_sty = db_continue_optcontinue execution (in various ways)
type db_vars_rty = (string * Pp.t) listtype get_options_rty = (option_name * option_state) listtype set_options_sty = (option_name * option_value) listSet 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.
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.
type init_rty = state_idtype about_rty = coq_infotype interp_rty = state_id * (string, string) Util.uniontype print_ast_sty = state_idtype print_ast_rty = Xml_datatype.xmltype annotate_rty = Xml_datatype.xmltype handler = {add : add_sty -> add_rty;edit_at : edit_at_sty -> edit_at_rty;query : query_sty -> query_rty;goals : goals_sty -> goals_rty;evars : evars_sty -> evars_rty;hints : hints_sty -> hints_rty;status : status_sty -> status_rty;search : search_sty -> search_rty;get_options : get_options_sty -> get_options_rty;set_options : set_options_sty -> set_options_rty;mkcases : mkcases_sty -> mkcases_rty;about : about_sty -> about_rty;stop_worker : stop_worker_sty -> stop_worker_rty;print_ast : print_ast_sty -> print_ast_rty;annotate : annotate_sty -> annotate_rty;proof_diff : proof_diff_sty -> proof_diff_rty;db_cmd : db_cmd_sty -> db_cmd_rty;db_upd_bpts : db_upd_bpts_sty -> db_upd_bpts_rty;db_continue : db_continue_sty -> db_continue_rty;db_stack : db_stack_sty -> db_stack_rty;db_vars : db_vars_sty -> db_vars_rty;db_configd : db_configd_sty -> db_configd_rty;handle_exn : handle_exn_sty -> handle_exn_rty;init : init_sty -> init_rty;quit : quit_sty -> quit_rty;wait : wait_sty -> wait_rty;interp : interp_sty -> interp_rty;subgoals : subgoals_sty -> subgoals_rty;
}