Skip to content

Commit 96b7052

Browse files
committed
[new release] coq-lsp (0.1.1+v8.16)
CHANGES: ------------------------- - Don't crash if the log file can't be created (@ejgallego, ejgallego/rocq-lsp#87) - Use LSP functions for client-side logging (@ejgallego, ejgallego/rocq-lsp#87) - Log `_CoqProject` detection settings to client window (@ejgallego, ejgallego/rocq-lsp#88) - Use plugin include paths from `_CoqProject` (@ejgallego, ejgallego/rocq-lsp#88) - Support OCaml >= 4.12 (@ejgallego, ejgallego/rocq-lsp#93) - Optimize the number of diagnostics sent in eager mode (@ejgallego, ejgallego/rocq-lsp#104) - Improved syntax highlighting on VSCode client (@artagnon, ejgallego/rocq-lsp#105) - Resume document checking from the point it was interrupted (@ejgallego, ejgallego/rocq-lsp#95, ejgallego/rocq-lsp#99) - Don't convert Coq "Info" messages such as "Foo is defined" to feedback by default; users willing to see them can set the corresponding option (@ejgallego, ejgallego/rocq-lsp#113) - Send `$/coq/fileProgress` progress notifications from server, similarly to what Lean does; display them in Code's right gutter (@ejgallego, ejgallego/rocq-lsp#106, fixes ejgallego/rocq-lsp#54) - Show goals on click by default, allow users to configure the behavior to follow cursor in different ways (@ejgallego, ejgallego/rocq-lsp#116, fixes ejgallego/rocq-lsp#89) - Show file position in goal buffer, use collapsible elements for goal list (@ejgallego, ejgallego/rocq-lsp#115, fixes ejgallego/rocq-lsp#109) - Resume checking from common prefix on document update (@ejgallego, ejgallego/rocq-lsp#111, fixes ejgallego/rocq-lsp#110) - Only serve goals, hover, and symbols requests when the document has been sufficiently processed (@ejgallego, ejgallego/rocq-lsp#120, fixes ejgallego/rocq-lsp#100)
1 parent cb23d5f commit 96b7052

File tree

1 file changed

+41
-0
lines changed
  • packages/coq-lsp/coq-lsp.0.1.1+v8.16

1 file changed

+41
-0
lines changed
Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
synopsis: "Language Server Protocol native server for Coq"
2+
description:
3+
"""
4+
Language Server Protocol native server for Coq
5+
"""
6+
opam-version: "2.0"
7+
maintainer: "[email protected]"
8+
bug-reports: "https://github.com/ejgallego/coq-lsp/issues"
9+
homepage: "https://github.com/ejgallego/coq-lsp"
10+
dev-repo: "git+https://github.com/ejgallego/coq-lsp.git"
11+
authors: [
12+
"Emilio Jesús Gallego Arias <[email protected]>"
13+
]
14+
license: "LGPL-2.1-or-later"
15+
doc: "https://ejgallego.github.io/coq-lsp/"
16+
17+
depends: [
18+
"ocaml" { >= "4.12.0" }
19+
"dune" { >= "3.2" }
20+
21+
# Not yet required, install Coq deps instead
22+
"coq" { >= "8.16.0" & < "8.17" }
23+
"coq-serapi" { >= "8.16.0" & < "8.17" }
24+
"camlp-streams" { >= "5.0" }
25+
26+
# lsp dependencies
27+
"cmdliner" { >= "1.1.0" }
28+
"yojson" { >= "1.7.0" }
29+
]
30+
31+
build: [ [ "dune" "build" "-p" name "-j" jobs ] ]
32+
run-test: [ [ "dune" "runtest" "-p" name "-j" jobs ] ]
33+
url {
34+
src:
35+
"https://github.com/ejgallego/coq-lsp/releases/download/0.1.1%2Bv8.16/coq-lsp-0.1.1.v8.16.tbz"
36+
checksum: [
37+
"sha256=be48fd1449d8a0eb209e83ebbcde95090e94ba74ee7e744a399c3a5b67cc4acb"
38+
"sha512=c711b953346d3e45ed61c75d5f3825d877820dec38e5dc803cd1ab9a32d6b4a850232a84984c3c340d3939c459ea0595f606d303e1ba714e4245a784b3507ab0"
39+
]
40+
}
41+
x-commit-hash: "5a7a5de8784061f46b58a00dae9365aabd9daa31"

0 commit comments

Comments
 (0)