HOL4 and vim wrapped in tmux

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 closed, the fifo pipe is deleted (by the session-closed tmux hook). 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. The readline wrapper rlwrap enriches the interaction with the hol REPL. (However, using readline versions strictly larger than version 8.0 is not recommended as the output gets partially scrambled.) For convenience prefix key followed by Ctrl-q ends the session also triggering the fifo pipe deletion.

#!/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="$(mktemp -u -p "${XDG_RUNTIME_DIR:-/tmp}" "hol-XXXXXXXXXX")"
test -p "$VIMHOL_FIFO" || mkfifo "$VIMHOL_FIFO"

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" rlwrap $HOLDIR/bin/hol \; \
  split-window -b -h env VIMHOL_FIFO="$VIMHOL_FIFO" \
    "${EDITOR:-vim}" "${files[@]}" \; \
  set-hook -g session-closed "run-shell 'rm -f \"$VIMHOL_FIFO\"'" \; \
  bind-key C-q confirm-before -p "kill-session #S? (y/n)" kill-session \; \
  set-option status off

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.