On Thu, Nov 29, 2018 at 11:16 AM Emilio Jesús Gallego Arias <e...@x80.org> 
wrote:
> As of today, you have coq-serapi[1], which was specifically designed to
> make interaction with Emacs easy.

That helps a bit for some issues, but I think most of the bugs in the
async branch mostly relate to maintaining
unstated or unknown invariants in the implementation.

> Also, a LSP server for Coq is expected to appear very soon.

That would be a definite advance for all IDEs.

-- Paul
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to