search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.74k stars 636 forks source link

LSP server support meta issue #9012

Closed maximedenes closed 1 year ago

maximedenes commented 5 years ago

This is a meta-issue to communicate around an on-going effort by @ejgallego, @gares, @siegebell, @vbgl and myself, trying to improve Coq's support for UI implementations.

The plan is to improve the STM API and provide an LSP server, probably based on https://github.com/rlepigre/lambdapi/tree/master/lp-lsp

We plan to connect it to @siegebell 's VsCoq client: https://github.com/siegebell/vscoq

Currently, @gares and I are working on #566 which should resolve blocking issues related to parsing state.

The corresponding project can be seen here: https://github.com/coq/coq/projects/30

herbelin commented 5 years ago

Thanks for the news.

Among the questions I have, I'd be interested in understanding how to organize the code implementing CoqIDE features such that it is reusable for LSP. For instance, if I want to implement a graphical "search" widget for both CoqIDE and LSP (or VsCoq) what parts of the feature can I factorize?

herbelin commented 5 years ago

See also some information on LSP and VScode at #7055.

carlpaten commented 5 years ago

I'd like to help with the LSP effort. Do you know of any relatively self-contained tasks that still need doing?

Zimmi48 commented 5 years ago

Indeed, it would be helpful to have some feedback on the current status of the effort. In particular, I recently read in SerAPI's Gitter room + on Twitter that @ejgallego has a branch implementing a working LSP protocol for Coq. It would helpful to share this branch with the world, even if in a completely unpolished state and with many unmerged dependencies, so that people can evaluate the work that has still to be done.

ejgallego commented 5 years ago

Hi folks, I will publish the branch soon, job interviews are keeping me too busy so sorry for the delay.

I'm afraid that until I finish the ongoing rework there is not a lot that can be parallelized, I am working on the base architecture [which is extremely tricky due to inter-process communication issues] and that indeed requires care. I won't publish the branch until I am not sure I am not going to rewrite the whole thing next day.

brendanzab commented 5 years ago

Just cross-linking the discussion here, which might be of interest: https://github.com/siegebell/vscoq/issues/167

I'd recommend posting public branches in general @ejgallego - sometimes people can give you advice that actually speeds stuff up! In saying that, I know it can be hard to do if you've been working on something for a while and it's still unfinished and unpolished. Anyway, good luck with the job hunt! 🙂

ejgallego commented 5 years ago

Thanks @brendanzab ; the branch is almost ready; indeed I am a fan of publishing branches early, however LSP + Coq is something many people has been looking forward to, so publishing unstable stuff may also make them lose a lot of time, in particular when the code is going to be fully rewritten.

Anyways that's a thing of the past, as the branch should appear very very soon [once I do a bit more of testing].

Zimmi48 commented 5 years ago

Thanks for the link @brendanzab! There is also an interesting discussion on Coq + esy in this thread.

strub commented 5 years ago

Is the branch published now?

ejgallego commented 5 years ago

Is the branch published now?

Not yet. It seems to me the project is dead.

maximedenes commented 5 years ago

@ejgallego Can you clarify why you think the project is dead? And if you plan to not work on it anymore, can you at least restore the repository we were collaborating on, before you closed it without notice? This seems very unprofessional to me.

carlpaten commented 4 years ago

So... If I were to invest in this, would my best bet be to start from scratch?

Zimmi48 commented 4 years ago

No. For the record, contrary to what was said here, the project is absolutely not dead. The long term plan has not changed and is still to improve Coq's internals to provide a native LSP server in Coq, which can be used in substitution of the XML protocol. On the other hand, the short term plan to provide VSCode support to all the users who ask for it is to revive the VSCoq extension, which is based on an intermediate server, that bridges the XML protocol with something that can be understood by VSCode. The revived repository is here: https://github.com/coq-community/vscoq. It has already been ported to support Coq 8.9+ and should be available in the VSCode marketplace pretty soon.

Zimmi48 commented 4 years ago

Quoting @palmskog, something that might be of interest:

have you seen this btw: https://github.com/nasa/vscode-pvs https://shemesh.larc.nasa.gov/people/cam/publications/vscode-pvs-draft.pdf

This adds to the existing VSCode support in Isabelle, Lean, LambdaPI (ex-Dedukti), and maybe others as well...

rgrinberg commented 4 years ago

The plan is to improve the STM API and provide an LSP server, probably based on rlepigre/lambdapi:lp-lsp@master

Another option is to provide it on top of the LSP library used to implement OCaml's lsp server: https://github.com/ocaml/ocaml-lsp/

It's hard to say which one is better, but our implementation already has users and is maturing rapidly. Of course I'm also not against joining forces with the LSP implementation of lambdapi.

Zimmi48 commented 4 years ago

FTR (and unrelated to the specific comment above) there was also a recent discussion about this on Coq's Discourse: https://coq.discourse.group/t/emacs-and-lsp-or-why-are-we-stuck-with-current-pg/524

fblanqui commented 4 years ago

Hello. Concerning Lambdapi, I just would like to mention that the correct URL is https://github.com/Deducteam/lambdapi .

ejgallego commented 4 years ago

Another option is to provide it on top of the LSP library used to implement OCaml's lsp server: https://github.com/ocaml/ocaml-lsp/

Indeed the plan on the LSP front is to re-use that library; the current implementation in lambapi is minimal.

What Coq is missing is something akin to merlin, we are working on that.

XVilka commented 3 years ago

Since it was mentioned here - ocaml-lsp got the first (1.0.0) release and on its way to opam repository.

ejgallego commented 1 year ago

I can indeed clarify why the project got stuck for a long time, and how it did resurrect:

I think with the release of coq-lsp 0.1.0 this issue can be closed; we are discussing how to better coordinate changes to Coq in other channels.

coq-lsp feedback can be provided here

Also note that coq-lsp is designed to be used by other systems implemented in OCaml beyond Coq, see https://github.com/ejgallego/coq-lsp/pull/66 for more information.

There is also an effort to update vsCoq to LSP , I don't have the right link at hand, I'll let those knowledgeable to post the right link.

herbelin commented 1 year ago

Thanks for the update and the good news. What I saw from coq-lsp is very nice.

(About better coordinating, I'm sure we'll make it!)

Zimmi48 commented 1 year ago

There is also an effort to update vsCoq to LSP , I don't have the right link at hand, I'll let those knowledgeable to post the right link.

Since you ask, the relevant link regarding VsCoq is https://github.com/coq-community/vscoq/wiki/VsCoq-1.0-Roadmap.