[new release] coq-lsp (0.2.3+9.0)

[ejgallego]

Language Server Protocol native server for Coq

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

CHANGES:

---

• [fleche] fix quick fixes for errors being lost due to incorrect
  handling of send_diags_extra_data (@ejgallego, [web worker] Allow users to select different Coq versions rocq-community/rocq-lsp#850)
• [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, [vscode] Syntax highlighting for Coq 8.17-8.20 rocq-community/rocq-lsp#872)
• [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, [vendor] Bump Coq rocq-community/rocq-lsp#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, [js worker] Update js_of_ocaml to 5.9.1 and Coq -> Roqc / stdlib split rocq-community/rocq-lsp#881)
• [js worker] Update stubs (@ejgallego, @hhugo, [js worker] Update js_of_ocaml to 5.9.1 and Coq -> Roqc / stdlib split rocq-community/rocq-lsp#881)
• [js worker] Fix build for Coq -> Rocq renaming and stdlib split
  (@ejgallego, [js worker] Update js_of_ocaml to 5.9.1 and Coq -> Roqc / stdlib split rocq-community/rocq-lsp#881)
• [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer,
  Adapt to coq/coq#19927 (coq-core renamed to rocq-runtime) rocq-community/rocq-lsp#883)
• [general] [js] Adapt to Rocq stdlib split (@ejgallego, [build] Adapt to Rocq stdlib split + fix setup-ocaml CI rocq-community/rocq-lsp#890)
• [ci] Bump setup-ocaml to v3 (@ejgallego, [build] Adapt to Rocq stdlib split + fix setup-ocaml CI rocq-community/rocq-lsp#890)
• [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, [ci] [windows] Try OPAM 2.2 for the Windows build rocq-community/rocq-lsp#815,
  [build] Adapt to Rocq stdlib split + fix setup-ocaml CI rocq-community/rocq-lsp#890)
• [petanque] petanque/start now fails when the theorem was parsed
  but not successfully executed (@ejgallego, reported by @gbdrt,
  [petanque] Fix petanque/start when a theorem is parsed but has errors rocq-community/rocq-lsp#901, fixes [petanque] Return error on start when there is no proof to build. rocq-community/rocq-lsp#886)
• [ci] Test Ocaml 5.3 (@ejgallego, [ci] Test OCaml 5.3 rocq-community/rocq-lsp#904)
• [js worker] Add Shachar Itzhaky's trampoline patch; this greatly
  reduces the Stack Overflow in the proof engine (@ejgallego,
  @corwin-of-amber, [build] [js] Add coq-waterproof to JS build. rocq-community/rocq-lsp#905)
• [js worker] [build] Include Coq WaterProof in the default Web
  Worker build (@ejgallego, waterproof team, [build] [js] Add coq-waterproof to JS build. rocq-community/rocq-lsp#905, closes [build] [js] Coq WaterProof build for coq-lsp.js  rocq-community/rocq-lsp#888)
• [vscode] [web] Fix web extension not exporting the coq-lsp
  extension API (@ejgallego, reported by @amblafont, [vscode] [web] Fix web extension not exporting the coq-lsp API rocq-community/rocq-lsp#911, fixes
  The web extension does not export any API rocq-community/rocq-lsp#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, [build] [general] Rename our internal Lsp library to Fleche_lsp rocq-community/rocq-lsp#912, fixes
  name conflict with the lsp package rocq-community/rocq-lsp#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, [coq] [workspace] Remove machinery for old-style manual ML path handling rocq-community/rocq-lsp#916)
• [lsp] [debug] Respect $/setTrace call , refactor logging system,
  and allow file logging of protocol traces again (@ejgallego, [lsp] Cleanup of LSP IO rocq-community/rocq-lsp#919,
  fixes [debug] [ui] Provide an easier way to output a protocol trace. rocq-community/rocq-lsp#868)
• [coq] Support Coq relocatable mode (@SkySkimmer, Adapt to coq/coq#19901 (relocatable mode) rocq-community/rocq-lsp#891)
• [ci] [deps] Remove support for OCaml 4.12 and 4.13, following
  upstream's Bump minimum ocaml version to 4.14.0 rocq-prover/rocq#20576 Note that these compiler versions have
  been unsupported for a long time, please upgrade (@ejgallego, [ci] [deps] Remove support for OCaml 4.12 and 4.13 rocq-community/rocq-lsp#951)
• [hover] New option show_state_hash_on_hover that displays state
  hash on hover for debug (@ejgallego, [hover] Improve API to enable/disable hover plugins rocq-community/rocq-lsp#954)
• [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023,
  thanks to Patrick Nicodemus for pointing out the outdated
  documentation (@ejgallego, [faq] Update FAQ for VsCoq 2 release. rocq-community/rocq-lsp#846, fixes Clarify the difference between VsCoq 1 and VsCoq 2 here? rocq-community/rocq-lsp#817)
• [vscode] [macos] Resolve keybinding conflict with Cmd+N and
  Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei
  Listochkin, VSCode extension keybindings shouldn't conflict with editor defaults. rocq-community/rocq-lsp#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, [rocq] Disable memprof-limits interruption backend by default rocq-community/rocq-lsp#957, fixes 0.2.0 crashes frequently rocq-community/rocq-lsp#857, reported by @dariusf,
  cc: [core] Improved state protection against memprof-limits interruptions 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, [controller] [lsp] Include Rocq feedback on request errors. rocq-community/rocq-lsp#959, [fleche] [lsp] Uniformize feedback type with message, bugfixes for #961 rocq-community/rocq-lsp#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, [petanque] Add feedback field to errors and Run_result.t rocq-community/rocq-lsp#960)
• [petanque] new get_state_at_pos and get_root_state calls, that
  allow to retrieve a petanque proof state from position
  (@JulesViennotFranca, @ejgallego, [petanque] Add get_state calls rocq-community/rocq-lsp#962)
• [doc] [petanque] Document petanque v1, improve readme (@ejgallego,
  [doc] [petanque] [readme] Document and version petanque, improve README. rocq-community/rocq-lsp#963)
• [plugin] [astdump] Make the JSON and SEXP output into a line per
  object by default (@blackbird1128, @ejgallego, [plugins] Fix the output of the AST dump plugin to be valid JSON rocq-community/rocq-lsp#874)
• [doc] [emacs] [protocol] Improve documentation for proof/goals,
  add link to official emacs mode by Josselin Poiret (@ejgallego,
  [doc] Some improvements to proof/goals doc, emacs link. rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: error field of proof/goals does not respect goal_after_tactic rocq-community/rocq-lsp#941)
• [goals] Include range in proof/goals answer. This is useful for
  clients willing to do highlighting (@ejgallego, @jpoiret, [goals] Include sentence range in proof/goals answer. rocq-community/rocq-lsp#970)

[ejgallego]

curl fails to get the source, this is strange, I can get it just fine using the same command :/

[ejgallego]

curl fails to get the source, this is strange, I can get it just fine using the same command :/

The exit code is 6, from the curl manual: "Could not resolve host. The given remote host could not be resolved."

That seems bizarre.

[raphael-proust]

@ejgallego there are occasional transient network issues in the CI, it could be that all the jobs started around the same time when there was some network general (not job-specific) network issue. I've restarted the jobs to see. (If it doesn't work we'll look into it more.)

[raphael-proust]

separate question: the coq.9.0 package were compatibility/transition package for coq→rocq, should there be a rocq-lsp package starting at version 9?

[raphael-proust]

opened ocurrent/opam-repo-ci#441 re: curl issues

[ejgallego]

Thanks a lot @raphael-proust ! Indeed the network problem seems to be there, I guess a DNS issue?

Windows CI works fine.

separate question: the coq.9.0 package were compatibility/transition package for coq→rocq, should there be a rocq-lsp package starting at version 9?

Due to compat constraints we will rename coq-lsp to rocq-lsp in the 0.3.x series.

[raphael-proust]

There are some curl issues, more likely opam issues actually because the tests do run successfully for the opam-2.0, opam-2.1, and opam-2.3 checks. This suggests a regression in opam-dev but possibly something else instead I'm not sure.

Anyway, I'm ok to merge this PR although do note that:

we are lacking tests for some architectures
we are lacking tests for some distributions

I don't think these tests are very important for this lsp plugin (unlikely to be plateform-specific bug) so I'm merging. @ejgallego don't hesitate to ping if you think that's the wrong move and it needs to be tested more widely.

[ejgallego]

Thanks a lot @raphael-proust , I do appreciate the quick help. I think the tests are not important.