this repo has no description

[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)

Changed files
+48
packages
coq-lsp
coq-lsp.0.1.8+8.19
+48
packages/coq-lsp/coq-lsp.0.1.8+8.19/opam
···
+
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 <e@x80.org>"
+
"Ali Caglayan <alizter@gmail.com>"
+
"Shachar Itzhaky <shachari@cs.technion.ac.il>"
+
"Ramkumar Ramachandra <r@artagnon.com>"
+
]
+
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"