From 54b9591a82889e3cdb31325e22c5af3e0e69e3df Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 9 Oct 2017 13:55:54 +0200
Subject: Add linter.

---
 .gitattributes      | 33 +++++++++++++++++++++++++++++++++
 .travis.yml         | 15 +++++++++++++++
 dev/lint-commits.sh | 32 ++++++++++++++++++++++++++++++++
 3 files changed, 80 insertions(+)
 create mode 100755 dev/lint-commits.sh

diff --git a/.gitattributes b/.gitattributes
index 00f78b4494..f2c096f2d6 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,3 +1,36 @@
 .gitattributes export-ignore
 .gitignore export-ignore
 .mailmap export-ignore
+
+*.asciidoc whitespace=trailing-space,tab-in-indent
+*.bat whitespace=cr-at-eol,trailing-space,tab-in-indent
+*.bib whitespace=trailing-space,tab-in-indent
+*.c whitespace=trailing-space,tab-in-indent
+*.css whitespace=trailing-space,tab-in-indent
+*.dtd whitespace=trailing-space,tab-in-indent
+*.el whitespace=trailing-space,tab-in-indent
+*.h whitespace=trailing-space,tab-in-indent
+*.html whitespace=trailing-space,tab-in-indent
+*.hva whitespace=trailing-space,tab-in-indent
+*.js whitespace=trailing-space,tab-in-indent
+*.json whitespace=trailing-space,tab-in-indent
+*.lang whitespace=trailing-space,tab-in-indent
+*.md whitespace=trailing-space,tab-in-indent
+*.merlin whitespace=trailing-space,tab-in-indent
+*.ml whitespace=trailing-space,tab-in-indent
+*.ml4 whitespace=trailing-space,tab-in-indent
+*.mli whitespace=trailing-space,tab-in-indent
+*.mll whitespace=trailing-space,tab-in-indent
+*.mllib whitespace=trailing-space,tab-in-indent
+*.mlp whitespace=trailing-space,tab-in-indent
+*.mlpack whitespace=trailing-space,tab-in-indent
+*.nsh whitespace=trailing-space,tab-in-indent
+*.nsi whitespace=trailing-space,tab-in-indent
+*.py whitespace=trailing-space,tab-in-indent
+*.sh whitespace=trailing-space,tab-in-indent
+*.sty whitespace=trailing-space,tab-in-indent
+*.tex whitespace=trailing-space,tab-in-indent
+*.txt whitespace=trailing-space,tab-in-indent
+*.v whitespace=trailing-space,tab-in-indent
+*.xml whitespace=trailing-space,tab-in-indent
+*.yml whitespace=trailing-space,tab-in-indent
diff --git a/.travis.yml b/.travis.yml
index 1a9f6964f7..4e937b50fa 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -135,6 +135,21 @@ matrix:
           - avsm
           packages: *coqide-packages
 
+    - if: type = pull_request
+      env:
+      - TEST_TARGET="lint"
+      install: []
+      before_script: []
+      addons:
+      apt:
+        sources: []
+        packages: []
+      script:
+        - CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
+        - PR_HEAD=${TRAVIS_COMMIT_RANGE##*...}
+        - MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD)
+        - dev/lint-commits.sh $MERGE_BASE $PR_HEAD
+
     - os: osx
       osx_image: xcode8.3
       env:
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
new file mode 100755
index 0000000000..eb12bc2273
--- /dev/null
+++ b/dev/lint-commits.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+
+# A script to check prettyness for a range of commits
+
+CALLNAME="$0"
+
+function usage
+{
+    >&2 echo "usage: $CALLNAME <commit> <commit>"
+    >&2 echo "The order of commits is as given to 'git diff'"
+}
+
+if [ "$#" != 2 ];
+then
+    usage
+    exit 1
+fi
+
+BASE_COMMIT="$1"
+HEAD_COMMIT="$2"
+
+# git diff --check
+# uses .gitattributes to know what to check
+if git diff --check "$BASE_COMMIT" "$HEAD_COMMIT";
+then
+    :
+else
+    >&2 echo "Whitespace errors!"
+    >&2 echo "Running 'git diff --check $BASE_COMMIT $HEAD_COMMIT'."
+    >&2 echo "If you use emacs, you can prevent this kind of error from reocurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
+    exit 1
+fi
-- 
cgit v1.2.3


From 4c954a3479e002d3a350c3094ae73e6ca5865202 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 24 Oct 2017 14:41:05 +0200
Subject: Put newlines at the end of files.

---
 dev/build/windows/MakeCoq_regtest_noproxy.bat | 4 ++--
 dev/build/windows/configure_profile.sh        | 2 +-
 dev/build/windows/patches_coq/ln.c            | 2 +-
 dev/nsis/FileAssociation.nsh                  | 2 +-
 doc/common/styles/html/simple/style.css       | 2 +-
 doc/refman/index.html                         | 2 +-
 test-suite/bugs/closed/5245.v                 | 2 +-
 test-suite/success/guard.v                    | 2 +-
 8 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/dev/build/windows/MakeCoq_regtest_noproxy.bat b/dev/build/windows/MakeCoq_regtest_noproxy.bat
index 7b17e721b3..7140a7c619 100644
--- a/dev/build/windows/MakeCoq_regtest_noproxy.bat
+++ b/dev/build/windows/MakeCoq_regtest_noproxy.bat
@@ -25,5 +25,5 @@ call MakeCoq_MinGW.bat ^
   -cygquiet=Y ^
   -destcyg   %ROOTPATH%\cygwin_coq64_85pl2_abs ^
   -destcoq   %ROOTPATH%\coq64_85pl2_abs
-
-pause
\ No newline at end of file
+
+pause
diff --git a/dev/build/windows/configure_profile.sh b/dev/build/windows/configure_profile.sh
index 0b61a31e7f..16c972e80c 100644
--- a/dev/build/windows/configure_profile.sh
+++ b/dev/build/windows/configure_profile.sh
@@ -40,4 +40,4 @@ if [ ! -f $donefile ] ; then
     echo unset OCAMLLIB >> $rcfile
 
     touch $donefile
-fi
\ No newline at end of file
+fi
diff --git a/dev/build/windows/patches_coq/ln.c b/dev/build/windows/patches_coq/ln.c
index 5e02c72bb7..41f64f98b2 100644
--- a/dev/build/windows/patches_coq/ln.c
+++ b/dev/build/windows/patches_coq/ln.c
@@ -134,4 +134,4 @@ int WINAPI WinMain( HINSTANCE hInstance, HINSTANCE hPrevInstance, LPSTR lpCmdLin
     
     // Everything is fine
     return 0;
-}
\ No newline at end of file
+}
diff --git a/dev/nsis/FileAssociation.nsh b/dev/nsis/FileAssociation.nsh
index b8c1e5ee78..71a9162efc 100644
--- a/dev/nsis/FileAssociation.nsh
+++ b/dev/nsis/FileAssociation.nsh
@@ -187,4 +187,4 @@ NoOwn:
   !verbose pop
 !macroend
  
-!endif # !FileAssociation_INCLUDED
\ No newline at end of file
+!endif # !FileAssociation_INCLUDED
diff --git a/doc/common/styles/html/simple/style.css b/doc/common/styles/html/simple/style.css
index 0b1e640b38..d1b2ce1112 100644
--- a/doc/common/styles/html/simple/style.css
+++ b/doc/common/styles/html/simple/style.css
@@ -10,4 +10,4 @@
     margin: 0pt;
     padding: .5ex 1em;
     list-style: none 
-}
\ No newline at end of file
+}
diff --git a/doc/refman/index.html b/doc/refman/index.html
index 9b5250abcb..b937350e6e 100644
--- a/doc/refman/index.html
+++ b/doc/refman/index.html
@@ -11,4 +11,4 @@
   <FRAME SRC="menu.html">
 </FRAMESET>
 
-</HTML>
\ No newline at end of file
+</HTML>
diff --git a/test-suite/bugs/closed/5245.v b/test-suite/bugs/closed/5245.v
index 77bf169e18..e5bca5b5e4 100644
--- a/test-suite/bugs/closed/5245.v
+++ b/test-suite/bugs/closed/5245.v
@@ -15,4 +15,4 @@ Undo.
 progress hnf; intros; exact eq_refl.
 Undo.
 unfold foo_rel. intros x. exact eq_refl.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v
index 83d47dc683..3a1c6dabeb 100644
--- a/test-suite/success/guard.v
+++ b/test-suite/success/guard.v
@@ -25,4 +25,4 @@ match f with
     match e in (_ = B) return (B -> foo A) -> nat with
     | eq_refl => fun (g' : nat -> foo A) => bar A e (g' O)
     end g
-end e.
\ No newline at end of file
+end e.
-- 
cgit v1.2.3


From d3de8fe500c736aa92aa87c9cd8b83fa4f44b7d8 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 24 Oct 2017 14:41:36 +0200
Subject: Linter: check that files end with newlines.

We use git check-attr to look at the same files as git diff --check.
---
 .travis.yml                          |  8 ++------
 dev/lint-repository.sh               | 28 ++++++++++++++++++++++++++++
 dev/tools/check-eof-newline.sh       |  9 +++++++++
 dev/tools/should-check-whitespace.sh |  5 +++++
 4 files changed, 44 insertions(+), 6 deletions(-)
 create mode 100755 dev/lint-repository.sh
 create mode 100755 dev/tools/check-eof-newline.sh
 create mode 100755 dev/tools/should-check-whitespace.sh

diff --git a/.travis.yml b/.travis.yml
index 4e937b50fa..c99a3db4ef 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -135,8 +135,7 @@ matrix:
           - avsm
           packages: *coqide-packages
 
-    - if: type = pull_request
-      env:
+    - env:
       - TEST_TARGET="lint"
       install: []
       before_script: []
@@ -145,10 +144,7 @@ matrix:
         sources: []
         packages: []
       script:
-        - CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
-        - PR_HEAD=${TRAVIS_COMMIT_RANGE##*...}
-        - MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD)
-        - dev/lint-commits.sh $MERGE_BASE $PR_HEAD
+        - dev/lint-repository.sh
 
     - os: osx
       osx_image: xcode8.3
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
new file mode 100755
index 0000000000..ecf7880e20
--- /dev/null
+++ b/dev/lint-repository.sh
@@ -0,0 +1,28 @@
+#!/usr/bin/env bash
+
+# A script to check prettyness over the repository.
+
+# lint-commits.sh seeks to prevent the worsening of already present
+# problems, such as tab indentation in ml files. lint-repository.sh
+# seeks to prevent the (re-)introduction of solved problems, such as
+# newlines at the end of .v files.
+
+CODE=0
+
+if [ "(" "-n" "${TRAVIS_PULL_REQUEST}" ")" "-a" "(" "${TRAVIS_PULL_REQUEST}" "!=" "false" ")" ];
+then
+    # Some problems are too widespread to fix in one commit, but we
+    # can still check that they don't worsen.
+    CUR_HEAD=${TRAVIS_COMMIT_RANGE%%...*}
+    PR_HEAD=${TRAVIS_COMMIT_RANGE##*...}
+    MERGE_BASE=$(git merge-base $CUR_HEAD $PR_HEAD)
+    dev/lint-commits.sh $MERGE_BASE $PR_HEAD || CODE=1
+fi
+
+# Check that the files with 'whitespace' gitattribute end in a newline.
+# xargs exit status is 123 if any file failed the test
+find . "(" -path ./.git -prune ")" -type f \
+-o "(" -exec dev/tools/should-check-whitespace.sh '{}' ';' ")" \
+-print0 | xargs -0 -L 1 dev/tools/check-eof-newline.sh || CODE=1
+
+exit $CODE
diff --git a/dev/tools/check-eof-newline.sh b/dev/tools/check-eof-newline.sh
new file mode 100755
index 0000000000..1c578c05ce
--- /dev/null
+++ b/dev/tools/check-eof-newline.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+if [ -z "$(tail -c 1 "$1")" ]
+then
+    exit 0
+else
+    echo "No newline at end of file $1!"
+    exit 1
+fi
diff --git a/dev/tools/should-check-whitespace.sh b/dev/tools/should-check-whitespace.sh
new file mode 100755
index 0000000000..8159506b41
--- /dev/null
+++ b/dev/tools/should-check-whitespace.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+
+# determine if a file has whitespace checking enabled in .gitattributes
+
+git check-attr whitespace -- "$1" | grep -q -v 'unspecified$'
-- 
cgit v1.2.3


From 7bd0fc03e5656e6672e8329b070ca9bda88d6b99 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 24 Oct 2017 16:32:44 +0200
Subject: Put linter at the top of the tests.

---
 .travis.yml | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/.travis.yml b/.travis.yml
index c99a3db4ef..22ae6b7aa1 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -64,6 +64,17 @@ env:
 matrix:
 
   include:
+    - env:
+      - TEST_TARGET="lint"
+      install: []
+      before_script: []
+      addons:
+      apt:
+        sources: []
+        packages: []
+      script:
+        - dev/lint-repository.sh
+
     # Full Coq test-suite with two compilers
     - env:
       - TEST_TARGET="test-suite"
@@ -135,17 +146,6 @@ matrix:
           - avsm
           packages: *coqide-packages
 
-    - env:
-      - TEST_TARGET="lint"
-      install: []
-      before_script: []
-      addons:
-      apt:
-        sources: []
-        packages: []
-      script:
-        - dev/lint-repository.sh
-
     - os: osx
       osx_image: xcode8.3
       env:
-- 
cgit v1.2.3