From 202bb1e4d7c0fb3e55cc31ef4760c67985c9c10f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 29 Nov 2017 19:26:54 +0100 Subject: A pre-commit hook to magically fix whitespace issues. --- dev/tools/pre-commit | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100755 dev/tools/pre-commit (limited to 'dev/tools/pre-commit') diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit new file mode 100755 index 0000000000..7718b26d56 --- /dev/null +++ b/dev/tools/pre-commit @@ -0,0 +1,36 @@ +#!/bin/sh + +# Copy to .git/hooks/ to use. + +set -e + +# NB: even though we use --cached it seems to exit code 1 with +# unstaged whitespace errors. That just means they get fixed though. +if git diff-index --check --cached HEAD --quiet; +then + : +else + 1>&2 echo "Auto fixing whitespace issues..." + + TEMP=$(mktemp) + # We fix whitespace in the index and in the working tree + # separately to preserve non-added changes. + git diff-index -p --cached HEAD > "$TEMP" + git apply --cached -R "$TEMP" + git apply --cached --whitespace=fix "$TEMP" + + git diff-index -p HEAD > "$TEMP" + git apply -R "$TEMP" + git apply --whitespace=fix "$TEMP" + rm "$TEMP" + + # 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!" +fi -- cgit v1.2.3 From 95ee1fe61d3623b2d07f1806520de591536976f2 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 16 Jan 2018 15:14:55 +0100 Subject: pre-commit hook: fix whitespace error detection --quiet implies --exit-code --- dev/tools/pre-commit | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'dev/tools/pre-commit') diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index 7718b26d56..ce8bc67df2 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -4,9 +4,7 @@ set -e -# NB: even though we use --cached it seems to exit code 1 with -# unstaged whitespace errors. That just means they get fixed though. -if git diff-index --check --cached HEAD --quiet; +if git diff-index --check --cached HEAD >/dev/null 2>&1 ; then : else -- cgit v1.2.3 From d31777adb88eb5ba54f68ac7a4cb7a2a29c1fc20 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 16 Jan 2018 08:31:08 -0500 Subject: Auto-create .git/hooks/pre-commit on ./configure The hook created checks to see if dev/tools/pre-commit exists, and, if so, runs it. This way, we don't have to do any fancy logic to update the git pre-commit hook. The configure script never overwrites an existing precommit hook, so users can disable it by creating an empty pre-commit hook. The check for existence is so that if users check out an old version of Coq, attempting to commit won't give an error about non-existent files. --- dev/tools/pre-commit | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'dev/tools/pre-commit') diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index ce8bc67df2..59cc84856d 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -1,6 +1,7 @@ #!/bin/sh -# Copy to .git/hooks/ to use. +# configure automatically sets up a wrapper at .git/hooks/pre-commit +# which calls this script (if it exists). set -e -- cgit v1.2.3 From 8ab30d25b5ffc6a56e9ca41f446504bba4a726ad Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 16 Jan 2018 18:12:55 +0100 Subject: Have the pre-commit hook also fix end-of-file nl --- dev/tools/pre-commit | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'dev/tools/pre-commit') diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index 59cc84856d..0cd0a0b705 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -5,6 +5,17 @@ set -e +CODE=0 +git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix || CODE=1 + +if [ $CODE -ne 0 ] +then + 1>&2 echo "Some files had newline errors; they have been fixed in the working tree." + 1>&2 echo "Make sure to add them before committing." + 1>&2 echo "This may fix itself if you were using git commit -a, and you try again." + exit 1 +fi + if git diff-index --check --cached HEAD >/dev/null 2>&1 ; then : -- cgit v1.2.3 From 85bcd29052d30db75df5b8e8aeeb91b0327077f2 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 23 Jan 2018 16:36:25 +0100 Subject: pre-commit: add files after fixing ending newlines. --- dev/tools/pre-commit | 57 +++++++++++++++++++++++++++++++--------------------- 1 file changed, 34 insertions(+), 23 deletions(-) (limited to 'dev/tools/pre-commit') diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index 0cd0a0b705..c5f6868d15 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -5,34 +5,42 @@ set -e -CODE=0 -git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix || CODE=1 - -if [ $CODE -ne 0 ] -then - 1>&2 echo "Some files had newline errors; they have been fixed in the working tree." - 1>&2 echo "Make sure to add them before committing." - 1>&2 echo "This may fix itself if you were using git commit -a, and you try again." - exit 1 -fi - -if git diff-index --check --cached HEAD >/dev/null 2>&1 ; +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 - : -else 1>&2 echo "Auto fixing whitespace issues..." - TEMP=$(mktemp) # We fix whitespace in the index and in the working tree # separately to preserve non-added changes. - git diff-index -p --cached HEAD > "$TEMP" - git apply --cached -R "$TEMP" - git apply --cached --whitespace=fix "$TEMP" - - git diff-index -p HEAD > "$TEMP" - git apply -R "$TEMP" - git apply --whitespace=fix "$TEMP" - rm "$TEMP" + 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.)" + + 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 + git apply --cached --whitespace=fix "$index" + git apply --whitespace=fix "$index" + git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix + git add -u + + # reset work tree + git diff-index -p --cached HEAD > "$fixed_index" + git apply -R "$fixed_index" + + # Fix worktree + git apply --whitespace=fix "$tree" + git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix # Check that we did fix whitespace if ! git diff-index --check --cached HEAD; @@ -43,4 +51,7 @@ else exit 1 fi 1>&2 echo "Whitespace issues fixed!" + + # clean up temporary files + rm "$index" "$tree" "$fixed_index" fi -- cgit v1.2.3 From 8cefdd3289776ed58199e5f608802546d6681eef Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 8 Feb 2018 17:13:12 +0100 Subject: pre-commit: fail gracefully if fixing whitespace removes all changes --- dev/tools/pre-commit | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'dev/tools/pre-commit') diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index c5f6868d15..656455aee9 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -36,12 +36,23 @@ then # reset work tree git diff-index -p --cached HEAD > "$fixed_index" - git apply -R "$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 git apply --whitespace=fix "$tree" git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix + 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 -- cgit v1.2.3 From aab9a48b16ffbc6b697da39d314298b692447b72 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 8 Feb 2018 17:13:49 +0100 Subject: pre-commit: nicer messages --- dev/tools/pre-commit | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'dev/tools/pre-commit') diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit index 656455aee9..c9cdee84ab 100755 --- a/dev/tools/pre-commit +++ b/dev/tools/pre-commit @@ -18,6 +18,7 @@ then 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" @@ -29,10 +30,12 @@ then # 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" + 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" @@ -44,8 +47,10 @@ then 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 -- cgit v1.2.3