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.
