New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[new release] coq-lsp (0.1.8+8.16) #24674

Merged

avsm merged 1 commit into ocaml:master from ejgallego:release-coq-lsp-0.1.8+8.16

Oct 26, 2023

Commits on Oct 25, 2023

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

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
   coq-community/coq-nix-toolbox#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)

ejgallego committed Oct 25, 2023