package coq-lsp

You can search for identifiers within the package.

in-package search v0.2.0

Language Server Protocol native server for Coq

Install

sha256=36340f464107ac60bb4033fad249984690cdcce3a6bef4ca439ffb2a4458dbf9

sha512=4866f4c2f0acda0c114e27b32cd60fa054333e1c7249227b8c3b23a316d7f306676203bd317f135a40368a292b7b49b76f0bdacff21d7e9bfb5a422d1c8d6ad8

Flèche memo / cache tables, with some advanced features

type input

type output

For now, to generalize later if needed

val eval : token:Coq.Limits.Token.t -> input -> (output, Loc.t) Coq.Protect.E.t

eval i Eval an input i

val evalS : 
  token:Coq.Limits.Token.t ->
  input ->
  (output, Loc.t) Coq.Protect.E.t * Stats.t

eval i Eval an input i and produce stats

val size : unit -> int

size () Return the cache size in words, expensive

val all_freqs : unit -> int list

freqs (): (sorted) histogram

val stats : unit -> Hashtbl.statistics

stats (): hashtbl stats

val input_info : input -> string

debug data for input

val clear : unit -> unit

clears the cache