0.2.2+8.20

CHANGES:

---

• [vscode] Expand selectors to include vscode-vfs:// URIs used in
  github.dev, document limited virtual workspace support in
  package.json (@ejgallego, #849)

0.2.2+8.19

CHANGES:

---

• [vscode] Expand selectors to include vscode-vfs:// URIs used in
  github.dev, document limited virtual workspace support in
  package.json (@ejgallego, #849)

0.2.2+8.18

CHANGES:

---

• [vscode] Expand selectors to include vscode-vfs:// URIs used in
  github.dev, document limited virtual workspace support in
  package.json (@ejgallego, #849)

0.2.2+8.17

CHANGES:

---

• [vscode] Expand selectors to include vscode-vfs:// URIs used in
  github.dev, document limited virtual workspace support in
  package.json (@ejgallego, #849)

0.2.0+8.20

CHANGES:

---

• [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
  dependency, and will greatly easy the development of tools that
  require AST manipulation (@ejgallego, #698)
• [fleche] Remove 8.16 compatibility layer (@ejgallego, #747)
• [fleche] Preserve view hint across document changes. With this
  change, we get local continuous checking mode when the view-port
  heuristic is enabled (@ejgallego, #748)
• [memo] More precise hashing for Coq states, this improves cache
  performance quite a bit (@ejgallego, #751)
• [fleche] Enable sharing of .vo file parsing. This enables better
  sharing, achieving an almost 50% memory reduction for example when
  opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh,
  #744)
• [memo] Provide API to query Hashtbl stats (@ejgallego, #753)
• [nix] Add pet-server deps to flake.nix (Léo Stefanesco, #754)
• [coq-lsp] Fix crash on --help option (Léo Stefanesco, @ejgallego,
  #754)
• [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
  #755, cc: #722, #725)
• [hover] Show input howto for unicode characters on hover
  (@ejgallego, Léo Stefanesco, #756)
• [lsp] [definition] Support for jump to definition across workspace
  files. The location information is obtained from .glob files, so
  it is often not perfect. (@ejgallego, #762, fixes #317)
• [lsp] [hover] Show full name and provenance of identifiers
  (@ejgallego, #762)
• [lsp] [definition] Try also to resolve and locate module imports
  (@ejgallego, #764)
• [code] Don't start server on extension activation, unless an editor
  we own is active. We also auto-start the server if a document that
  we own is opened later (@ejgallego, #758, fixes #750)
• [petanque] Allow init to be called multiple times (@ejgallego,
  @gbdrt, #766)
• [petanque] Faster query for goals status after run_tac
  (@ejgallego, #768)
• [petanque] New parameter pre_commands to start which allows
  instrumenting the goal before starting the proof (@ejgallego, Alex
  Sanchez-Stern #769)
• [petanque] New http_headers={yes,no} parameter for pet json
  shell, plus some improvements on protocol handling (@ejgallego,
  #770)
• [petanque] Make agent agnostic of environment, allowing embedding
  inside LSP (@ejgallego, #771)
• [diagnostics] Ensure extra diagnostics info is present in all
  errors, not only on those sentences that did parse successfully
  (@ejgallego, Diego Rivera, #772)
• [hover] New option show_universes_on_hover that will display
  universe data on hover (@ejgallego, @SkySkimmer, #666)
• [hover] New plugin unidiff that will elaborate a summary of
  universe data a file, in particular regarding universes added at
  Qed time (@ejgallego, #773)
• [fleche] Support meta-command Abort All (@ejgallego, #774, fixes
  #550)
• [petanque] Allow memoization control on petanque/run via a new
  parameter memo (@ejgallego, #780)
• [lsp] [petanque] Allow acces to petanque protocol from the lsp
  server (@ejgallego, #778)
• [petanque] Always initialize a workspace. This made pet crash if
  --root was not used and client didn't issue the optimal
  setWorkspace call (#782, @ejgallego, @gbdrt)
• [lsp] [petanque] New methods state/eq and state/hash; this
  allows clients to implement a client-side hash; equality is
  configurable with different methods; moreover, petanque/run can
  compute some extra data like state hashing without a round-trip
  (@ejgallego @gbdrt, #779)
• [petanque] New methods to hash proof states; use proof state hash
  by default in petanque agent (@ejgallego, @gbdrt, #808)
• [petanque] New shell method petanque/toc that returns a document
  outline in LSP-style (@ejgallego, #794)

0.2.0+8.19

CHANGES:

---

• [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
  dependency, and will greatly easy the development of tools that
  require AST manipulation (@ejgallego, #698)
• [fleche] Remove 8.16 compatibility layer (@ejgallego, #747)
• [fleche] Preserve view hint across document changes. With this
  change, we get local continuous checking mode when the view-port
  heuristic is enabled (@ejgallego, #748)
• [memo] More precise hashing for Coq states, this improves cache
  performance quite a bit (@ejgallego, #751)
• [fleche] Enable sharing of .vo file parsing. This enables better
  sharing, achieving an almost 50% memory reduction for example when
  opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh,
  #744)
• [memo] Provide API to query Hashtbl stats (@ejgallego, #753)
• [nix] Add pet-server deps to flake.nix (Léo Stefanesco, #754)
• [coq-lsp] Fix crash on --help option (Léo Stefanesco, @ejgallego,
  #754)
• [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
  #755, cc: #722, #725)
• [hover] Show input howto for unicode characters on hover
  (@ejgallego, Léo Stefanesco, #756)
• [lsp] [definition] Support for jump to definition across workspace
  files. The location information is obtained from .glob files, so
  it is often not perfect. (@ejgallego, #762, fixes #317)
• [lsp] [hover] Show full name and provenance of identifiers
  (@ejgallego, #762)
• [lsp] [definition] Try also to resolve and locate module imports
  (@ejgallego, #764)
• [code] Don't start server on extension activation, unless an editor
  we own is active. We also auto-start the server if a document that
  we own is opened later (@ejgallego, #758, fixes #750)
• [petanque] Allow init to be called multiple times (@ejgallego,
  @gbdrt, #766)
• [petanque] Faster query for goals status after run_tac
  (@ejgallego, #768)
• [petanque] New parameter pre_commands to start which allows
  instrumenting the goal before starting the proof (@ejgallego, Alex
  Sanchez-Stern #769)
• [petanque] New http_headers={yes,no} parameter for pet json
  shell, plus some improvements on protocol handling (@ejgallego,
  #770)
• [petanque] Make agent agnostic of environment, allowing embedding
  inside LSP (@ejgallego, #771)
• [diagnostics] Ensure extra diagnostics info is present in all
  errors, not only on those sentences that did parse successfully
  (@ejgallego, Diego Rivera, #772)
• [hover] New option show_universes_on_hover that will display
  universe data on hover (@ejgallego, @SkySkimmer, #666)
• [hover] New plugin unidiff that will elaborate a summary of
  universe data a file, in particular regarding universes added at
  Qed time (@ejgallego, #773)
• [fleche] Support meta-command Abort All (@ejgallego, #774, fixes
  #550)
• [petanque] Allow memoization control on petanque/run via a new
  parameter memo (@ejgallego, #780)
• [lsp] [petanque] Allow acces to petanque protocol from the lsp
  server (@ejgallego, #778)
• [petanque] Always initialize a workspace. This made pet crash if
  --root was not used and client didn't issue the optimal
  setWorkspace call (#782, @ejgallego, @gbdrt)
• [lsp] [petanque] New methods state/eq and state/hash; this
  allows clients to implement a client-side hash; equality is
  configurable with different methods; moreover, petanque/run can
  compute some extra data like state hashing without a round-trip
  (@ejgallego @gbdrt, #779)
• [petanque] New methods to hash proof states; use proof state hash
  by default in petanque agent (@ejgallego, @gbdrt, #808)
• [petanque] New shell method petanque/toc that returns a document
  outline in LSP-style (@ejgallego, #794)

0.2.0+8.18

CHANGES:

---

• [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
  dependency, and will greatly easy the development of tools that
  require AST manipulation (@ejgallego, #698)
• [fleche] Remove 8.16 compatibility layer (@ejgallego, #747)
• [fleche] Preserve view hint across document changes. With this
  change, we get local continuous checking mode when the view-port
  heuristic is enabled (@ejgallego, #748)
• [memo] More precise hashing for Coq states, this improves cache
  performance quite a bit (@ejgallego, #751)
• [fleche] Enable sharing of .vo file parsing. This enables better
  sharing, achieving an almost 50% memory reduction for example when
  opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh,
  #744)
• [memo] Provide API to query Hashtbl stats (@ejgallego, #753)
• [nix] Add pet-server deps to flake.nix (Léo Stefanesco, #754)
• [coq-lsp] Fix crash on --help option (Léo Stefanesco, @ejgallego,
  #754)
• [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
  #755, cc: #722, #725)
• [hover] Show input howto for unicode characters on hover
  (@ejgallego, Léo Stefanesco, #756)
• [lsp] [definition] Support for jump to definition across workspace
  files. The location information is obtained from .glob files, so
  it is often not perfect. (@ejgallego, #762, fixes #317)
• [lsp] [hover] Show full name and provenance of identifiers
  (@ejgallego, #762)
• [lsp] [definition] Try also to resolve and locate module imports
  (@ejgallego, #764)
• [code] Don't start server on extension activation, unless an editor
  we own is active. We also auto-start the server if a document that
  we own is opened later (@ejgallego, #758, fixes #750)
• [petanque] Allow init to be called multiple times (@ejgallego,
  @gbdrt, #766)
• [petanque] Faster query for goals status after run_tac
  (@ejgallego, #768)
• [petanque] New parameter pre_commands to start which allows
  instrumenting the goal before starting the proof (@ejgallego, Alex
  Sanchez-Stern #769)
• [petanque] New http_headers={yes,no} parameter for pet json
  shell, plus some improvements on protocol handling (@ejgallego,
  #770)
• [petanque] Make agent agnostic of environment, allowing embedding
  inside LSP (@ejgallego, #771)
• [diagnostics] Ensure extra diagnostics info is present in all
  errors, not only on those sentences that did parse successfully
  (@ejgallego, Diego Rivera, #772)
• [hover] New option show_universes_on_hover that will display
  universe data on hover (@ejgallego, @SkySkimmer, #666)
• [hover] New plugin unidiff that will elaborate a summary of
  universe data a file, in particular regarding universes added at
  Qed time (@ejgallego, #773)
• [fleche] Support meta-command Abort All (@ejgallego, #774, fixes
  #550)
• [petanque] Allow memoization control on petanque/run via a new
  parameter memo (@ejgallego, #780)
• [lsp] [petanque] Allow acces to petanque protocol from the lsp
  server (@ejgallego, #778)
• [petanque] Always initialize a workspace. This made pet crash if
  --root was not used and client didn't issue the optimal
  setWorkspace call (#782, @ejgallego, @gbdrt)
• [lsp] [petanque] New methods state/eq and state/hash; this
  allows clients to implement a client-side hash; equality is
  configurable with different methods; moreover, petanque/run can
  compute some extra data like state hashing without a round-trip
  (@ejgallego @gbdrt, #779)
• [petanque] New methods to hash proof states; use proof state hash
  by default in petanque agent (@ejgallego, @gbdrt, #808)
• [petanque] New shell method petanque/toc that returns a document
  outline in LSP-style (@ejgallego, #794)

0.2.0+8.17

CHANGES:

---

• [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
  dependency, and will greatly easy the development of tools that
  require AST manipulation (@ejgallego, #698)
• [fleche] Remove 8.16 compatibility layer (@ejgallego, #747)
• [fleche] Preserve view hint across document changes. With this
  change, we get local continuous checking mode when the view-port
  heuristic is enabled (@ejgallego, #748)
• [memo] More precise hashing for Coq states, this improves cache
  performance quite a bit (@ejgallego, #751)
• [fleche] Enable sharing of .vo file parsing. This enables better
  sharing, achieving an almost 50% memory reduction for example when
  opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh,
  #744)
• [memo] Provide API to query Hashtbl stats (@ejgallego, #753)
• [nix] Add pet-server deps to flake.nix (Léo Stefanesco, #754)
• [coq-lsp] Fix crash on --help option (Léo Stefanesco, @ejgallego,
  #754)
• [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
  #755, cc: #722, #725)
• [hover] Show input howto for unicode characters on hover
  (@ejgallego, Léo Stefanesco, #756)
• [lsp] [definition] Support for jump to definition across workspace
  files. The location information is obtained from .glob files, so
  it is often not perfect. (@ejgallego, #762, fixes #317)
• [lsp] [hover] Show full name and provenance of identifiers
  (@ejgallego, #762)
• [lsp] [definition] Try also to resolve and locate module imports
  (@ejgallego, #764)
• [code] Don't start server on extension activation, unless an editor
  we own is active. We also auto-start the server if a document that
  we own is opened later (@ejgallego, #758, fixes #750)
• [petanque] Allow init to be called multiple times (@ejgallego,
  @gbdrt, #766)
• [petanque] Faster query for goals status after run_tac
  (@ejgallego, #768)
• [petanque] New parameter pre_commands to start which allows
  instrumenting the goal before starting the proof (@ejgallego, Alex
  Sanchez-Stern #769)
• [petanque] New http_headers={yes,no} parameter for pet json
  shell, plus some improvements on protocol handling (@ejgallego,
  #770)
• [petanque] Make agent agnostic of environment, allowing embedding
  inside LSP (@ejgallego, #771)
• [diagnostics] Ensure extra diagnostics info is present in all
  errors, not only on those sentences that did parse successfully
  (@ejgallego, Diego Rivera, #772)
• [hover] New option show_universes_on_hover that will display
  universe data on hover (@ejgallego, @SkySkimmer, #666)
• [hover] New plugin unidiff that will elaborate a summary of
  universe data a file, in particular regarding universes added at
  Qed time (@ejgallego, #773)
• [fleche] Support meta-command Abort All (@ejgallego, #774, fixes
  #550)
• [petanque] Allow memoization control on petanque/run via a new
  parameter memo (@ejgallego, #780)
• [lsp] [petanque] Allow acces to petanque protocol from the lsp
  server (@ejgallego, #778)
• [petanque] Always initialize a workspace. This made pet crash if
  --root was not used and client didn't issue the optimal
  setWorkspace call (#782, @ejgallego, @gbdrt)
• [lsp] [petanque] New methods state/eq and state/hash; this
  allows clients to implement a client-side hash; equality is
  configurable with different methods; moreover, petanque/run can
  compute some extra data like state hashing without a round-trip
  (@ejgallego @gbdrt, #779)
• [petanque] New methods to hash proof states; use proof state hash
  by default in petanque agent (@ejgallego, @gbdrt, #808)
• [petanque] New shell method petanque/toc that returns a document
  outline in LSP-style (@ejgallego, #794)

0.1.9+8.19

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 m...

0.1.9+8.18

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 m...