this repo has no description

[new release] coq-lsp (0.2.0+8.17)

CHANGES:

-----------------------------------

- [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
dependency, and will greatly easy the development of tools that
require AST manipulation (@ejgallego, ejgallego/coq-lsp#698)
- [fleche] Remove 8.16 compatibility layer (@ejgallego, ejgallego/coq-lsp#747)
- [fleche] Preserve view hint across document changes. With this
change, we get local continuous checking mode when the view-port
heuristic is enabled (@ejgallego, ejgallego/coq-lsp#748)
- [memo] More precise hashing for Coq states, this improves cache
performance quite a bit (@ejgallego, ejgallego/coq-lsp#751)
- [fleche] Enable sharing of `.vo` file parsing. This enables better
sharing, achieving an almost 50% memory reduction for example when
opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh,
ejgallego/coq-lsp#744)
- [memo] Provide API to query Hashtbl stats (@ejgallego, ejgallego/coq-lsp#753)
- [nix] Add `pet-server` deps to flake.nix (Léo Stefanesco, ejgallego/coq-lsp#754)
- [coq-lsp] Fix crash on `--help` option (Léo Stefanesco, @ejgallego,
ejgallego/coq-lsp#754)
- [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
ejgallego/coq-lsp#755, cc: ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
- [hover] Show input howto for unicode characters on hover
(@ejgallego, Léo Stefanesco, ejgallego/coq-lsp#756)
- [lsp] [definition] Support for jump to definition across workspace
files. The location information is obtained from `.glob` files, so
it is often not perfect. (@ejgallego, ejgallego/coq-lsp#762, fixes ejgallego/coq-lsp#317)
- [lsp] [hover] Show full name and provenance of identifiers
(@ejgallego, ejgallego/coq-lsp#762)
- [lsp] [definition] Try also to resolve and locate module imports
(@ejgallego, ejgallego/coq-lsp#764)
- [code] Don't start server on extension activation, unless an editor
we own is active. We also auto-start the server if a document that
we own is opened later (@ejgallego, ejgallego/coq-lsp#758, fixes ejgallego/coq-lsp#750)
- [petanque] Allow `init` to be called multiple times (@ejgallego,
@gbdrt, ejgallego/coq-lsp#766)
- [petanque] Faster query for goals status after `run_tac`
(@ejgallego, ejgallego/coq-lsp#768)
- [petanque] New parameter `pre_commands` to `start` which allows
instrumenting the goal before starting the proof (@ejgallego, Alex
Sanchez-Stern ejgallego/coq-lsp#769)
- [petanque] New `http_headers={yes,no}` parameter for `pet` json
shell, plus some improvements on protocol handling (@ejgallego,
ejgallego/coq-lsp#770)
- [petanque] Make agent agnostic of environment, allowing embedding
inside LSP (@ejgallego, ejgallego/coq-lsp#771)
- [diagnostics] Ensure extra diagnostics info is present in all
errors, not only on those sentences that did parse successfully
(@ejgallego, Diego Rivera, ejgallego/coq-lsp#772)
- [hover] New option `show_universes_on_hover` that will display
universe data on hover (@ejgallego, @SkySkimmer, ejgallego/coq-lsp#666)
- [hover] New plugin `unidiff` that will elaborate a summary of
universe data a file, in particular regarding universes added at
`Qed` time (@ejgallego, ejgallego/coq-lsp#773)
- [fleche] Support meta-command `Abort All` (@ejgallego, ejgallego/coq-lsp#774, fixes
ejgallego/coq-lsp#550)
- [petanque] Allow memoization control on `petanque/run` via a new
parameter `memo` (@ejgallego, ejgallego/coq-lsp#780)
- [lsp] [petanque] Allow acces to `petanque` protocol from the lsp
server (@ejgallego, ejgallego/coq-lsp#778)
- [petanque] Always initialize a workspace. This made `pet` crash if
`--root` was not used and client didn't issue the optimal
`setWorkspace` call (ejgallego/coq-lsp#782, @ejgallego, @gbdrt)
- [lsp] [petanque] New methods `state/eq` and `state/hash`; this
allows clients to implement a client-side hash; equality is
configurable with different methods; moreover, `petanque/run` can
compute some extra data like state hashing without a round-trip
(@ejgallego @gbdrt, ejgallego/coq-lsp#779)
- [petanque] New methods to hash proof states; use proof state hash
by default in petanque agent (@ejgallego, @gbdrt, ejgallego/coq-lsp#808)
- [petanque] New shell method `petanque/toc` that returns a document
outline in LSP-style (@ejgallego, ejgallego/coq-lsp#794)

Changed files
+73
packages
coq-lsp
coq-lsp.0.2.0+8.17
+73
packages/coq-lsp/coq-lsp.0.2.0+8.17/opam
···
+
synopsis: "Language Server Protocol native server for Coq"
+
description:
+
"""
+
Language Server Protocol native server for Coq
+
"""
+
opam-version: "2.0"
+
maintainer: "e@x80.org"
+
bug-reports: "https://github.com/ejgallego/coq-lsp/issues"
+
homepage: "https://github.com/ejgallego/coq-lsp"
+
dev-repo: "git+https://github.com/ejgallego/coq-lsp.git"
+
authors: [
+
"Emilio Jesús Gallego Arias <e@x80.org>"
+
"Ali Caglayan <alizter@gmail.com>"
+
"Shachar Itzhaky <shachari@cs.technion.ac.il>"
+
"Ramkumar Ramachandra <r@artagnon.com>"
+
]
+
license: "LGPL-2.1-or-later"
+
doc: "https://ejgallego.github.io/coq-lsp/"
+
+
depends: [
+
+
("ocaml" {>= "5.0"} | ("ocaml" {<= "5.0"} & "memprof-limits" { >= "0.2.1" } ))
+
+
"dune" { >= "3.2.0" }
+
+
# lsp dependencies
+
"cmdliner" { >= "1.1.0" }
+
"yojson" { >= "1.7.0" }
+
"uri" { >= "4.2.0" }
+
"dune-build-info" { >= "3.2.0" }
+
+
# waterproof parser
+
"menhir" { >= "20220210" }
+
+
# unit testing
+
"ppx_inline_test" { >= "0.14.1" }
+
+
# Uncomment this for releases
+
"coq" { >= "8.17" < "8.18" }
+
+
# coq deps: remove this for releases
+
"ocamlfind" {>= "1.8.1"}
+
"zarith" {>= "1.11"}
+
+
# result dep, fixed in main, but kept for older releases
+
"result" { >= "1.5" }
+
+
# serlib deps: see what we need to keep for release
+
"ppx_deriving" { >= "4.2.1" }
+
"ppx_deriving_yojson" { >= "3.4" }
+
"ppx_import" { >= "1.11.0" }
+
"sexplib" { >= "v0.13.0" & < "v0.18" }
+
"ppx_sexp_conv" { >= "v0.13.0" & < "v0.18" }
+
"ppx_compare" { >= "v0.13.0" & < "v0.18" }
+
"ppx_hash" { >= "v0.13.0" & < "v0.18" }
+
]
+
+
depopts: ["lwt" "logs"]
+
+
build: [
+
[ "rm" "-rf" "vendor" ]
+
[ "dune" "build" "-p" name "-j" jobs ]
+
]
+
run-test: [ [ "dune" "runtest" "-p" name "-j" jobs ] ]
+
url {
+
src:
+
"https://github.com/ejgallego/coq-lsp/releases/download/0.2.0%2B8.17/coq-lsp-0.2.0.8.17.tbz"
+
checksum: [
+
"sha256=36340f464107ac60bb4033fad249984690cdcce3a6bef4ca439ffb2a4458dbf9"
+
"sha512=4866f4c2f0acda0c114e27b32cd60fa054333e1c7249227b8c3b23a316d7f306676203bd317f135a40368a292b7b49b76f0bdacff21d7e9bfb5a422d1c8d6ad8"
+
]
+
}
+
x-commit-hash: "fb09ea31c79b8a175ab01675580df8e1e6af3887"