Add Emacs mode.

[arthuraa]

Currently this implements a single user-facing command, lsp-coq-proof/goals, which displays the current goals at point. I mostly created this PR as a means to get people together to decide what we want this mode to be -- I don't expect this to be merged right away necessarily. Here are some discussion topics:

• How do we test this/incorporate this into CI?
• How do we ensure that people can install this via package and melpa?
• What other commands and features do we want?
• Do we want to use this with its own major mode? Right now I am running this on top of Proof General's coq-mode.

[ejgallego]

Currently this implements a single user-facing command, lsp-coq-proof/goals, which displays the current goals at point. I mostly created this PR as a means to get people together to decide what we want this mode to be -- I don't expect this to be merged right away necessarily.

Thanks a lot @arthuraa ! That's indeed already pretty helpful IMHO. Regarding merging, IMHO we should do whatever is more convenient for us. I find organizing in Zulip works well, but whatever works best can be tried indeed.

• How do we test this/incorporate this into CI?
• How do we ensure that people can install this via package and melpa?

IMHO these two questions do belong together, I propose we follow standard practices for Melpa packages in terms of CI / packaing (c.f. https://github.com/melpa/melpa/blob/master/README.md#contributing).

For CI, we can add a new job as we have now for the VSCode client.

For releases, we should add a "publish to MELPA" step in addition to the current publish to OPAM and VSCode marketplace.

Note that opam has some Emacs packages (like tuareg) so we can also add the right dune rules to ensure coq-lsp opam package is installed in opam's emacs lib dir.

• What other commands and features do we want?

I think the main one is to implement the progress notification notification. Fortunately, we are compatible with Lean's format, so we should be able to use Lean's code for this.

The rest of interesting calls are within the LSP standard, so IMHO we don't need to do anything else.

Another thing to look into is server configuration, we can indeed see how emacs can expose server options; for VSCode, this is done in package.json.

• Do we want to use this with its own major mode? Right now I am running this on top of Proof General's coq-mode.

Good question! Maybe we should discuss with PG folks?

A lot of functionality PG provides is covered by LSP, but maybe not all?

I'll open a thread on Coq PG Zulip's

[ejgallego]

Thread: https://coq.zulipchat.com/#narrow/stream/304020-Proof-General-devs