Clément Pit-Claudel <clement....@gmail.com> writes: > 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?
Indeed you can send the whole document if you want; diffs are an optimization. Here we follow LSP. > 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. When you send to SerAPI/Coq-lsp the server will just parse your input, checking is lazy and requires an explicit command. We may experiment with speculative checking in the future, but with the current architecture it will likely be too heavy. The design allows for it tho, one constraint is that we should be able to reuse the new architecture with multicore OCaml for example. [And in fact I have Coq running under multicore OCaml but unfortunately tactic execution is very far from becoming thread safe; who knows tho, if we are able to push a lot of PRs in 8.11 maybe we could make it work] > Also, can SerAPI answer e.g. completion queries while running tactics? Not in the current version but this will work correctly with the new document manager. [Barring the problem that Coq itself has terrible internal support for completion as of today] Cheers, E. _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
