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 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
for f in "$@"; do
  [ "${f:0:1}" == "/" ] || f="${cwd}/$f"

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.

Using holtmux in Non-Standard Heaps

For non-standard heaps the hol configuration file is not loaded, which will not set up hol for use with vim. The hol session needs to use ".../path/to/hol-config.sml";. As a workaround the following vim shortcut hC will copy that string into the clipboard, so it can be pasted into the hol session. The vim snippet (to be added to $HOLDIR/tools/vim/hol.src) assumes that the hol configuration is located as specified by the environment variable $HOL_CONFIG.

" copy the use-ing of the hol configuration into the clipboard
" in order to paste it into hol, and to get vimhol.sh/holtmux to work in
" non-standard heaps
nn <silent> <LocalLeader>C :let @+='Option.app use $ Process.getEnv "HOL_CONFIG";'<CR>