Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in / Register
  • Iris Iris
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 169
    • Issues 169
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 24
    • Merge requests 24
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Iris
  • IrisIris
  • Issues
  • #308
Closed
Open
Issue created Apr 07, 2020 by Tej Chajed@tchajedMaintainer

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 λ.

Edited Apr 16, 2020 by Tej Chajed
Assignee
Assign to
Time tracking