package coq-lsp
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=dd5d0993261d3742e77ccac8344307d97b507b265d8743ae0ce33d0b3fcfd98a
sha512=76727400b27900fdd659af7f03c5f2cd979f50ea0c76ad6f5b5de56a53b9db06dba1e1c786fd3e8ab695e42d94c53d58415c0c5b5eef8192f9863eaf7dcca693
doc/coq-lsp.petanque/Petanque/Agent/index.html
Module Petanque.AgentSource
Protocol notes:
The idea is that the types of the functions here have a direct translation to the JSON-RPC (or any other) protocol.
Thus, types here correspond to types in the wire, except for cases where the protocol layer performs an implicit mapping on types.
So far, the mappings are:
uri<->Doc.tint<->State.t
The State.t mapping is easy to do at the protocol level with a simple mapping, however uri -> Doc.t may need to yield to the document manager to build the corresponding doc. This is very convenient for users, but introduces a little bit more machinery.
We could imagine a future where State.t need to be managed asynchronously, then the same approach that we use for Doc.t could happen.
get_root_state ?opts ~doc return the root state of the document doc.
val get_state_at_pos :
?opts:Run_opts.t ->
doc:Fleche.Doc.t ->
point:(int * int) ->
unit ->
State.t Run_result.t R.tget_state_at_pos ?opts ~doc ~position return the state at position position in doc. Note that LSP positions are zero-based!
val start :
token:Coq.Limits.Token.t ->
doc:Fleche.Doc.t ->
?opts:Run_opts.t ->
?pre_commands:string ->
thm:string ->
unit ->
State.t Run_result.t R.tstart ~token ~doc ~pre_commands ~thm start a new proof for theorem thm in file uri under fn. token can be used to interrupt the computation. Returns the proof state or error otherwise. pre_commands is a string of dot-separated Coq commands that will be executed before the proof starts.
val run :
token:Coq.Limits.Token.t ->
?opts:Run_opts.t ->
st:State.t ->
tac:string ->
unit ->
State.t Run_result.t R.trun ~token ?memo ~st ~tac tries to run tac over state st. memo (by default true) controls whether the command execution will be memoized in Flèche incremental engine.
goals ~token ~st return the list of goals for a given st
Return the list of defined constants and inductives for a given state. For now we just return their fully qualified name, but more options are of course possible.
Petanque version