Skip to content

Commit

Permalink
[code] Update client changelog.
Browse files Browse the repository at this point in the history
  • Loading branch information
ejgallego committed Oct 25, 2023
1 parent e4082ec commit 550a4a4
Showing 1 changed file with 61 additions and 0 deletions.
61 changes: 61 additions & 0 deletions editor/code/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,3 +1,64 @@
# coq-lsp 0.1.8: Trick-or-treat
-------------------------------

- Update VSCode client dependencies, should bring some performance
improvements to goal pretty printing (@ejgallego, #530)
- Update goal display colors for light mode so they are actually
readable now. (@bhaktishh, #539, fixes #532)
- Added link to Python coq-lsp client by Pedro Carrot and Nuno
Saavedra (@Nfsaavedra, #536)
- Properly concatenate warnings from _CoqProject (@ejgallego,
reported by @mituharu, #541, fixes #540)
- Fix broken `coq/saveVo` and `coq/getDocument` requests due to a
parsing problem with extra fields in their requests (@ejgallego,
#547, reported by @Zimmi48)
- `fcc` now understands the `--coqlib`, `--coqcorelib`,
`--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, #555)
- Describe findlib status in `Workspace.describe`, which is printed
in the output windows (@ejgallego, #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, #557)
- Add pointers to Windows installers (@ejgallego, #559)
- Recognize `Goal` and `Definition $id : ... .` as proof starters
(@ejgallego, #561, reported by @Zimmi48, fixes #548)
- Provide basic notation information on hover. This is intended for
people to build their own more refined notation feedback systems
(@ejgallego, #562)
- Hover request can now be extended by plugins (@ejgallego, #562)
- Updated LSP and JS client libs, notably to vscode-languageclient 9
(@ejgallego, #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, #566, fixes #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, #567, fixes #33)
- `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48,
@CohenCyril, #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, #581, fixes #579)
- Export Query Goals API in VSCode client; this way other extensions
can implement their own commands that query Coq goals (@amblafont,
@ejgallego, #576, closes #558)
- New `pretac` field for preprocessing of goals with a tactic using
speculative execution, this is experimental for now (@amblafont,
@ejgallego, #573, helps with #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, #582)
- Be more robust to mixed-separator windows paths in workspace
detection (@ejgallego, #583, fixes #569)
- Adjust printing breaks in error and message panels (@ejgallego,
@Alizter, #586, fixes #457 , fixes #458 , fixes #571)

# coq-lsp 0.1.7: Just-in-time
-----------------------------

Expand Down

0 comments on commit 550a4a4

Please sign in to comment.