Skip to content

Commit

Permalink
[new release] coq-lsp (0.1.6.1+8.17)
Browse files Browse the repository at this point in the history
CHANGES:

---------------------

 - The info / goal view now uses jsCoq's client-side rendering, with
   better highlighting and layout rendering (@artagnon, @ejgallego,
   ejgallego/coq-lsp#143, fixes ejgallego/coq-lsp#96)
 - Printing method is now configurable by the user (@ejgallego, ejgallego/coq-lsp#143,
   fixes ejgallego/coq-lsp#321)
 - Trigger completion on quote char "'" (@ejgallego, ejgallego/coq-lsp#350)
 - Fix typo on keybinding config for show goals (@tomtomjhj, ejgallego/coq-lsp#357)
 - New request `coq/getDocument` to get serialized full document
   contents. Thanks to Clément Pit-Claudel for feedback and ideas.
   (@ejgallego, ejgallego/coq-lsp#350)
 - Auto-ignore Coq object files; can be disabled in config
   (@ejgallego, ejgallego/coq-lsp#365)
 - Support workspaces with multiple roots, this is very useful for
   projects that contain several `_CoqProject` files in different
   directories (@ejgallego, ejgallego/coq-lsp#374)
 - Add VS Code commands to start / stop the server (@ejgallego, ejgallego/coq-lsp#377,
   cc ejgallego/coq-lsp#209)
 - Fix bug that made the server not exit on `exit` LSP notification
   (@artagnon, @ejgallego, ejgallego/coq-lsp#375, fixes ejgallego/coq-lsp#230)
 - Lay the foundation for server tests (@artagnon, ejgallego/coq-lsp#356)
 - Remove the `coq-lsp.ok_diagnostics` setting (@artagnon, ejgallego/coq-lsp#129)
 - Print abbreviations on hover (@ejgallego, ejgallego/coq-lsp#384)
 - Print hover types without parenthesis (@ejgallego, ejgallego/coq-lsp#384)
 - Parse identifiers with dot for hover and jump to definition
   (@ejallego, ejgallego/coq-lsp#385)
 - Update `vscode-languageclient` to 8.1.0 (@ejgallego, @Alizter,
   ejgallego/coq-lsp#383, fixes ejgallego/coq-lsp#273)
 - Fix typo on max_errors checking, this made coq-lsp stop on the
   number of total diagnostics, instead of only errors (@ejgallego,
   ejgallego/coq-lsp#386)
 - Hover symbol information: hypothesis names must shadow globals of
   the same name (@ejgallego, ejgallego/coq-lsp#391, fixes ejgallego/coq-lsp#388)
 - De-schedule document on didClose, otherwise the scheduler will keep
   trying to resume it if it didn't finish (@ejgallego, ejgallego/coq-lsp#392)
 - Hover symbol information: correctly handle identifiers before '.'
   and containing a quote (') themselves (@ejgallego, ejgallego/coq-lsp#393)
 - Add children entries to the table-of-contents (@ejgallego, ejgallego/coq-lsp#394)
 - Invalidate Coq's imperative cache on error (@ejgallego, @r-muhairi,
   ejgallego/coq-lsp#395)
 - Add status bar button to toggle server run status (@ejgallego,
   @Alizter, ejgallego/coq-lsp#378, closes ejgallego/coq-lsp#209)
 - Support for `COQLIB` and `COQCORELIB` environment variables, added
   `--coqcorelib` command line argument (@ejgallego, ejgallego/coq-lsp#403)
 - Protocol infrastructure for code lenses (@ejgallego, ejgallego/coq-lsp#396)
 - Set binary mode for protocol input / output (@ejgallego, ejgallego/coq-lsp#408)
 - Allow to set `ocamlpath` from the command line (@ejgallego, ejgallego/coq-lsp#408)
 - Windows support (@ejgallego, @jim-portegies, ejgallego/coq-lsp#408)
 - Scroll active goal into view (@ejgallego, ejgallego/coq-lsp#410, fixes ejgallego/coq-lsp#381)
 - Server status icon will now react properly to fatal server errors
   (@ejgallego, reported by @Alizter, ejgallego/coq-lsp#411, fixes ejgallego/coq-lsp#399)
 - Info on memory and time is now disabled by default, new option
   `coq-lsp.stats_on_hover_option` to re-enable it (@ejgallego, ejgallego/coq-lsp#412,
   fixes ejgallego/coq-lsp#398).
 - `coq-lsp` can now save `.vo` files for files opened in the
   editor. Use the new "Save to .vo" command, or the new protocol
   `coq/saveVo` request (@ejgallego, ejgallego/coq-lsp#417, fixes ejgallego/coq-lsp#339)
  • Loading branch information
ejgallego committed Apr 3, 2023
1 parent 0067676 commit f1962a2
Showing 1 changed file with 48 additions and 0 deletions.
48 changes: 48 additions & 0 deletions packages/coq-lsp/coq-lsp.0.1.6.1+8.17/opam
Original file line number Diff line number Diff line change
@@ -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 <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.17" < "8.18" }
"coq-serapi" { >= "8.17+rc1+0.17.1" < "8.18" }
]

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.6.1%2B8.17/coq-lsp-0.1.6.1.8.17.tbz"
checksum: [
"sha256=7fa63b7e0742f20f6b1a3a7abf64459db5776493830bd5941e60a9a100d53562"
"sha512=20d0931f821825cee11cd6aa24aeb8d1676620d3b79ba27cd42de1a49edbbd789cfcd49cf76faa946779700f575403f0f632ff48e81f2095c6f3170261351559"
]
}
x-commit-hash: "bfe6da959cf854a9b483bbe419b5447cb8a1516d"

0 comments on commit f1962a2

Please sign in to comment.