From 0088dfd801f724af7e8d1c6ea39fdbeb467a3854 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 5 Feb 2024 19:13:22 +0100 Subject: [PATCH] [new release] coq-lsp (0.1.8+8.19) CHANGES: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via https://github.com/coq-community/coq-nix-toolbox/pull/164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571) --- packages/coq-lsp/coq-lsp.0.1.8+8.19/opam | 48 ++++++++++++++++++++++++ 1 file changed, 48 insertions(+) create mode 100644 packages/coq-lsp/coq-lsp.0.1.8+8.19/opam diff --git a/packages/coq-lsp/coq-lsp.0.1.8+8.19/opam b/packages/coq-lsp/coq-lsp.0.1.8+8.19/opam new file mode 100644 index 000000000000..3699df30f65c --- /dev/null +++ b/packages/coq-lsp/coq-lsp.0.1.8+8.19/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: "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 " + "Ali Caglayan " + "Shachar Itzhaky " + "Ramkumar Ramachandra " +] +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.19" < "8.20" } + "coq-serapi" { >= "8.19" < "8.20" } +] + +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.8%2B8.19/coq-lsp-0.1.8.8.19.tbz" + checksum: [ + "sha256=1e63289d620e533615812267e96e44c1b5cd2dbdaf26cc9dc8ba00051c2b08c0" + "sha512=9f5e25c6974d293e7c073e65f85936ef18180692dd031c7b709d24d3eefb1955e955c6208cf02c2ac70fa12966d96bc1d43b29f55c425274802289dcf66d5eb2" + ] +} +x-commit-hash: "045913a5bf299f033b82d377dff4e79b288f9b07"