[new release] coq-lsp (0.1.9+8.17)

[ejgallego]

Language Server Protocol native server for Coq

• Project page: https://github.com/ejgallego/coq-lsp
• Documentation: https://ejgallego.github.io/coq-lsp/

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, [hover] New option show_loc_info_on_hover to display parsing debug info. ejgallego/coq-lsp#588)
• hover plugins can now access the full document, this is convenient
  for many use cases (@ejgallego, [hover] [api] Allow hover access to full document. ejgallego/coq-lsp#591)
• fix hover position computation on the presence of Utf characters
  (@ejgallego, [hover] Fix get_id_at_point in the presence of Unicode chars ejgallego/coq-lsp#597, thanks to Pierre Courtieu for the report and
  example, closes [hover] Missing character to byte offset conversion on hover. 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, [vscode] Workaround broken activation for .mv files ejgallego/coq-lsp#598, cc [vscode] Extension is not actived for .mv files 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, [vscode] Require VSCode >= 1.82 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, [goals] Allow goal mode as LSP parameter, internals ejgallego/coq-lsp#600)
• fix some cases where interrupted computations where memoized
  (@ejgallego, [memo] Fix some cases where interrupted computations where memoized. 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, [internal] [fleche] Absorb errors on document creation and update. ejgallego/coq-lsp#604)
• support OCaml 5.1.x (@ejgallego, [fleche] update progress indicator correctly on End Of File ejgallego/coq-lsp#606)
• update progress indicator correctly on End Of File (@ejgallego,
  [fleche] Store document environment in [Doc.t] ejgallego/coq-lsp#605, fixes Progress indicator and comments don't interact correctly ejgallego/coq-lsp#445)
• [plugins] New astdump plugin to dump AST of files into JSON and
  SEXP (@ejgallego, [ci] Test OCaml 5.1 series ejgallego/coq-lsp#607)
• errors on save where not properly caught (@ejgallego, [plugins] AST dump plugin ejgallego/coq-lsp#608)
• switch default of goal_after_tactic to true (@Alizter,
  @ejgallego, cc: Minor issue with vim and cursor tracking ejgallego/coq-lsp#614)
• error recovery: Recognize Defined and Admitted in lex recovery
  (@ejgallego, [error recovery] Recognize Defined and Admitted in lex recovery ejgallego/coq-lsp#616)
• completion: correctly understand UTF-16 code points on completion
  request (Léo Stefanesco, Follow LSP and treat positions as UTF16 code units ejgallego/coq-lsp#613, fixes No unicode completion after a mathcal character ejgallego/coq-lsp#531)
• don't trigger the goals window in general markdown buffer
  (@ejgallego, [code] Don't trigger goals buffer action in general Markdown documents ejgallego/coq-lsp#625, reported by Théo Zimmerman)
• allow not to postpone full document requests ([example] Example how to use the LSP client ejgallego/coq-lsp#626, @ejgallego)
• new configuration value check_only_on_request which will delay
  checking the document until a request has been made ([fleche] Experimental option for "lazy" document checking. ejgallego/coq-lsp#629, cc: Lazy checking of documents ejgallego/coq-lsp#24,
  @ejgallego)
• fix typo on package.json configuration section (@ejgallego, [code] Fix typo on package.json configuration section ejgallego/coq-lsp#645)
• be more resilient with invalid _CoqProject files (@ejgallego, [workspace] Be more resilient to CoqProject errors. ejgallego/coq-lsp#646)
• support for Coq 8.16 has been abandoned due to lack of dev
  resources (@ejgallego, [compat] Drop support for Coq 8.16, update README 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, [fcc] Add --no_vo option, turn .vo file saving into a plugin. ejgallego/coq-lsp#650)
• depend on memprof-limits on OCaml 4.x (@ejgallego, [coq] Adapt Coq.Protect interface to incorporate an interruption token ejgallego/coq-lsp#660)
• bump minimal OCaml version to 4.12 due to memprof-limits
  (@ejgallego, [coq] Adapt Coq.Protect interface to incorporate an interruption token ejgallego/coq-lsp#660)
• monitor all Coq-level calls under an interruption token
  (@ejgallego, [coq] Monitor Coq calls under a token interruption parameter. ejgallego/coq-lsp#661)
• interpret require thru our own custom execution env-aware path
  (@bhaktishh, @ejgallego, [coq] API to handle Require Ast specifically ejgallego/coq-lsp#642, [memo] Add memo table for Require. ejgallego/coq-lsp#643, [fleche] [doc] Interpret require via special custom path. ejgallego/coq-lsp#644)
• new coq-lsp.plugin.goaldump plugin, as an example on how to dump
  goals from a document (@ejgallego @gbdrt, [plugin] Goal dump plugin. ejgallego/coq-lsp#619)
• new trim command (both in the server and in VSCode) to liberate
  space used in the cache (@ejgallego, [memo] Cache control and eviction improvements ejgallego/coq-lsp#662, fixes [memo] General Memo datatype ejgallego/coq-lsp#367 cc: After closing the buffer coq-lsp should reduce memory consumption ejgallego/coq-lsp#253 Add configurable limit to number of coq-lsp instances running ejgallego/coq-lsp#236
  [memo] Allow users to configure size of Memo table ejgallego/coq-lsp#348)
• fix Coq performance view display (@ejgallego, [bug] The selectionRange request only returns the range of one position of the sent positions ejgallego/coq-lsp#663, regression in
  [fleche] Abstract IO callbacks from LSP transport detail. 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, heatmap display for timing data ejgallego/coq-lsp#686,
  grants Heatmap for timing and other data ejgallego/coq-lsp#681).
• allow more than one input position in selectionRange LSP call
  (@ejgallego, [lsp] Allow selectionRange call to take more than one position. ejgallego/coq-lsp#667, fixes [bug] The selectionRange request only returns the range of one position of the sent positions 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, [vscode] Add simple commands to move backwards / forward in a proof. ejgallego/coq-lsp#671, fixes Shortcut for jump to next sentence ejgallego/coq-lsp#263, fixes Enhancement: action to jump to next/previous Coq sentence ejgallego/coq-lsp#580)
• VSCode commands coq-lsp.sentenceNext / coq-lsp.sentencePrevious
  are now bound by default to Alt + N / Alt + P keybindings
  (@ejgallego, [code] Add keybindings for sentenceNext / sentencePrevious 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, [diagnostics] Add sentence's range to errors extra data field. ejgallego/coq-lsp#670)
• include range of full sentence in error diagnostic extra data
  (@ejgallego, [diagnostics] Add sentence's range to errors extra data field. ejgallego/coq-lsp#670 , thanks to @driverag22 for the idea, cc: [bug] The selectionRange request only returns the range of one position of the sent positions 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, [vscode] Have coq-lsp.pp_type changes take effect immediately ejgallego/coq-lsp#675)
• new public VSCode extension API so other extensions can perform
  actions when the user request the goals (@ejgallego, @bhaktishh,
  [vscode] Provide generic user goal request hook. ejgallego/coq-lsp#672, fixes [vscode client] Export an API for ViZX integration 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, [vscode] [goals] Handle goal requests better when in Live Share 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,
  [fleche] New InjectRequire plugin API ejgallego/coq-lsp#679)
• Add --max_errors=n option to fcc, this way users can set
  --max_errors=0 to imitate coqc behavior (@ejgallego, [fcc] Implement max_errors, fix exit status. ejgallego/coq-lsp#680)
• Fix fcc exit status when checking terminates with fatal errors
  (@ejgallego, @Alizter, [fcc] Implement max_errors, fix exit status. ejgallego/coq-lsp#680)
• Fix install to OPAM switches from main branch (@ejgallego, [build] [doc] [ci] Document and test global opam dev install ejgallego/coq-lsp#683,
  fixes Prelude Not Loading On #509 ejgallego/coq-lsp#682, cc [doc] [contributing] Build setup woes ejgallego/coq-lsp#479 moving projects to /vendor directory doesn't force them to be compiled with the vendored coq version 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, chore: update nix flake ejgallego/coq-lsp#684)
• Update package-lock.json for latest bugfixes (@ejgallego, [code] Update package-lock.json ejgallego/coq-lsp#687)
• Update Nix flake enviroment (@Alizter, chore: update nix flake ejgallego/coq-lsp#684 [dev env] Update prettier to 3.2.5 ejgallego/coq-lsp#688)
• Update prettier (@Alizter @ejgallego, chore: update nix flake ejgallego/coq-lsp#684 [dev env] Update prettier to 3.2.5 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, [fleche] Handle performance data correctly for cached sentences ejgallego/coq-lsp#693)
• Fix type errors in the Performance Data Notifications (@ejgallego,
  @Alizter, [perf] Fixes and improvements towards more interesting uses. ejgallego/coq-lsp#689, [fleche] Handle performance data correctly for cached sentences ejgallego/coq-lsp#693)
• Send performance performance data for the full document
  (@ejgallego, @Alizter, [perf] Fixes and improvements towards more interesting uses. ejgallego/coq-lsp#689, [fleche] Handle performance data correctly for cached sentences ejgallego/coq-lsp#693)
• Better types coq/perfData call (@ejgallego @Alizter, [perf] Fixes and improvements towards more interesting uses. ejgallego/coq-lsp#689)
• New server option to enable / disable coq/perfData (@ejgallego, [perf] Fixes and improvements towards more interesting uses. ejgallego/coq-lsp#689)
• New client option to enable / disable coq/perfData (@ejgallego, [fleche] Auto-check documents on scroll when in lazy mode. ejgallego/coq-lsp#717)
• The coq-lsp.document VSCode command will now display the returned
  JSON data in a new editor (@ejgallego, [code] Display JSON data for coq-lsp.document in new editor. ejgallego/coq-lsp#701)
• Update server settings on the fly when tweaking them in VSCode.
  Implement workspace/didChangeConfiguration (@ejgallego, [lsp] Update server settings on the fly. ejgallego/coq-lsp#702)
• [Coq API] Add functions to retrieve list of declarations done in
  .vo files (@ejallego, @eytans, [coq] Add .vo library file functions ejgallego/coq-lsp#704)
• New petanque API to interact directly with Coq's proof
  engine. (@ejgallego, @gbdrt, Laetitia Teodorescu [petanque] Initial commit, as an OCaml library 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, [petanque] Add a JSON-RPC shell ejgallego/coq-lsp#705)
• New pet-server.exe TCP server for keep-alive sessions (@gbdrt,
  Add a Petanque TCP server ejgallego/coq-lsp#697)
• Always dispose UI elements. This should improve some strange
  behaviors on extension restart (@ejgallego, [code] Correctly dispose even if client shutdown fails. 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, heatmap display for timing data ejgallego/coq-lsp#686,
  grants Heatmap for timing and other data 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, [fleche] Support Coq Meta Commands Reset and Back ejgallego/coq-lsp#709)
• JSON-RPC library now supports all kind of incoming messages
  (@ejgallego, [lsp] Better JSON-RPC serialization 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, [fleche] Auto-check documents on scroll when in lazy mode. 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, [code] Wait for shutdown to complete before we start the client again. ejgallego/coq-lsp#719)
• [code] Center the view if cursor goes out of scope in
  sentenceNext/sentencePrevious (@ejgallego, [code] Add keybindings for sentenceNext / sentencePrevious ejgallego/coq-lsp#718)
• Switch Flèche range encoding to protocol native, this means UTF-16
  code points for now (Léo Stefanesco, @ejgallego, [flèche] Store ranges in protocol-native encoding ejgallego/coq-lsp#624, fixes Diagnostics report positions in UTF-8 code points ejgallego/coq-lsp#620,
  [lsp] Requests input positions are not translated uniformly, and often handled as UTF-8 codepoints instead of UTF-16 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, Give focus back to Goals panel when navigating proofs ejgallego/coq-lsp#722, [code] Preserve original focus when refocusing the panel. 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, [code] Display and allow status bar item to toggle continuous / lazy … ejgallego/coq-lsp#721)
• Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
  [doc] [example] Example of a setup with multiple workspaces. 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, [code] Don't show goals type when details are closed. ejgallego/coq-lsp#730, workarounds
  [goals] Option to hide collapsed goal type display ejgallego/coq-lsp#525 Improvement for goal display ejgallego/coq-lsp#652)
• Support for .lv / .v.tex TeX files with embedded Coq code
  (@ejgallego, [fleche] Support .tex literate documents ejgallego/coq-lsp#727)
• Don't expand bullet goals at previous levels by default
  (@ejgallego, @Alizter, [goals] Don't open goals levels by default. ejgallego/coq-lsp#731 cc [goals] Option to hide collapsed goal type display ejgallego/coq-lsp#525)
• [petanque] Return basic goal information after run_tac, so we
  avoid a goals round-trip for each tactic (@gbdrt, @ejgallego,
  [petanque] Several tweaks from pet-server PR ejgallego/coq-lsp#733)
• [coq] Add support for reading glob files metadata (@ejgallego,
  [petanque] Return extra premise information. ejgallego/coq-lsp#735)
• [petanque] Return extra premise information: file name, position,
  raw_text, using the above support for reading .glob files
  (@ejgallego, [petanque] Return extra premise information. ejgallego/coq-lsp#735)
• [code] Display server status using the LanguageStatusItem
  facility, for now we display version and checking status
  information (moved from [code] Display and allow status bar item to toggle continuous / lazy … ejgallego/coq-lsp#721), and we also allow to toggle the
  checking mode from there (@ejgallego, [code] Show server status using LanguageStatusItem ejgallego/coq-lsp#728)

[mseri]

thanks