Sounds really exciting!

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]

Hi, I'm just curious if there's any reason one cannot leverage work done on integrating ocaml with jupyter. That project appears to have implemented their own zeromq interface. I should add I am no expert in ocaml/coq and my knowledge of zeromq is minimal (coming from a python background).

@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 to tweak Coq upstream itself so clients such as SerAPI have a better time interacting with it]

Any help here will be more than welcome!

Thanks for the info @ejgallego. If I can help, I will; although, initially only from a testing perspective.

There is a better (and more modern) implementation of OCaml kernel for Jupyter by the way : https://github.com/akabe/ocaml-jupyter

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 's OCaml bindings.

How are you planning to handle backtracking? Will it be more OCaml-style (redefinitions override previous definitions?)

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 Coq maintains an internal document representation, that is synchronized with the Jupyter document, so indeed certain changes may force invalidation, etc... We will see how well it fits, but in principle, adding an already existing definition would error. Until the new document model can land in Coq, I will use a compat layer that should take care of the most pressing subjects.

p.s: IMVHO the word "backtracking" applied to Coq documents used incorrectly, as the usual meaning is in the context of proof search.

We will see how well it fits, but in principle, adding an already existing definition would error.

OK :)

p.s: IMVHO the word "backtracking" applied to Coq documents used incorrectly, as the usual meaning is in the context of proof search.

I tend to use both the algorithmic sense and the usual one, "reverse one's previous action or opinion."

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 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 kernels is better done in Python; thus if we would complete the Python interface that could significantly help this issue.

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

Jupyter protocol is for now not planned, in favor of coq-lsp