Jason Qin (Dec 17 2022 at 08:42): 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?
Karl Palmskog (Dec 17 2022 at 08:45):See here: https://github.com/coq-community/awesome-coq#user-interfaces
Specifically, for Jupyter there is https://github.com/EugeneLoy/coq_jupyter
Not listed is the recent https://github.com/ejgallego/coq-lsp
Karl Palmskog (Dec 17 2022 at 08:48):in the recent survey, people reported using this
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
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.
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.
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