package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

coq-lsp.coq
- Coq
  - Args
  - Ast
    
    Id
    
    Map
    
    Monad
    
    M
    
    Smart
    
    Set
    
    Meta
    
    Command
    
    Require
  - Compat
    
    Ocaml_414
    
    In_channel
    
    Out_channel
    
    Result
    
    O
  - Files
  - Glob
    
    Info
  - Goals
  - Init
  - Interp
    
    Require
  - Library_file
    
    Entry
  - Limits
    
    Coq
    
    Token
    
    Intf
    
    Token
    
    Mp
    
    Token
    
    Token
  - Limits_mp_impl
    
    Token
  - Loader
  - Message
  - Parsing
    
    Parsable
  - Print
  - Protect
    
    E
    
    O
    
    Error
    
    R
  - Save
  - State
    
    Proof
  - Utils
  - Workspace
    
    CmdLine
    
    Flags
    
    Require
    
    Warning
coq-lsp.fleche
- Fleche
  - Config
    
    Unicode_completion
  - Contents
    
    R
  - Debug
  - Doc
    
    Completion
    
    Env
    
    Node
    
    Ast
    
    Info
    
    Message
    
    Target
  - Info
    
    Completion
    
    Goals
    
    LC
    
    LineCol
    
    O
    
    Offset
    
    Point
    
    S
    
    P
  - Io
    
    CallBack
    
    Level
    
    Log
    
    Report
  - Memo
    
    Admit
    
    GlobalCacheStats
    
    Init
    
    Interp
    
    Require
    
    S
    
    Stats
  - Perf
    
    Info
    
    Sentence
  - Perf_analysis
  - Progress
    
    Info
  - ServerInfo
    
    Status
    
    Version
  - Stats
    
    Global
    
    Kind
  - Theory
    
    Check
    
    Register
    
    Completed
    
    InjectRequire
    
    Request
  - Version
coq-lsp.fleche.waterproof
- Fleche_waterproof
  - Json
    
    CAst
  - Ljson
  - Tjson
coq-lsp.lang
- Lang
  - Ast
    
    Info
    
    Name
  - Diagnostic
    
    Data
    
    Severity
  - LUri
    
    File
  - Point
  - Range
  - Utf
    
    Encoding
  - With_range
coq-lsp.lsp
- Lsp
coq-lsp.petanque
- Petanque
  - Agent
    
    Env
    
    Error
    
    Premise
    
    R
    
    Run_result
    
    State
coq-lsp.petanque.json
- Petanque_json
  - Client
    
    Chans
    
    S
    
    C
  - Interp
  - JAgent
    
    Env
    
    Error
    
    Goals
    
    Lang
    
    Range
    
    Premise
    
    R
    
    Run_result
    
    State
    
    Stdlib
    
    Result
  - Obj_map
    
    Make
    
    O
    
    Obj
    
    S
  - Protocol
    
    Goals
    
    Handler
    
    Params
    
    Params
    
    Response
    
    Handler
    
    Params
    
    Response
    
    Init
    
    Handler
    
    Response
    
    Params
    
    Response
    
    Message
    
    Params
    
    Notification
    
    S
    
    Params
    
    Premises
    
    Handler
    
    Params
    
    Params
    
    Response
    
    Request
    
    S
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    RunTac
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    Start
    
    Handler
    
    Params
    
    Response
    
    Params
    
    Response
    
    Trace
    
    Params
  - Utils
coq-lsp.plugin.astdump
- Astdump_plugin
  - Main
coq-lsp.plugin.example
- Example_plugin
  - Main
coq-lsp.plugin.goaldump
- Goaldumpl_plugin
  - Main
coq-lsp.plugin.save_vo
- Savevo_plugin
  - Main

Legend:
Library
Module
Module type
Parameter
Class
Class type

module Error : sig ... end

This modules reifies Coq side effects into an algebraic structure.

module R : sig ... end

This "monad" could be related to "Runners in action" (Ahman, Bauer), thanks to Guillaume Munch-Maccagnoni for the reference and for many useful tips!

module E : sig ... end

val fb_queue : Loc.t Message.t list ref

Must be hooked to allow Protect to capture the feedback.

val eval : token:Limits.Token.t -> f:('i -> 'o) -> 'i -> ('o, Loc.t) E.t

Eval a function and reify the exceptions. Note f _must_ be pure, as in case of anomaly f may be re-executed with debug options. Beware, not thread-safe! token Does allow to interrupt the evaluation.