Emilio Jesús Gallego Arias

Hi @gares, thanks for the information; but note than in the SerAPI protocol all the messages (except StmAdd for now) are not "synchronous" by design, that is to say, the...

Some more discussion on ZeroMQ in Ocaml here: https://sympa.inria.fr/sympa/arc/caml-list/2016-07/msg00181.html [unfortunately, the ocaml mailing list is not accessible to google]

@bsdz indeed that is the plan; I guess we are all just short on time / working on other stuff [in my case I am using my free time trying...

Thanks @XVilka , the info is really appreciated.

For those interested, we plan to work on the first prototype at the Coq Implementors Workshop 2018 if I can finally attend. We will use the SerAPI toplevel + @akabe...

> How are you planning to handle backtracking? Will it be more OCaml-style (redefinitions override previous definitions?) There is no notion of "backtracking" in the Coq document model, but rather...

Lately I tend to prefer the model of "updating the document" to "reversing a concrete edit or checking action".

> I saw the Python interface issue is linked to this. Sorry if this a naive question, but how is this issue related to it? I feel like implementing Jupyter...

cc: https://github.com/EugeneLoy/coq_jupyter

@Ptival out of curiosity, which command produced that output?