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