Merge PR #6283: A pre-commit hook to magically fix whitespace issues.

4 files changed, 120 insertions, 2 deletions

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 1a769333c..74a138f14 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -32,6 +32,8 @@ If your pull request fixes a bug, please consider adding a regression test as we
 
 Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes.
 
+Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by Travis (using `git diff --check`). We ship a [`dev/tools/pre-commit`](/dev/tools/pre-commit) git hook which fixes these errors at commit time. `configure` automatically sets you up to use it, unless you already have a hook at `.git/hooks/pre-commit`.
+
 Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests.
 
 - [needs: rebase](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22%20) indicates the PR should be rebased on top of the latest `master` branch. See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`.
diff --git a/configure.ml b/configure.ml
index 9992e03b8..69db9407a 100644
--- a/configure.ml
+++ b/configure.ml
@@ -451,6 +451,22 @@ let vcs =
   else if dir_exists "{arch}" then "gnuarch"
   else "none"
 
+(** * Git Precommit Hook *)
+let _ =
+  let f = ".git/hooks/pre-commit" in
+  if vcs = "git" && dir_exists ".git/hooks" && not (Sys.file_exists f) then begin
+    printf "Creating pre-commit hook in %s\n" f;
+    let o = open_out f in
+    let pr s = fprintf o s in
+    pr "#!/bin/sh\n";
+    pr "\n";
+    pr "if [ -x dev/tools/pre-commit ]; then\n";
+    pr "    exec dev/tools/pre-commit\n";
+    pr "fi\n";
+    close_out o;
+    Unix.chmod f 0o775
+  end
+
 (** * Browser command *)
 
 let browser =
diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh
index 9e4c8661d..e244d9ab8 100755
--- a/dev/tools/check-eof-newline.sh
+++ b/dev/tools/check-eof-newline.sh
@@ -1,13 +1,40 @@
 #!/usr/bin/env bash
 
+# Usage: check-eof-newline.sh [--fix] FILES...
+# Detect missing end of file newlines for FILES.
+# Files are skipped if untracked by git and depending on gitattributes.
+# With --fix, automatically append a newline.
+# Exit status:
+# Without --fix: 1 if any file had a missing newline, 0 otherwise.
+# With --fix: 1 if any non writable file had a missing newline, 0 otherwise.
+
+FIX=
+if [ "$1" = --fix ];
+then
+   FIX=1
+   shift
+fi
+
 CODE=0
 for f in "$@"; do
     if git ls-files --error-unmatch "$f" >/dev/null 2>&1 && \
            git check-attr whitespace -- "$f" | grep -q -v -e 'unset$' -e 'unspecified$' && \
            [ -n "$(tail -c 1 "$f")" ]
     then
-        echo "No newline at end of file $f!"
-        CODE=1
+        if [ -n "$FIX" ];
+        then
+            if [ -w "$f" ];
+            then
+                echo >> "$f"
+                echo "Newline appended to file $f!"
+            else
+                echo "File $f is missing a newline and not writable!"
+                CODE=1
+            fi
+        else
+            echo "No newline at end of file $f!"
+            CODE=1
+        fi
     fi
 done
 
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
new file mode 100755
index 000000000..c9cdee84a
--- /dev/null
+++ b/dev/tools/pre-commit
@@ -0,0 +1,73 @@
+#!/bin/sh
+
+# configure automatically sets up a wrapper at .git/hooks/pre-commit
+# which calls this script (if it exists).
+
+set -e
+
+if ! git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh ||
+        ! git diff-index --check --cached HEAD >/dev/null 2>&1 ;
+then
+    1>&2 echo "Auto fixing whitespace issues..."
+
+    # We fix whitespace in the index and in the working tree
+    # separately to preserve non-added changes.
+    index=$(mktemp "git-fix-ws-index.XXXXX")
+    fixed_index=$(mktemp "git-fix-ws-index-fixed.XXXXX")
+    tree=$(mktemp "git-fix-ws-tree.XXXXX")
+    1>&2 echo "Patches are saved in '$index', '$fixed_index' and '$tree'."
+    1>&2 echo "If an error destroys your changes you can recover using them."
+    1>&2 echo "(The files are cleaned up on success.)"
+    1>&2 echo #newline
+
+    git diff-index -p --cached HEAD > "$index"
+    git diff-index -p HEAD > "$tree"
+
+    # reset work tree and index
+    # NB: untracked files which were not added are untouched
+    git apply --cached -R "$index"
+    git apply -R "$tree"
+
+    # Fix index
+    # For end of file newlines we must go through the worktree
+    1>&2 echo "Fixing staged changes..."
+    git apply --cached --whitespace=fix "$index"
+    git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself
+    git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
+    git add -u
+    1>&2 echo #newline
+
+    # reset work tree
+    git diff-index -p --cached HEAD > "$fixed_index"
+    # If all changes were bad whitespace changes the patch is empty
+    # making git fail. Don't fail now: we fix the worktree first.
+    if [ -s "$fixed_index" ]
+    then
+        git apply -R "$fixed_index"
+    fi
+
+    # Fix worktree
+    1>&2 echo "Fixing unstaged changes..."
+    git apply --whitespace=fix "$tree"
+    git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
+    1>&2 echo #newline
+
+    if ! [ -s "$fixed_index" ]
+    then
+        1>&2 echo "No changes after fixing whitespace issues!"
+        exit 1
+    fi
+
+    # Check that we did fix whitespace
+    if ! git diff-index --check --cached HEAD;
+    then
+        1>&2 echo "Auto-fixing whitespace failed: errors remain."
+        1>&2 echo "This may fix itself if you try again."
+        1>&2 echo "(Consider whether the number of errors decreases after each run.)"
+        exit 1
+    fi
+    1>&2 echo "Whitespace issues fixed!"
+
+    # clean up temporary files
+    rm "$index" "$tree" "$fixed_index"
+fi