Jupyter Kernel for Coq

Hi, I’ve been developing Coq kernel for Jupyter notebooks for some time now and I think it is ready to be shared with community.

Kernel itself can be found here.

You can try online demo here.

What do you guys think? Is there something you’d like to see added/improved?


It’s very good. IMHO, it might be even a good idea to promote this on the main Coq site, to lower the participation bar. I know a lot of people tried CoCalc, but there is a free and open source alternative from the Jupyter creators - JupyterLab. See their documentation to learn more about its features. You can read their blogpost why it was created and that it is ready for the end users now. The only missing piece now is real time collaboration, which is currently being worked on.

Nextjournal also uses your kernel now by the way.

1 Like


Thank you for your feedback.

I’ll check what can be done to improve support for JupyterLab. Last time I checked it was usable but somewhat limited (with regards to rollbacks).

It looks like JupyterLab uses it’s own extensions and maybe I could use it to provide better experience.

Note the following issue if you would also like for Eugene’s Jupyter kernel to be installed by default in CoCalc: https://github.com/sagemathinc/cocalc/issues/2867