"Paul A. Steckler" <st...@stecksoft.com> writes: > 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.
Umm, I'm not sure I share that view, I'd dare to say that for a start the new protocol would allow to drop 90% of the code, and after all I don't see a reason things wouldn't work as long as you stay within the supported feature set. I think we have a good understanding on what the invariants are in the CoqAPI protocol, and so far there is only 1 known issue which IMO is not very important [`newtip` is not respected for certain combinations of commands inside proofs] Then of course you have bugs of the platform [Coq] itself, but now Maxime is working in trying to polish them out. Note that SerAPI does indeed try to workaround a few quirks of the STM so clients don't have to care; and it can do so with moderate success as it lives in the OCaml work. So far there has been some more serious battle testing of SerAPI by the proof engineering group, and apart from some issues with serialization the behavior seems to be pretty predictable. SerAPI is missing some critical piece of information tho: what ideal interface the Emacs people would like to have? For example, I have a branch where you can just send the full document over and over again and Coq will compute the diff and update the client about the result. [This is the seed for the LSP mode indeed] The branch is not yet public as sadly there are some platform problems that impede us to do this reliably yet, but we will get there soon I hope. As of today indeed you need to use `Add` and `Cancel` I'm much afraid. Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
