GitLab

Iris can check (at least approximately) for new uses of -> in a pre-commit hook to enforce this style. This should save @robbertkrebbers several hours of writing "Please use Unicode →" in MRs.

Here's my attempt at this. To install, you need to copy this file to .git/hooks/pre-commit and make it executable.

This was tested on macOS with BSD grep, but it should be cross-platform.

#!/bin/bash

set -e
# redirect stdout to stderr
exec 1>&2

error() {
  echo -e "\033[31m$1\033[0m"
}
## Check for adding ASCII -> instead of Unicode →
# first filter to Coq files not containing "ascii"
if find . -name '*.v' -and -not -name '*ascii*' -print0 |\
  xargs -0 git diff --staged --unified=0 --             |\
	# only check additions, not deletions
	grep    '^\+.*->'                                   |\
	# skip lines that legitimately use -> in Ltac
	grep -v '\b(rewrite|destruct|iDestruct|iMod)\b.*->'
then
	error "Please use Unicode [→] instead of [->]."
	exit 1
fi

Note that this doesn't need to be perfect. You can always override the check with git commit --no-verify.

I can also add checks for \bexists\b, \bforall\b, and \bfun\b that should be replaced with their Unicode variants ∃, ∀, and λ.