Stream: Coq users

Topic: Jupyter/Notebook integration

view this post on Zulip Jason Qin (Dec 17 2022 at 08:42):

Does anyone know of any coq kernel implementations for jupyter or any notebook like apps? Or do people mostly just use CoqIDE or a regular IDE?

view this post on Zulip Karl Palmskog (Dec 17 2022 at 08:45):

See here:

Specifically, for Jupyter there is

Not listed is the recent

view this post on Zulip Karl Palmskog (Dec 17 2022 at 08:48):

in the recent survey, people reported using this

view this post on Zulip Jason Qin (Dec 17 2022 at 08:48):

:thumbs_up: Im using coq jupyter rn and its quite good, esp since its the same interface for many other langs like python and julia. The others I felt were kinda clunky

view this post on Zulip Julien Puydt (Dec 17 2022 at 10:48):

I just had a look at coq-jupyter with the in-browser test: one can run each cell, but I haven't found how one can step-run within the cells to see context and goals.

view this post on Zulip Théo Zimmermann (Dec 19 2022 at 09:54):

@Julien Puydt You can't AFAIK. The idea is rather that you put any important steps in separate cells so that you can keep the intermediate output displayed. When you are developing, if you deem that some steps are not important enough to deserve a new cell, you just add a new tactic to the current one and re-run it. coq_jupyter has sane defaults and when you do this it retracts the cell before replaying it (contrary to a notebook for a language like Python where the state is cumulative). Note that the state is still cumulative in the whole notebook and won't make sense anymore if you reorder cells or delete some of them. Notebooks can be confusing for reproducibility for that reason if you do not use them defensively. This is why a colleague of mine did not like the experience with coq_jupyter (comparing it to a return to coqtop-era). I disagree with this assessment, but YMMV.

view this post on Zulip Emilio Jesús Gallego Arias (Dec 19 2022 at 14:21):

coq-lsp does support markdown documents, and this is the way we are going in jsCoq too; it should be not too hard to support LSP new Notebook capabilities, but indeed, there are some UI issues w.r.t. interaction that I'm unsure how to approach; anyways, I'll be happy to help if someone would like to add NoteBookServerCapabilities to coq-lsp.

Last updated: Oct 04 2023 at 19:01 UTC