Couple of shortcuts for Coqtail

Tags: / coq nvim vim /

A couple of shortcut key bindings that I use with nvim and Coqtail, a vim plugin to use coq interactively.

Of the user interfaces available for coq, I use:

No offense to emacs users, but I found it difficult to get used to the emacs way of doing things (except for table editing in org-mode, which I use often) and would rather stick with (n)vim.

That means Coqtail is the obvious choice.

I altered key bindings for two things in my nvim config:

Running commands

Coqtail is nice (thanks to Wolf Honore and others working on it!) but its default shortcuts with the <leader> key sometimes got in the way for me.

For example, when I do <leader>cc to start coq via Coqtail, if I'm a bit late to do the cc after the <leader>, the current line is deleted and I got to do undo.

Similar problems with some other shortcuts like:

Of course, the maximum delay for the '<leader> shortcuts' can be adjusted but I thought I could try something else.

I liked some of the shortcuts of emacs' proofgeneral mode.

And since vim makes limited use of control key, I thought it would be nice to have a similar key binding in vim with Coqtail. Like

and so used noremap to make the key bindings:

noremap <C-n> :CoqNext<CR>hh  " next line
noremap <C-p> :CoqUndo<CR>hh  " undo last line

I couldn't yet figure out why, but it seems that the <CR> at the end of the above two lines somehow causes the cursor to advance by two characters horizonatally. Hence the hh at the end to move the cursor back left by two character positions.

(I didn't delve into this, but please tell me if you know why this happens.)

Some alternative key bindings

  1. Change leader key

    The leader key (<Leader>) in nvim can be changed by setting the mapleader variable.

    For example, the following can be used to make Space as leader key:

    let g:mapleader = "\<Space>"

    (Got to use double quote and the backslash here for space. Single quote doesn't work.)

    And then you can do like

    • Space C-j: execute next command
    • Space C-k: retract one command

    (Used space as leader key just for example. I don't prefer to have Space as the leader key, though. 😅)

  2. Coqtail variables

    Coqtail also offers the following variables that can be used to set the key prefix just in the context of Coqtail:

    • g:coqtail_map_prefix
    • g:coqtail_imap_prefix

    We can do

    let coqtail_map_prefix = <c-c>

    Could also make the coqtail_map_prefix as g:coqtail_map_prefix. See this stackoverflow post.

    to modify the default shortcuts to things like

    • C-c C-j: execute next command
    • C-c C-k: retract one command

    See the Coqtail README.

Adding coq output as comment

Coq produces two kinds of output:

('Info' is termed 'response' in emacs proofgeneral mode.)

Figured it would be nice to have a way to add these output from coq as a comment within the source file itself.

Like the way alectryon does it but within the source itself and not as separate html.

There is an open issue at the Coqtail github repo regarding this where they mention a quick way to have this.

Like placing the following in the .vimrc / init.vim file:

function! InsertOutput(buffer)
    " Position cursor after last executed line
    CoqJumpToEnd

    " Get Info/Goal buffer contents
    let instrlst = getbufline(b:coqtail_panel_bufs[tolower(a:buffer)], 1, '$')

    " Make comment to output
    let outstrlst = ['(*', '#+BEGIN_OUTPUT (' . a:buffer . ')']
        \ + instrlst[:-2] + ['#+END_OUTPUT (' . a:buffer . ') *)']

    " Add comment to file
    call append('.', outstrlst)
endfunction

let @i = ":call InsertOutput('Info')^M"
let @g = ":call InsertOutput('Goal')^M"

(The ^M at the end of the last two lines is actually the code for the Enter key. You can type it in vim using its digraph: C-k CR.)

Thanks to Jaehwang Jerry Jung for suggesting this. 🙂

I inserted the command for that into two of vim registers and execute when needed with @<reg>.

@i to insert 'Info' and @g to insert 'Goal' output.

But this means you can't use those registers for anything else. There is probably a better way (but am sticking with this till I find one 😊).

An example on doing @i:

Check nat. <---
(*
#+BEGIN_OUTPUT (Info)
nat
     : Set
#+END_OUTPUT (Info) *)

where the <--- represents the last line executed by coq.

Another example:

Theorem plus_0_n : forall (n : nat), 0 + n = n.
Proof.
    intros n. <---
(*
#+BEGIN_OUTPUT (Goal)
1 subgoal

n : nat

========================= (1 / 1)

0 + n = n
#+END_OUTPUT (Goal) *)
    reflexivity.
Qed.