Alectryon for Rocq 9.0

[yforster]

Is there any hope that there will be Alectryon for Rocq 9.0? There seems to be no new maintainer for coq-serapi rocq-community/manifesto#160

[cpitclaudel]

Yep, it should be released this summer!
We're rebasing on LSP instead of SerAPI. I'll be at Rocq'n'share to wrap it up, hoping for a release soon after.

[Blaisorblade]

Any news on this issue?

[cpitclaudel]

Yes! The branch is nearly ready; @rtetley is wrapping up a patch at rocq-prover/vsrocq#1133 , I'm finishing the branch based on vscoq at https://github.com/cpitclaudel/alectryon/tree/rocq-lsp and @MathisBD is polishing up an alternative implementation based on coq-lsp . So I think we're on track!

[mattam82]

Ping :)

[TheoWinterhalter]

We've been discussing on Zulip (#Rocq users > Using Alectryon for Rocq) and now it seems to works mostly ok, but both the vsrocq and coqlsp drivers have bugs. My experience right now is that vsrocq works better (running it from the rocq-lsp branch 😅) as long as you don't indent your doc comments:

(*|
This is ok.
|*)
  (*|
  This is often not.
  |*)