Hi folks, I thought I'd give an update on what has been going on w.r.t. SerAPI and its successor.
First, we added a bit of documentation, it is not a wonder, and moreover, it will change, but here it is: http://ejgallego.github.io/coq-serapi/priv-serapi/Serapi_protocol/ The main change is that SerAPI will converge to something pretty much isomorphic to LSP with some extensions for proving. There will be more news about this in the summer, but I don't expect that clients supporting SerAPI today would have to do any significant change if implementing the recommended architecture. Recommended implementation architecture: ---------------------------------------- For SerAPI / Coq-LSP, the recommended implementation architecture is: - the document is considered as a whole unit, - updates are in the form of diffs sent to the server, - sentences are identified by their position in the buffer, - all meta-info [goals, etc...] is functional and must be queried for. As of now, SerAPI clients have a slightly harder time as they must keep the document as a list of sentences and they also have to maintain a table position to sentence id; this will be lifted soon. Best regards, Emilio _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
