HOL4 and vim wrapped in tmux

Hosting hol inside a vim terminal buffer is part of the HOL4 vim mode. This requires that vim (or neovim) supports terminal buffers, which is the case if the following vim command prints 1:

:echoerr 0 < exists(':terminal')

For old versions of vim without this feature the following approach for using HOL4 with vim is recommended.

For testing the vim plugin in isolation run:

export HOLDIR="..."
export HOL_CONFIG="$HOLDIR/tools/vim/hol-config.sml" 
unset VIMINIT
vim --clean \
  --cmd "source $HOLDIR/tools/vim/filetype.vim" \
  "$HOLDIR/src/coalgebras/llistScript.sml"

For not loosing a goal state when e.g. the ssh connection terminates, one may run HOL4 and vim (with HOL vim mode) side by side in a tmux session.

Save the below script as holtmux within $PATH and for example run

holtmux "$HOLDIR"/src/coalgebras/*Script.sml

to open a fresh hol session within "$HOLDIR"/src/coalgebras, opening all *Script.sml files in your editor.

The script sets up a tmux session with side by side vim and hol connected by a fresh shared VIMHOL_FIFO pipe. When the tmux session is quit (by prefix key followed by Ctrl-q) the fifo pipe is deleted. The optional arguments are the files to edit with $EDITOR, which may be vim. The tmux session’s working directory is that of the first file and defaults to the current working directory.

#!/usr/bin/env bash
# start a new hol tmux session with a fresh shared fifo
#
# arguments: [files...]

# get absolute pathnames of the argument files
cwd="$(pwd)"
files=()
for f in "$@"; do
  [ "${f:0:1}" == "/" ] || f="${cwd}/$f"
  files+=("$f")
done

VIMHOL_FIFO="$(env TMPDIR="${XDG_RUNTIME_DIR:-/tmp}" mktemp -t "hol-XXXXXXXXXX")"
test -p "$VIMHOL_FIFO" || mkfifo "$VIMHOL_FIFO"

# disables startup message via: vim --cmd 'set shortmess+=at'
tmux \
  new-session \
    -c "$(echo "$@" | xargs --no-run-if-empty dirname \
      | cat - <(pwd) | head -n 1)" \
    -s "$(basename "$VIMHOL_FIFO")" \
    env VIMHOL_FIFO="$VIMHOL_FIFO" $HOLDIR/bin/hol \; \
  split-window -b -h env VIMHOL_FIFO="$VIMHOL_FIFO" \
    "${EDITOR:-vim}" --cmd 'set shortmess+=at' "${files[@]}" \; \
  bind-key C-q confirm-before -p "kill-session '#S'? (y/n)" "kill-session; run-shell 'rm -f \"$VIMHOL_FIFO\"'"

If the command echo -n | xargs --no-run-if-empty echo produces an error, then you probably do not have xargs from the GNU coreutils. In that case you may replace xargs --no-run-if-empty dirname with xargs dirname 2> /dev/null.

Remote Pair-Programming

For remote pair-programming the above script can be used with tmate instant terminal sharing. If tmate is installed, one may redefine tmux as the tmate executable.

function tmux() {
  env LC_ALL=en_US.UTF-8 TERM=xterm-256color tmate "$@"
}

When the holtmux script is prepended by the previous lines and run, the command tmate show-messages will print both a read-only and a writable connection string, that can be shared with a pair-programming partner.