On 2019-04-29 19:50, Emilio Jesús Gallego Arias wrote: > - updates are in the form of diffs sent to the server,
Hi Emilio, Can you say more about this part? Is the UI expected to compute diffs between two updates, or can it just send the whole document and leave update computation to SerAPI? One thing I worry about, too, is computation time when the user doesn't explicitly choose which part of the buffer is to be sent to Coq. As a concrete example, sometimes I write an expression with not enough explicit parameters, and that sends Coq's typeclass mechanism in a loop. I fear that if Coq always sees the full document, it may spend a lot of time doing useless computation. Also, can SerAPI answer e.g. completion queries while running tactics? Clément.
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
