[meta] Put SerAPI in maintenance mode.

[ejgallego]

Thanks to everyone that helped and used this project for almost 7 years!

The following issues are solved by coq-lsp:

closes #252, closes #261, closes #234, closes #202, closes #117,
closes #49, closes #32, closes #26, closes #24, closes #21,
closes #18, closes #13

[cpitclaudel]

Exciting step! I guess I need to port Alectryon, but… do we really have feature parity between LSP and SerAPI? I would worry about these:

• Segmenting the document into sentences: is this capability available as a custom query in LSP?

• Push vs pull: Does the new LSP server have support for pull diagnostics? Otherwise LSP doesn't provide a way to know that you've received all diagnostics.

• Structured representation of goals: SerAPI goals were nicely structured; does our LSP server have the same thing?

[ejgallego]

SerAPI will be OK as long as the Coq API it uses (the STM) is still in Coq, the roadmap for that is not clear.

Actually most of the SerAPI API maps directly to coq-lsp, so if someone would be willing to port it the API could be kept even beyond Stm removal from Coq.

Segmenting the document into sentences: is this capability available as a custom query in LSP?

For now we only print this info as a debug information, but the request can be added easily, PR incoming.

Push vs pull: Does the new LSP server have support for pull diagnostics? Otherwise LSP doesn't provide a way to know that you've received all diagnostics.

Pull diagnostics are not yet implemented, but they are a priority and the checking engine supports them, main TODO is the LSP plumbing, will get to it soon I hope; also a range parameter has been approved for 3.18, so clients can request diagnostics for only a part of the buffer. Engine already does that (when you check for goals at point, it will just check the doc up to that point, then return the goals, then continue)

There is a hack in coq-lsp which is to query for info (or hover) etc... with the last point of the document, but indeed it is a hack, also you could use the fileProgress notification, but that's also a hack.

Structured representation of goals: SerAPI goals were nicely structured; does our LSP server have the same thing?

Yes, LSP server uses the same (a bit improved actually) Goal datatype, see https://github.com/ejgallego/coq-lsp/blob/main/etc/doc/PROTOCOL.md#goal-display

There are some other bits upcoming in PRs such as support for obligations (which tells you about holes in the document)

[cpitclaudel]

For now we only print this info as a debug information, but the request can be added easily, PR incoming.

Thanks!

use the fileProgress notification, but that's also a hack.

Ah, nice. It's one way to go at least :)

Yes, LSP server uses the same (a bit improved actually)

Excellent, thanks!