add nice Coq support (proof assistant)

[williamstein]

REQUESTED BY: Jinwoo Ye.

and i would be glad if you can provide Coq environment for reifying specification and realizing program that complies the specification in some day.

At least Coq is available on the command line, e.g.,

1. Click +New, then "Terminal".
2. Type something like "coqc f.coq", where f.coq is I guess a file.

We obviously need much better integration (more like with latex editing).

[slel]

See also previous discussion at #2635.

[Zimmi48]

Here is a summary of my exploration of using Coq in CoCalc:

1. You can use Coq with the Proof-General interface when loading Emacs in an X11 window. But there are a few caveats:

   • C-c C-RET (go to point) / C-c C-u (go back one step) work fine but C-c C-n (go forward one step) / C-c C-r (retract buffer) / C-c C-b (evaluate buffer) conflict with key bindings of my browser (Firefox). I don't think there is much that we can do about that.
   • You can also use the buttons of the Proof-General interface instead of the key bindings but when the button Next is grayed out because there is nothing new to process and you type a Coq sentence (ending with a dot) at the end of the buffer that should make this button usable again, but it isn't the case.

2. You should also be able to use the Proof-General interface in the terminal but, there, the C-c C-RET key binding doesn't work: Emacs says "C-c RET is undefined".

3. It would be nice to have native editor support like for Lean. Here is an interface that could serve of inspiration https://x80.org/collacoq/. The traditional way of communicating with Coq would be through coqtop (like Proof-General does) but a modern way would be through the SerAPI protocol (https://github.com/ejgallego/coq-serapi/). There is currently ongoing effort to provide native support for LSP (with extensions), see coq/coq#9012 but it will take a while to complete.

4. The available version of Coq is 8.6 (which is the one in Ubuntu / Debian Stable). Debian Unstable has now the latest version (8.9.0). It would be cool if it could be updated on CoCalc. See https://repology.org/metapackage/coq/versions.

5. I just discovered a Jupyter kernel for Coq (https://github.com/EugeneLoy/coq_jupyter). This is what prompted me to explore the Coq support in CoCalc.

   • I tested it in binder. It works well there (likely with Coq 8.6 given that it is installed through apt).
   • I have yet to test it locally with Coq 8.9.0.
   • It adds a "Rollback cell" button to the Jupyter notebook that is super important for the interaction with Coq (e.g. if you want to modify the proof you provide in a cell, then you should click rollaback before evaluating it again, otherwise the current state is not what you expect). This rollback button doesn't show up in CoCalc's Jupyter interface and, when switching to the standard interface, it even creates an error that is printed in a pop-up window.
   • That being said, I think that an even simpler interaction model would be to not have this button but automatically do the rollback when re-evaluating a cell. I want to try forking the Coq Jupyter kernel to test if that would work. In that case, it wouldn't be needed to make this button work in CoCalc.

6. It would be extra nice to support the Coq kernel in Sage worksheet as well (because then it would allow mixing exploration e.g. in Sage and proofs in Coq).

[williamstein]

• conflict with key bindings of my browser (Firefox). I don't think there is much that we can do about that.

On many OS's some browsers can be run pointed out a single URL in a special mode that allows cocalc to disable all those keybindings. E.g., if I type

google-chrome --app=https://cocalc.com

then use emacs in x11, I can hit control+N and control+p without making a new window or printing!

Here's me doing this in Crostini on my chromebook:

[Zimmi48]

Thanks for the tip!

[Zimmi48]

See also EugeneLoy/coq_jupyter#29.

[Zimmi48]

FTR version 1.5.0 of the Coq Jupyter kernel that was just released (https://github.com/EugeneLoy/coq_jupyter/releases/tag/v1.5.0) fixes the issue with the classic UI in the CoCalc Jupyter notebook. It would be nice to have this kernel installed by default, and also to update Coq to 8.9.0.

[slel]

One can now install coq-jupyter using Conda:

• https://github.com/conda-forge/coq-jupyter-feedstock

[jdchristensen]

In case it helps others, to use EugeneLoy's Coq jupyter kernel in CoCalc, I ran the following in a CoCalc terminal:

pip install coq-jupyter
python -m coq_jupyter.install

Then I was able to select the Coq kernel from the jupyter notebook Kernel menu.

It would be great if this was available by default.

[haraldschilly]

Thank's for pointing us to the python lib. I remember vaguely that I tried it without luck, but that was a long time ago. In any case, it will be installed with the next software update. What's missing is this rollback button. I guess you have to restart the kernel instead (there is this fast forward button to restart and re-eval all cells).

In case we ever get around implementing such a rollback button, is there somewhere an explanation what it actually does? I looked into that kernel.js file and found this:

roll_back_cell: function(cell) {
      $(cell.element[0]).find(".coq_kernel_roll_back_button").prop('disabled', true);

      self.kernel_comm.send({
        'comm_msg_type': 'roll_back',
        "execution_id": self.get_metadata(cell, "execution_id")
      });
    },

but I bet there are additional assumptions around this. I also saw a toggle for auto_roll_back, which modifies a cell's metadata.

[EugeneLoy]

@haraldschilly Hi.

What's missing is this rollback button. I guess you have to restart the kernel instead (there is this fast forward button to restart and re-eval all cells).

Yes, support for rollback button in default CoCalc ui is limited. This may be somewhat inconvenient but not breaking. Fortunately, there is a workaround: using classic ui. You can check out more detailed description of this here. (BTW, I guess I'll add this to documentation to make it more transparent to CoCalc users).

In case we ever get around implementing such a rollback button, is there somewhere an explanation what it actually does?

The main idea is as follows:

In Coq it is often convenient to backtrack to specific line of the script. In this case all the state that was accumulated since that line should be discarded. Note that this is different from workflow of, for example, python repl, where you only amend the state by feeding new lines to interpreter (state is never discarded).

Now, in coq-jupyter the idea behind "cells with auto rollback" and "rollback button" is to facilitate coq workflow and make cells work less like in python kernel (where every cell execution feeds code to repl thus amending state) and more like in CoqIDE (where you can re-evaluate (or rollback) cell and discard any state that was dependent on previous code executed in that cell).

In case we ever get around implementing such a rollback button [...] I looked into that kernel.js file and found this: [...] but I bet there are additional assumptions around this. I also saw a toggle for auto_roll_back, which modifies a cell's metadata.

The real show stopper for implementing rollback button is that default CoCalc ui does not load front-end extension part of kernel (kernel.js). Fortunately, I've managed to implement kernel in such a way that it will fallback to python-kernel-like cell behavior if kernel.js was ignored. Changes to cell metadata are specific to coq-kernel and are related to tracking cells in case kernel.js did load. I can elaborate more if this is really needed.

[haraldschilly]

hi @EugeneLoy ... thank you for the explanation. I'm exactly wondering how that metadata and rollback works under the hood. We could add those two additional buttons for notebooks where the coq language set, but we would need to know exactly what they do. e.g. I saw in the code that the rollback button sends roll_back to the kernel. Is that all? Part of the problem is that I don't know Coq and I've also not looked at the classic UI. So, sorry for talking to a bloody newbe ;-)

So, this would be mean to somehow re-implement kernel.js, or a minimal variation of it. It shouldn't be too hard, although I can't promise when we'll be able to do it. Maybe someone else wants to help as a summer project.

[EugeneLoy]

I'm exactly wondering how that metadata and rollback works under the hood. We could add those two additional buttons for notebooks where the coq language set, but we would need to know exactly what they do.

I'll post more detailed explanation sometime around this weekend but the broad picture is this:

Metadata related to coq_kernel is managed in a number of monkey-patched methods of CodeCell and OutputArea as well as by handling messages from kernel via comm.

When cell executes, execution_id is tracked and previous execution_id (if any) is also sent to kernel to perform rollback.

When rollback button is pressed, execution_id for the cell is sent to kernel through the comm for rollback.

Kernel can send updates through the comm to ui to update some of the cells (for example if rollback triggered for multiple cells).

There is also some redundancy related to fallback if kernel.js is ignored.

[EugeneLoy]

The following is more detailed explanation of how coq_kernel deals with rollbacks.

coq_kernel maintains association between frontend ui cell that was used to post code and state that was produced by execution of that code by kernel instance. This is needed to be able to "rollback" or "re-evaluate" cells (and as a result discard any relevant state that was produced by kernel instance by executing code of that cell before rollback). This is done through execution_id which is the same as message id of execution request.

There are number of messages that are sent from kernel instance to frontend ui:

• [K1] execute_result. This is a standard message that is sent when ui requests cell execution. The content contains both text/plain (rendered by cli console and current CoCalc) as well as text/html (rendered by classic ui). It also contains metadata with relevant state that kernel associates with the cell (note: meaning of coq_kernel_evaluated is: true if all the code in cell was evaluated without errors, false if there were errors in some of the lines of the cell, thus whole code in cell is treated as errored). CoCalc mostly implements this at the moment (ignores html output).
• [K2] update_display_data This is a standard message. In coq_kernel it is sent when cell gets rolled back. This can happen through [R1] re-evaluation of the cell when "auto rollback" is toggled, [R2] direct request through "rollback" button, [R3] when cell has to be rolled back as consequence of rollback of some other cell (triggered by [R1] or [R2]). The content of the message is the same as in [K1]. I think CoCalc implements this with same limitations as [K1] (ignores html output), although it is better to verify this.
• [K3] comm_msg/cell_state. coq_kernel-specific message. It is sent as a result of [R1], [R2] and [R3]. This message contains up-to-date state that kernel instance associates with cell.
• [K4] comm_msg/kernel_comm_opened. coq_kernel-specific message. It is sent when kernel.js counterpart connects to kernel. This message contains state that kernel instance associates with all cells it executed (history).

Note: [K3] and [K4] are handled by kernel.js and needed to provide best-effort to keep frontend cells in sync with kernel instance in case:

• multiple forntend instances connected to kernel instance (possibly at the same time)
• frontend loaded stale version of notebook
• [K2] was not handled/not supported by frontend

(some combination of situations above may occur when you simply reopen notebook tab).

Note: text/html sent by [K1] contains "rich cell output", that contains rollback controls, output and status message. Some of them may be present and\or hidden depending on success of code execution. Check out renderer for more details. Later on kernel.js is expected to update rich output as a result of [K2], [K3] and [K4].

The following messages are sent from frontend ui to kernel instance:

• [F1] execute_request. In addition to standard handling of cell execution kernel.js adds coq_kernel_roll_back_cell with execution_id of the code executed in that cell before (if "auto rollback" is toggled for that cell). This signals kernel that [R1] should be triggered. Also, message id of execute_request is associated with code executed in that cell and becomes current execution_id for that cell.
• [F2] comm_msg/roll_back. coq_kernel-specific message that is sent as a result of [R2].

Now, I can see few ways of implementing coq_kernel rollbacks in CoCalc.

0. Do nothing. [K1] is already implemented (and ignores text\html output) and [F1] works without extra patching done by kernel.js. This is sort of fallback mode where kernel works without rollbacks handled by kernel.

1. Implement [F1] as described above. Assuming [K2] is implemented in CoCalc, this should be 20% effort and provide 80% result. Remembering execution_id and sending it (if previous is present) as coq_kernel_roll_back_cell on cell execution will act as if cell has "auto rollback" toggled which is default behavior of coq_kernel anyway.

2. Implement handling text\html output in [K1] and [K2]. This will require CoCalc frontend to mimic what 'kernel.js' does (basically handling all described above).

3. If using text\html output in [K1] and [K2] is not an option then CoCalc frontend may implement handling rollback controls in it's own way, using [K2] [K3] [K4] to update cell outputs and [F2] to signal rollback.

Implementation gotcha: whatever strategy is picked, note that when cell gets copied in some way (dupplicate\split\etc) the metadata (mainly execution_id) should be wiped from duplicate to maintain identity of original cell.

I think this is the main gist. If someone is willing to implement this on CoCalc-side - just let me know and I can provide further assistance.