package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (36)

Authors

  1. E
    Emilio Jesús Gallego Arias <e@x80.org>
  2. A
    Ali Caglayan <alizter@gmail.com>
  3. S
    Shachar Itzhaky <shachari@cs.technion.ac.il>
  4. R
    Ramkumar Ramachandra <r@artagnon.com>

Maintainers

  1. E
    e@x80.org

Sources

coq-lsp-0.2.5+9.1.tbz
sha256=488520e2720cd0601a623be39ff87223d81ca1d2f81c77641f803fda21f3717e
sha512=146e43a6a9c516f4e7fe143d4fdf3e1e7ecdcd73ea5cc3e09b2886f68aa05210c016e905bf1596341faa0b55709ad530ef86212c92790b6dce6050a0a00e3325

doc/coq-lsp.petanque/Petanque/Agent/index.html

Module Petanque.AgentSource

Sourcemodule State : sig ... end

Petanque.Agent

Sourcemodule Error : sig ... end

Petanque errors

Sourcemodule R : sig ... end

Petanque results

Sourcemodule Run_opts : sig ... end
Sourcemodule Run_result : sig ... end

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.t
  • int <-> 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.

Sourceval get_root_state : ?opts:Run_opts.t -> doc:Fleche.Doc.t -> unit -> State.t Run_result.t R.t

get_root_state ?opts ~doc return the root state of the document doc.

Sourceval get_state_at_pos : ?opts:Run_opts.t -> doc:Fleche.Doc.t -> point:(int * int) -> unit -> State.t Run_result.t R.t

get_state_at_pos ?opts ~doc ~position return the state at position position in doc. Note that LSP positions are zero-based!

Sourceval 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.t

start ~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.

Sourceval run : token:Coq.Limits.Token.t -> ?opts:Run_opts.t -> st:State.t -> tac:string -> unit -> State.t Run_result.t R.t

run ~token ?opts ~st ~tac tries to run tac over state st. opts controls several parameters of the Fleche execution engine.

Sourceval run_at_pos : token:Coq.Limits.Token.t -> ?opts:Run_opts.t -> doc:Fleche.Doc.t -> point:(int * int) -> command:string -> unit -> unit Run_result.t R.t

run_at_pos ~token ?opts ~doc ~command tries to run command at doc position point. opts controls several parameters of the Fleche execution engine.

Sourcemodule Goal_opts : sig ... end
Sourceval goals : token:Coq.Limits.Token.t -> st:State.t -> ?opts:Goal_opts.t -> unit -> (string, string) Coq.Goals.reified option R.t

goals ~token ~st return the list of goals for a given st

Sourcemodule Premise : sig ... end
Sourceval premises : token:Coq.Limits.Token.t -> st:State.t -> Premise.t list R.t

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.

Sourceval list_notations_in_statement : token:Coq.Limits.Token.t -> st:State.t -> statement:string -> unit -> Coq.Notation_analysis.Info.t list Run_result.t R.t

List all notations present is some lemma statement statement, parsed at state st. Returns [] on EOF.

Sourceval ast : token:Coq.Limits.Token.t -> st:State.t -> text:string -> unit -> Coq.Ast.t option Run_result.t R.t

Return the ast of a string text, parsed at state st . Returns None on EOF

Sourceval ast_at_pos : doc:Fleche.Doc.t -> point:(int * int) -> unit -> Coq.Ast.t option R.t

Return the ast of a position in the document doc at position point. Will error if there is no node, will return None, when there is a node at the position, but the ast is not available, for example due to parsing error

Sourcemodule Proof_info : sig ... end
Sourceval proof_info : token:Coq.Limits.Token.t -> st:State.t -> unit -> Proof_info.t option R.t

Returns the proof name for a given st, if a proof is open. If no proof is open, returns None.

Sourceval proof_info_at_pos : token:Coq.Limits.Token.t -> doc:Fleche.Doc.t -> point:(int * int) -> unit -> Proof_info.t option R.t

Returns the proof name for a given point, in document doc if a proof is open. If no proof is open, returns None.

Sourceval version : int

Petanque version