ejgallego/coq-lsp 0.2.3+8.17

on GitHub

CHANGES:

• [fleche] fix quick fixes for errors being lost due to incorrect
  handling of send_diags_extra_data (@ejgallego, #850)
• [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, #872)
• [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, #879)
• [js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo
  Heuzard for longstanding continued support of the jsCoq and coq-lsp
  projects (@ejgallego, @hhugo, #881)
• [js worker] Update stubs (@ejgallego, @hhugo, #881)
• [js worker] Fix build for Coq -> Rocq renaming and stdlib split
  (@ejgallego, #881)
• [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
  #883)
• [general] [js] Adapt to Rocq stdlib split (@ejgallego, #890)
• [ci] Bump setup-ocaml to v3 (@ejgallego, #890)
• [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, #815,
  #890)
• [petanque] petanque/start now fails when the theorem was parsed
  but not successfully executed (@ejgallego, reported by @gbdrt,
  #901, fixes #886)
• [ci] Test Ocaml 5.3 (@ejgallego, #904)
• [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
  reduces the Stack Overflow in the proof engine (@ejgallego,
  @corwin-of-amber, #905)
• [js worker] [build] Include Coq WaterProof in the default Web
  Worker build (@ejgallego, waterproof team, #905, closes #888)
• [vscode] [web] Fix web extension not exporting the coq-lsp
  extension API (@ejgallego, reported by @amblafont, #911, fixes
  #877)
• [build] [general] Rename our internal Lsp library to
  Fleche_lsp; this should help avoiding conflicts with the OCaml
  lsp library (@ejgallego, reported by @blackbird1128, #912, fixes
  #861)
• [workspace] Remove support legacy ML-search path semantics. These
  were basically unused since Coq 8.16. As a consequence, coq-lsp /
  fcc don't accept the -I flag anymore, use OCAMLPATH or the
  --ocamlpath= option to pass extra findlib paths. We still
  respect the -I flag in _CoqMakefile (@ejgallego, #916)
• [lsp] [debug] Respect $/setTrace call , refactor logging system,
  and allow file logging of protocol traces again (@ejgallego, #919,
  fixes #868)
• [coq] Support Coq relocatable mode (@SkySkimmer, #891)
• [ci] [deps] Remove support for OCaml 4.12 and 4.13, following
  upstream's rocq-prover/rocq#20576 Note that these compiler versions have
  been unsupported for a long time, please upgrade (@ejgallego, #951)
• [hover] New option show_state_hash_on_hover that displays state
  hash on hover for debug (@ejgallego, #954)
• [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
  thanks to Patrick Nicodemus for pointing out the outdated
  documentation (@ejgallego, #846, fixes #817)
• [vscode] [macos] Resolve keybinding conflict with Cmd+N and
  Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
  Listochkin, #926)
• [rocq] [fleche] Disable memprof-limits interruption backend by
  default, as released Rocq versions are not safe yet. If you want to
  enable it, you can still do it with the --int_backend=Mp command
  line option (@ejgallego, #957, fixes #857, reported by @dariusf,
  cc: rocq-prover/rocq#19177)
• [lsp] [controller] Include Rocq feedback on request errors, using
  the optional data field. This is useful to still be able to
  obtain feedback messages such as debug messages even when a request
  fails. This also opens the door to better protocol handling and
  petanque integration (@ejgallego, #959, #961)
• [petanque] Add feedback field to Run_result.t, this is important
  for many use cases. We also return feedback on petanque errors.
  (@ejgallego, @JulesViennotFranca, #960)
• [petanque] new get_state_at_pos and get_root_state calls, that
  allow to retrieve a petanque proof state from position
  (@JulesViennotFranca, @ejgallego, #962)
• [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
  #963)
• [plugin] [astdump] Make the JSON and SEXP output into a line per
  object by default (@blackbird1128, @ejgallego, #874)
• [doc] [emacs] [protocol] Improve documentation for proof/goals,
  add link to official emacs mode by Josselin Poiret (@ejgallego,
  #969, thanks to @jpoiret, cc: #941)
• [goals] Include range in proof/goals answer. This is useful for
  clients willing to do highlighting (@ejgallego, @jpoiret, #970)