[new release] coq-lsp (0.1.7+8.16)

CHANGES:

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

 - New command line compiler `fcc`. `fcc` allows to access most
   features of `coq-lsp` without the need for a command line client,
   and it has been designed to be extensible and machine-friendly
   (@ejgallego, ejgallego/rocq-lsp#507, fixes ejgallego/rocq-lsp#472)
 - Enable web extension support. For now this will not try to start
   the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/rocq-lsp#430, fixes
   ejgallego/rocq-lsp#234)
 - Improvements and clenaups on hover display, in particular we don't
   print repeated `Notation` strings (@ejgallego, ejgallego/rocq-lsp#422)
 - Don't fail on missing serlib plugins, they are indeed an
   optimization; this mostly impacts 8.16 by lowering the SerAPI
   requirements (@ejgallego, ejgallego/rocq-lsp#421)
 - Fix bug that prevented "Goal after tactic" from working properly
   (@ejgallego, ejgallego/rocq-lsp#438, reported by David Ilcinkas)
 - Fix "Error message browser becomes non-visible when there are many
   goals" by using a fixed-position separated error display (@TDiazT,
   ejgallego/rocq-lsp#445, fixes ejgallego/rocq-lsp#441)
 - Message about workspace detection was printing the wrong file,
   (@ejgallego, ejgallego/rocq-lsp#444, reported by Alex Sanchez-Stern)
 - Display the list of pending obligations in info panel (@ejgallego,
   ejgallego/rocq-lsp#262)
 - Preliminary support to display document performance data in panel
   (@ejgallego, ejgallego/rocq-lsp#181)
 - Fix cases when workspace / root URIs are `null`, as per LSP spec,
   (ejgallego/rocq-lsp#453 , reported by orilahav, fixes ejgallego/rocq-lsp#283)
 - Pass implicit argument information to hover printer (@ejgallego, ejgallego/rocq-lsp#453,
   fixes ejgallego/rocq-lsp#448)
 - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/rocq-lsp#460)
 - Alert when `rootPath` is relative (ejgallego/rocq-lsp#465, @ejgallego, report by Alex
   Sanchez-Stern)
 - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/rocq-lsp#469)
 - `proof/goals` request now takes an optional formatting parameter
   so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/rocq-lsp#470)
 - New command line argument `--idle-delay=$secs` that controls how
   much an idle server will sleep before going back to request
   processing. Default setting is `0.1`, using more aggressive
   settings like `0.01` can decrease latency of requests by ~4x
   (@ejgallego, @HazardousPeach, ejgallego/rocq-lsp#467, ejgallego/rocq-lsp#471)
 - Warnings from `_CoqProject` files are now applied (@ejgallego,
   reported by @arthuraa, ejgallego/rocq-lsp#500)
 - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/rocq-lsp#503,
   reported by Gijs Pennings)
 - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/rocq-lsp#511)
 - More granular options `send_perf_data` `send_diags`, `verbosity`
   will set them now (@ejgallego, ejgallego/rocq-lsp#517)
 - Preliminary plugin API for completion events (@ejgallego, ejgallego/rocq-lsp#518,
   fixes ejgallego/rocq-lsp#506)
 - Limit the number of messages displayed in the goal window to 101,
   as to workaround slow render of Coq's pretty printing format. This
   is an issue for example in Search where we can get thousand of
   results. We also speed up the rendering a bit by not hashing twice,
   and fix a parameter-passing bug. (@ejgallego, ejgallego/rocq-lsp#523, reported by
   Anton Podkopaev)

Author: ejgallego

packages/coq-lsp/coq-lsp.0.1.7+8.16/opam

@@ -0,0 +1,48 @@
+synopsis: "Language Server Protocol native server for Coq"
+description:
+"""
+Language Server Protocol native server for Coq
+"""
+opam-version: "2.0"
+maintainer: "[email protected]"
+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 <[email protected]>"
+  "Ali Caglayan <[email protected]>"
+  "Shachar Itzhaky <[email protected]>"
+  "Ramkumar Ramachandra <[email protected]>"
+]
+license: "LGPL-2.1-or-later"
+doc: "https://ejgallego.github.io/coq-lsp/"
+
+depends: [
+  "ocaml"        { >= "4.11.0" }
+  "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" }
+
+  # Uncomment this for releases
+  "coq"           { >= "8.16.0" & < "8.17" }
+  "coq-serapi"    { >= "8.16.0" & < "8.17" }
+  "camlp-streams" { >= "5.0" }
+]
+
+build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
+url {
+  src:
+    "https://github.com/ejgallego/coq-lsp/releases/download/0.1.7%2B8.16/coq-lsp-0.1.7.8.16.tbz"
+  checksum: [
+    "sha256=6a88fdb3e42994204f5d2cbc8f4e7da2ac7cf28568a93c8455464c05d1087022"
+    "sha512=38c417cc28a3a0d5eb4305ee5239a0cda6ba425d7f22a17f8d3ec7b9baf27598f57fd9d5ee9a44584a3730b6105128f774abeaf2eb560cfc8bb612aa95fcc0b7"
+  ]
+}
+x-commit-hash: "2ae3f3543a59394750bf081908598906063a051d"