Automatically enforce use of Unicode → instead of ASCII ->
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 λ
.