Skip to content

Commit

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

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

 - new option `show_loc_info_on_hover` that will display parsing debug
   information on hover; previous flag was fixed in code, which is way
   less flexible. This also fixes the option being on in 0.1.8 by
   mistake (@ejgallego, ejgallego/coq-lsp#588)
 - hover plugins can now access the full document, this is convenient
   for many use cases (@ejgallego, ejgallego/coq-lsp#591)
 - fix hover position computation on the presence of Utf characters
   (@ejgallego, ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
   example, closes ejgallego/coq-lsp#594)
 - fix activation bug that prevented extension activation for `.mv`
   files, see discussion in the issues about the upstream policy
   (@ejgallego @r3m0t, ejgallego/coq-lsp#598, cc ejgallego/coq-lsp#596, reported by Théo Zimmerman)
 - require VSCode >= 1.82 in package.json . Our VSCode extension uses
   `vscode-languageclient` 9 which imposes this. (@ejgallego, ejgallego/coq-lsp#599,
   thanks to Théo Zimmerman for the report)
 - `proof/goals` request: new `mode` parameter, to specify goals
   after/before sentence display; renamed `pretac` to `command`, as to
   provide official support for speculative execution (@ejgallego, ejgallego/coq-lsp#600)
 - fix some cases where interrupted computations where memoized
   (@ejgallego, ejgallego/coq-lsp#603)
 - [internal] Flèche [Doc.t] API will now absorb errors on document
   update and creation into the document itself. Thus, a document that
   failed to create or update is still valid, but in the right failed
   state. This is a much needed API change for a lot of use cases
   (@ejgallego, ejgallego/coq-lsp#604)
 - support OCaml 5.1.x (@ejgallego, ejgallego/coq-lsp#606)
 - update progress indicator correctly on End Of File (@ejgallego,
   ejgallego/coq-lsp#605, fixes ejgallego/coq-lsp#445)
 - [plugins] New `astdump` plugin to dump AST of files into JSON and
   SEXP (@ejgallego, ejgallego/coq-lsp#607)
 - errors on save where not properly caught (@ejgallego, ejgallego/coq-lsp#608)
 - switch default of `goal_after_tactic` to `true` (@Alizter,
   @ejgallego, cc: ejgallego/coq-lsp#614)
 - error recovery: Recognize `Defined` and `Admitted` in lex recovery
   (@ejgallego, ejgallego/coq-lsp#616)
 - completion: correctly understand UTF-16 code points on completion
   request (Léo Stefanesco, ejgallego/coq-lsp#613, fixes ejgallego/coq-lsp#531)
 - don't trigger the goals window in general markdown buffer
   (@ejgallego, ejgallego/coq-lsp#625, reported by Théo Zimmerman)
 - allow not to postpone full document requests (ejgallego/coq-lsp#626, @ejgallego)
 - new configuration value `check_only_on_request` which will delay
   checking the document until a request has been made (ejgallego/coq-lsp#629, cc: ejgallego/coq-lsp#24,
   @ejgallego)
 - fix typo on package.json configuration section (@ejgallego, ejgallego/coq-lsp#645)
 - be more resilient with invalid _CoqProject files (@ejgallego, ejgallego/coq-lsp#646)
 - support for Coq 8.16 has been abandoned due to lack of dev
   resources (@ejgallego, ejgallego/coq-lsp#649)
 - new option `--no_vo` for `fcc`, which will skip the `.vo` saving
   step. `.vo` saving is now an `fcc` plugins, but for now, it is
   enabled by default (@ejgallego, ejgallego/coq-lsp#650)
 - depend on `memprof-limits` on OCaml 4.x (@ejgallego, ejgallego/coq-lsp#660)
 - bump minimal OCaml version to 4.12 due to `memprof-limits`
   (@ejgallego, ejgallego/coq-lsp#660)
 - monitor all Coq-level calls under an interruption token
   (@ejgallego, ejgallego/coq-lsp#661)
 - interpret require thru our own custom execution env-aware path
   (@bhaktishh, @ejgallego, ejgallego/coq-lsp#642, ejgallego/coq-lsp#643, ejgallego/coq-lsp#644)
 - new `coq-lsp.plugin.goaldump` plugin, as an example on how to dump
   goals from a document (@ejgallego @gbdrt, ejgallego/coq-lsp#619)
 - new trim command (both in the server and in VSCode) to liberate
   space used in the cache (@ejgallego, ejgallego/coq-lsp#662, fixes ejgallego/coq-lsp#367 cc: ejgallego/coq-lsp#253 ejgallego/coq-lsp#236
   ejgallego/coq-lsp#348)
 - fix Coq performance view display (@ejgallego, ejgallego/coq-lsp#663, regression in
   ejgallego/coq-lsp#513)
 - Added new heatmap feature allowing timing data to be seen in the
   editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   command. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - allow more than one input position in `selectionRange` LSP call
   (@ejgallego, ejgallego/coq-lsp#667, fixes ejgallego/coq-lsp#663)
 - new VSCode commands to allow to move one sentence backwards /
   forward, this is particularly useful when combined with lazy
   checking mode (@ejgallego, ejgallego/coq-lsp#671, fixes ejgallego/coq-lsp#263, fixes ejgallego/coq-lsp#580)
 - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
   are now bound by default to `Alt + N` / `Alt + P` keybindings
   (@ejgallego, ejgallego/coq-lsp#718)
 - change diagnostic `extra` field to `data`, so we now conform to the
   LSP spec, include the data only when the `send_diags_extra_data`
   server-side option is enabled (@ejgallego, ejgallego/coq-lsp#670)
 - include range of full sentence in error diagnostic extra data
   (@ejgallego, ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: ejgallego/coq-lsp#663).
 - The `coq-lsp.pp_type` VSCode client option now takes effect
   immediately, no more need to restart the server to get different
   goal display formats (@ejgallego, ejgallego/coq-lsp#675)
 - new public VSCode extension API so other extensions can perform
   actions when the user request the goals (@ejgallego, @bhaktishh,
   ejgallego/coq-lsp#672, fixes ejgallego/coq-lsp#538)
 - Support Visual Studio Live Share URIs better (`vsls://`), in
   particular don't try to display goals if the URI is VSLS one
   (@ejgallego, ejgallego/coq-lsp#676)
 - New `InjectRequire` plugin API for plugins to be able to instrument
   the default import list of files (@ejgallego @corwin-of-amber,
   ejgallego/coq-lsp#679)
 - Add `--max_errors=n` option to `fcc`, this way users can set
   `--max_errors=0` to imitate `coqc` behavior (@ejgallego, ejgallego/coq-lsp#680)
 - Fix `fcc` exit status when checking terminates with fatal errors
   (@ejgallego, @Alizter, ejgallego/coq-lsp#680)
 - Fix install to OPAM switches from `main` branch (@ejgallego, ejgallego/coq-lsp#683,
   fixes ejgallego/coq-lsp#682, cc ejgallego/coq-lsp#479 ejgallego/coq-lsp#488, thanks to @HazardousPeach for the report)
 - New `--int_backend={Coq,Mp}` command line parameter to select the
   interruption method for Coq (@ejgallego, ejgallego/coq-lsp#684)
 - Update `package-lock.json` for latest bugfixes (@ejgallego, ejgallego/coq-lsp#687)
 - Update Nix flake enviroment (@Alizter, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Update `prettier` (@Alizter @ejgallego, ejgallego/coq-lsp#684 ejgallego/coq-lsp#688)
 - Store original performance data in the cache, so we now display the
   original timing and memory data even for cached commands (@ejgallego, ejgallego/coq-lsp#693)
 - Fix type errors in the Performance Data Notifications (@ejgallego,
   @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Send performance performance data for the full document
   (@ejgallego, @Alizter, ejgallego/coq-lsp#689, ejgallego/coq-lsp#693)
 - Better types `coq/perfData` call (@ejgallego @Alizter, ejgallego/coq-lsp#689)
 - New server option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#689)
 - New client option to enable / disable `coq/perfData` (@ejgallego, ejgallego/coq-lsp#717)
 - The `coq-lsp.document` VSCode command will now display the returned
   JSON data in a new editor (@ejgallego, ejgallego/coq-lsp#701)
 - Update server settings on the fly when tweaking them in VSCode.
   Implement `workspace/didChangeConfiguration` (@ejgallego, ejgallego/coq-lsp#702)
 - [Coq API] Add functions to retrieve list of declarations done in
   .vo files (@ejallego, @eytans, ejgallego/coq-lsp#704)
 - New `petanque` API to interact directly with Coq's proof
   engine. (@ejgallego, @gbdrt, Laetitia Teodorescu ejgallego/coq-lsp#703, thanks to
   Alex Sanchez-Stern for many insightful feedback and testing)
 - New `petanque` JSON-RPC `pet.exe`, which can be used à la SerAPI
   to perform proof search and more (@ejgallego, @gbdrt, ejgallego/coq-lsp#705)
 - New `pet-server.exe` TCP server for keep-alive sessions (@gbdrt,
   ejgallego/coq-lsp#697)
 - Always dispose UI elements. This should improve some strange
   behaviors on extension restart (@ejgallego, ejgallego/coq-lsp#708)
 - [code] Added new heatmap feature allowing timing data to be seen in
   the editor. Can be enabled with the `Coq LSP: Toggle heatmap`
   comamnd. Can be configured to show memory usage. Colors and
   granularity are configurable. (@Alizter and @ejgallego, ejgallego/coq-lsp#686,
   grants ejgallego/coq-lsp#681).
 - [server] Support Coq meta-commands (Reset, Reset Initial, Back)
   They are actually pretty useful to hint the incremental engine to
   ignore changes in some part of the document (@ejgallego, ejgallego/coq-lsp#709)
 - JSON-RPC library now supports all kind of incoming messages
   (@ejgallego, ejgallego/coq-lsp#713)
 - [code/server] New `coq/viewRange` notification, from client to
   server, than hints the scheduler for the visible area of the
   document; combined with the new lazy checking mode, this provides
   checking on scroll, a feature inspired from Isabelle IDE
   (@ejgallego, ejgallego/coq-lsp#717)
 - [code] Have VSCode wait for full LSP client shutdown on server
   restart. This fixes some bugs on extension restart (finally!)
   (@ejgallego, ejgallego/coq-lsp#719)
 - [code] Center the view if cursor goes out of scope in
   `sentenceNext/sentencePrevious` (@ejgallego, ejgallego/coq-lsp#718)
 - Switch Flèche range encoding to protocol native, this means UTF-16
   code points for now (Léo Stefanesco, @ejgallego, ejgallego/coq-lsp#624, fixes ejgallego/coq-lsp#620,
   ejgallego/coq-lsp#621)
 - Give `Goals` panel focus back if it has lost it (in case of
   multiple panels in the second viewColumn of Vscode) whenever
   user navigates proofs (@Alidra @ejgallego, ejgallego/coq-lsp#722, ejgallego/coq-lsp#725)
 - `fcc`: new option `--diags_level` to control whether Coq's notice
   and info messages appear as diagnostics
 - [code] Display the continous/on-request checking mode in the status bar,
   allow to change it by clicking on it (@ejgallego, ejgallego/coq-lsp#721)
 - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
   ejgallego/coq-lsp#611)
 - Don't show types of un-expanded goals. We should add an option for
   this, but we don't have the cycles (@ejgallego, ejgallego/coq-lsp#730, workarounds
   ejgallego/coq-lsp#525 ejgallego/coq-lsp#652)
 - Support for `.lv / .v.tex` TeX files with embedded Coq code
   (@ejgallego, ejgallego/coq-lsp#727)
 - Don't expand bullet goals at previous levels by default
   (@ejgallego, @Alizter, ejgallego/coq-lsp#731 cc ejgallego/coq-lsp#525)
 - [petanque] Return basic goal information after `run_tac`, so we
   avoid a `goals` round-trip for each tactic (@gbdrt, @ejgallego,
   ejgallego/coq-lsp#733)
 - [coq] Add support for reading glob files metadata (@ejgallego,
   ejgallego/coq-lsp#735)
 - [petanque] Return extra premise information: file name, position,
   raw_text, using the above support for reading .glob files
   (@ejgallego, ejgallego/coq-lsp#735)
 - [code] Display server status using the `LanguageStatusItem`
   facility, for now we display version and checking status
   information (moved from ejgallego/coq-lsp#721), and we also allow to toggle the
   checking mode from there (@ejgallego, ejgallego/coq-lsp#728)
  • Loading branch information
ejgallego committed May 31, 2024
1 parent b502ec7 commit 5d96299
Showing 1 changed file with 58 additions and 0 deletions.
58 changes: 58 additions & 0 deletions packages/coq-lsp/coq-lsp.0.1.9+8.19/opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
synopsis: "Language Server Protocol native server for Coq"
description:
"""
Language Server Protocol native server for Coq
"""
opam-version: "2.0"
maintainer: "[email protected]"
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 <[email protected]>"
"Ali Caglayan <[email protected]>"
"Shachar Itzhaky <[email protected]>"
"Ramkumar Ramachandra <[email protected]>"
]
license: "LGPL-2.1-or-later"
doc: "https://ejgallego.github.io/coq-lsp/"

depends: [

("ocaml" {>= "5.0"} | ("ocaml" {<= "5.0"} & "memprof-limits" { >= "0.2.1" } ))

"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" }

# unit testing
"ppx_inline_test" { >= "0.14.1" }

# Uncomment this for releases
"coq" { >= "8.19" < "8.20" }
"coq-serapi" { >= "8.19" < "8.20" }
]

depopts: ["lwt" "logs"]

build: [
[ "rm" "-rf" "vendor" ]
[ "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.9%2B8.19/coq-lsp-0.1.9.8.19.tbz"
checksum: [
"sha256=ef664281ab6e242dd79374cbbe4f177f2f071d3457cd3b75c23643948d475961"
"sha512=3c180c0c2e1218936b6cacb37197370cf80be4c372c46e38a2ab403a5a6e99cd6403f927ecfc017aefa2ead856abb389d48feb183049bf2c7badb029ce13f1ee"
]
}
x-commit-hash: "80475067d4ffee4ad370eadf41ad1188e2d2c1fe"

0 comments on commit 5d96299

Please sign in to comment.