ejgallego/coq-lsp 0.1.9+8.17

on GitHub

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, #588)
• hover plugins can now access the full document, this is convenient
  for many use cases (@ejgallego, #591)
• fix hover position computation on the presence of Utf characters
  (@ejgallego, #597, thanks to Pierre Courtieu for the report and
  example, closes #594)
• fix activation bug that prevented extension activation for .mv
  files, see discussion in the issues about the upstream policy
  (@ejgallego @r3m0t, #598, cc #596, reported by Théo Zimmerman)
• require VSCode >= 1.82 in package.json . Our VSCode extension uses
  vscode-languageclient 9 which imposes this. (@ejgallego, #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, #600)
• fix some cases where interrupted computations where memoized
  (@ejgallego, #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, #604)
• support OCaml 5.1.x (@ejgallego, #606)
• update progress indicator correctly on End Of File (@ejgallego,
  #605, fixes #445)
• [plugins] New astdump plugin to dump AST of files into JSON and
  SEXP (@ejgallego, #607)
• errors on save where not properly caught (@ejgallego, #608)
• switch default of goal_after_tactic to true (@Alizter,
  @ejgallego, cc: #614)
• error recovery: Recognize Defined and Admitted in lex recovery
  (@ejgallego, #616)
• completion: correctly understand UTF-16 code points on completion
  request (Léo Stefanesco, #613, fixes #531)
• don't trigger the goals window in general markdown buffer
  (@ejgallego, #625, reported by Théo Zimmerman)
• allow not to postpone full document requests (#626, @ejgallego)
• new configuration value check_only_on_request which will delay
  checking the document until a request has been made (#629, cc: #24,
  @ejgallego)
• fix typo on package.json configuration section (@ejgallego, #645)
• be more resilient with invalid _CoqProject files (@ejgallego, #646)
• support for Coq 8.16 has been abandoned due to lack of dev
  resources (@ejgallego, #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, #650)
• depend on memprof-limits on OCaml 4.x (@ejgallego, #660)
• bump minimal OCaml version to 4.12 due to memprof-limits
  (@ejgallego, #660)
• monitor all Coq-level calls under an interruption token
  (@ejgallego, #661)
• interpret require thru our own custom execution env-aware path
  (@bhaktishh, @ejgallego, #642, #643, #644)
• new coq-lsp.plugin.goaldump plugin, as an example on how to dump
  goals from a document (@ejgallego @gbdrt, #619)
• new trim command (both in the server and in VSCode) to liberate
  space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236
  #348)
• fix Coq performance view display (@ejgallego, #663, regression in
  #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, #686,
  grants #681).
• allow more than one input position in selectionRange LSP call
  (@ejgallego, #667, fixes #663)
• new VSCode commands to allow to move one sentence backwards /
  forward, this is particularly useful when combined with lazy
  checking mode (@ejgallego, #671, fixes #263, fixes #580)
• VSCode commands coq-lsp.sentenceNext / coq-lsp.sentencePrevious
  are now bound by default to Alt + N / Alt + P keybindings
  (@ejgallego, #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, #670)
• include range of full sentence in error diagnostic extra data
  (@ejgallego, #670 , thanks to @driverag22 for the idea, cc: #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, #675)
• new public VSCode extension API so other extensions can perform
  actions when the user request the goals (@ejgallego, @bhaktishh,
  #672, fixes #538)
• Support Visual Studio Live Share URIs better (vsls://), in
  particular don't try to display goals if the URI is VSLS one
  (@ejgallego, #676)
• New InjectRequire plugin API for plugins to be able to instrument
  the default import list of files (@ejgallego @corwin-of-amber,
  #679)
• Add --max_errors=n option to fcc, this way users can set
  --max_errors=0 to imitate coqc behavior (@ejgallego, #680)
• Fix fcc exit status when checking terminates with fatal errors
  (@ejgallego, @Alizter, #680)
• Fix install to OPAM switches from main branch (@ejgallego, #683,
  fixes #682, cc #479 #488, thanks to @HazardousPeach for the report)
• New --int_backend={Coq,Mp} command line parameter to select the
  interruption method for Coq (@ejgallego, #684)
• Update package-lock.json for latest bugfixes (@ejgallego, #687)
• Update Nix flake enviroment (@Alizter, #684 #688)
• Update prettier (@Alizter @ejgallego, #684 #688)
• Store original performance data in the cache, so we now display the
  original timing and memory data even for cached commands (@ejgallego, #693)
• Fix type errors in the Performance Data Notifications (@ejgallego,
  @Alizter, #689, #693)
• Send performance performance data for the full document
  (@ejgallego, @Alizter, #689, #693)
• Better types coq/perfData call (@ejgallego @Alizter, #689)
• New server option to enable / disable coq/perfData (@ejgallego, #689)
• New client option to enable / disable coq/perfData (@ejgallego, #717)
• The coq-lsp.document VSCode command will now display the returned
  JSON data in a new editor (@ejgallego, #701)
• Update server settings on the fly when tweaking them in VSCode.
  Implement workspace/didChangeConfiguration (@ejgallego, #702)
• [Coq API] Add functions to retrieve list of declarations done in
  .vo files (@ejallego, @eytans, #704)
• New petanque API to interact directly with Coq's proof
  engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #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, #705)
• New pet-server.exe TCP server for keep-alive sessions (@gbdrt,
  #697)
• Always dispose UI elements. This should improve some strange
  behaviors on extension restart (@ejgallego, #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, #686,
  grants #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, #709)
• JSON-RPC library now supports all kind of incoming messages
  (@ejgallego, #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, #717)
• [code] Have VSCode wait for full LSP client shutdown on server
  restart. This fixes some bugs on extension restart (finally!)
  (@ejgallego, #719)
• [code] Center the view if cursor goes out of scope in
  sentenceNext/sentencePrevious (@ejgallego, #718)
• Switch Flèche range encoding to protocol native, this means UTF-16
  code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620,
  #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, #722, #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, #721)
• Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
  #611)
• Don't show types of un-expanded goals. We should add an option for
  this, but we don't have the cycles (@ejgallego, #730, workarounds
  #525 #652)
• Support for .lv / .v.tex TeX files with embedded Coq code
  (@ejgallego, #727)
• Don't expand bullet goals at previous levels by default
  (@ejgallego, @Alizter, #731 cc #525)
• [petanque] Return basic goal information after run_tac, so we
  avoid a goals round-trip for each tactic (@gbdrt, @ejgallego,
  #733)
• [coq] Add support for reading glob files metadata (@ejgallego,
  #735)
• [petanque] Return extra premise information: file name, position,
  raw_text, using the above support for reading .glob files
  (@ejgallego, #735)
• [code] Display server status using the LanguageStatusItem
  facility, for now we display version and checking status
  information (moved from #721), and we also allow to toggle the
  checking mode from there (@ejgallego, #728)