[ANN] Coqoune

I am glad to announce the first release of Coqoune, a kakoune plugin for the Coq proof assistant.

Back to about three months ago kakoune had literally zero support for Coq… So I suppose few kakoune users use Coq, or even ever heard of it…The reason this needs to be a separate plugin rather than something in rc/filetype is that Coq (and in general proof assistants) needs more support than ordinary languages.

The story goes as follows. When you use a proof assistant, you write proofs interactively. That is , besides writing proof codes, you need to execute some commands from time to time, and see the current goal (what is left to be proved) interactively. The code-writing process and command-sending process in generally not synced, so one would need an extra mechanism of sending commands and getting the interactive feedback. A screenshot is worth a thousand words:

The bottom-left client (goal) and the bottom-right one (result, for miscellaneous information) will change interactively according to the sent commands (underlined part in the top client), which can be grown/shrunk through user commands.

As you can see, it is not that straightforward as syntax highlighting. Although most popular editors have Coq support to some extent, not all have even the minimal set of features — Coq is an expensive language to support. However I believe kakoune does not lack the ability to support complex editing tasks, but perhaps a large enough community to complete them, which can be solved as time goes on, hopefully. The following part of this post is some thoughts of me on the kakoune ecosystem during the development process.

Pros of kak

The first thing is the ability to write complex stuffs completely out of kakoune. Although I have used (tolerated) POSIX sh for coqoune (merely for portability), I can use any other languages, such as python, lua or OCaml (what Coq is written in). As a comparison, existing Coq plugins for other editors (emacs, VIM and VSCode) all use the editors’ main config languages (elisp, vimscript and js, in respect). Of course, one can write plugins for emacs, VIM and VSCode in other languages, too. But that can never be as natural as in kak. In fact, only a small (and relatively easy) portion of coqoune’s code is about interaction with kakoune. You can do basically everything through kak -p .

The biggest profit of this is the ability to rely on external tools. Coq plugins do command execution stuffs through a program provided by Coq, through a XML interface. Plugins written in elisp or vimscript would need to write (or bundle) xml-parsing stuffs, while I can use libxml2 to do that. Even with richness of features in mind, coqoune has the smallest code base among all Coq plugins.

Then comes to the part of user experiences. Besides the good deeds kak provides for editing the source, coqoune offers a unique feature of managing goal buffer via window manager or terminal multiplexer. So now I can use the same set of shortcuts everywhere, change the layout of these buffers freely, or even distribute these buffers on different monitors.

What I would like to have in kak

I am not sure if there is any way to do it now, but I would really like to have the ability to define user hooks and run them on demand. As mentioned above, coqoune lets one put different buffers in different windows. But manually getting the layout correct every time can be annoying, and it would be really great if I could define a hook on the creation of these buffers, and let the user fulfill how they would like to set up the layout.


Could a user hook just call a function, you define it for default case but the user can override it?

You had me at hello, now let’s see that coq.

All joking aside thanks for your work on this kak feature it’s a programming language I wish to explore and you have eased that burden. I agree with your sentiment on kakoune with a slight apprehension on the hook request as a wrestle between multiplexer and editor. Although on a project like this, I can see how it would have come to the rescue.

It was a pleasure to read your shell scripts, thanks again and looking forward to giving it a run at Xmas. Bye :wave:

As mentioned above, although it can be annoying to open several buffers every time, this method has its benefits, too.

The idealized way in my opinion actually requires some efforts from outside kak and coqoune. In my imagination, one can use features like i3’s layout saving/restoring to create a layout for their favorite way of putting the buffers, and then apply this pre-configured layout automatically inside hooks.

I am not writing a lot of Coq recently. But next time I do so, I’ll post my solution in the Config part of the README anyway. You also remind me of posting my own key-binding and init config as an example in the README, thanks.

That sounds workable. I’ll try that. Thanks.

User hooks are now in, hook global User blah ...; trigger-user-hook blah, this post led me to actually implement it.


This is awesome!!

I started to work on something like this a while back, but never got very far. I’m really happy to see this happen.

Off topic: Wow this is nice! Any chance we get next release soon?