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

CHANGES:

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

 - The info / goal view now uses jsCoq's client-side rendering, with
   better highlighting and layout rendering (@artagnon, @ejgallego,
   ejgallego/rocq-lsp#143, fixes ejgallego/rocq-lsp#96)
 - Printing method is now configurable by the user (@ejgallego, ejgallego/rocq-lsp#143,
   fixes ejgallego/rocq-lsp#321)
 - Trigger completion on quote char "'" (@ejgallego, ejgallego/rocq-lsp#350)
 - Fix typo on keybinding config for show goals (@tomtomjhj, ejgallego/rocq-lsp#357)
 - New request `coq/getDocument` to get serialized full document
   contents. Thanks to Clément Pit-Claudel for feedback and ideas.
   (@ejgallego, ejgallego/rocq-lsp#350)
 - Auto-ignore Coq object files; can be disabled in config
   (@ejgallego, ejgallego/rocq-lsp#365)
 - Support workspaces with multiple roots, this is very useful for
   projects that contain several `_CoqProject` files in different
   directories (@ejgallego, ejgallego/rocq-lsp#374)
 - Add VS Code commands to start / stop the server (@ejgallego, ejgallego/rocq-lsp#377,
   cc ejgallego/rocq-lsp#209)
 - Fix bug that made the server not exit on `exit` LSP notification
   (@artagnon, @ejgallego, ejgallego/rocq-lsp#375, fixes ejgallego/rocq-lsp#230)
 - Lay the foundation for server tests (@artagnon, ejgallego/rocq-lsp#356)
 - Remove the `coq-lsp.ok_diagnostics` setting (@artagnon, ejgallego/rocq-lsp#129)
 - Print abbreviations on hover (@ejgallego, ejgallego/rocq-lsp#384)
 - Print hover types without parenthesis (@ejgallego, ejgallego/rocq-lsp#384)
 - Parse identifiers with dot for hover and jump to definition
   (@ejallego, ejgallego/rocq-lsp#385)
 - Update `vscode-languageclient` to 8.1.0 (@ejgallego, @Alizter,
   ejgallego/rocq-lsp#383, fixes ejgallego/rocq-lsp#273)
 - Fix typo on max_errors checking, this made coq-lsp stop on the
   number of total diagnostics, instead of only errors (@ejgallego,
   ejgallego/rocq-lsp#386)
 - Hover symbol information: hypothesis names must shadow globals of
   the same name (@ejgallego, ejgallego/rocq-lsp#391, fixes ejgallego/rocq-lsp#388)
 - De-schedule document on didClose, otherwise the scheduler will keep
   trying to resume it if it didn't finish (@ejgallego, ejgallego/rocq-lsp#392)
 - Hover symbol information: correctly handle identifiers before '.'
   and containing a quote (') themselves (@ejgallego, ejgallego/rocq-lsp#393)
 - Add children entries to the table-of-contents (@ejgallego, ejgallego/rocq-lsp#394)
 - Invalidate Coq's imperative cache on error (@ejgallego, @r-muhairi,
   ejgallego/rocq-lsp#395)
 - Add status bar button to toggle server run status (@ejgallego,
   @Alizter, ejgallego/rocq-lsp#378, closes ejgallego/rocq-lsp#209)
 - Support for `COQLIB` and `COQCORELIB` environment variables, added
   `--coqcorelib` command line argument (@ejgallego, ejgallego/rocq-lsp#403)
 - Protocol infrastructure for code lenses (@ejgallego, ejgallego/rocq-lsp#396)
 - Set binary mode for protocol input / output (@ejgallego, ejgallego/rocq-lsp#408)
 - Allow to set `ocamlpath` from the command line (@ejgallego, ejgallego/rocq-lsp#408)
 - Windows support (@ejgallego, @jim-portegies, ejgallego/rocq-lsp#408)
 - Scroll active goal into view (@ejgallego, ejgallego/rocq-lsp#410, fixes ejgallego/rocq-lsp#381)
 - Server status icon will now react properly to fatal server errors
   (@ejgallego, reported by @Alizter, ejgallego/rocq-lsp#411, fixes ejgallego/rocq-lsp#399)
 - Info on memory and time is now disabled by default, new option
   `coq-lsp.stats_on_hover_option` to re-enable it (@ejgallego, ejgallego/rocq-lsp#412,
   fixes ejgallego/rocq-lsp#398).
 - `coq-lsp` can now save `.vo` files for files opened in the
   editor. Use the new "Save to .vo" command, or the new protocol
   `coq/saveVo` request (@ejgallego, ejgallego/rocq-lsp#417, fixes ejgallego/rocq-lsp#339)

Author: ejgallego

packages/coq-lsp/coq-lsp.0.1.6.1+8.17/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.17" < "8.18"  }
+  "coq-serapi"   { >= "8.17+rc1+0.17.1" < "8.18"  }
+]
+
+build: [ [ "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.1.6.1%2B8.17/coq-lsp-0.1.6.1.8.17.tbz"
+  checksum: [
+    "sha256=0b0ea3ce68aa549f61c004dd05d2b386dc18811ec4c9ac667ff2917857758707"
+    "sha512=d3e3ae7e055c1be38368fdc86679462e2aa4636805142e8fd1f73423a14a7c87e06d752f04964377fe39ed10972e3c47d433127694b104c0285adb976faadf66"
+  ]
+}
+x-commit-hash: "36467bd7442943af19ce84c646a64f356a0ca5bb"