Move lint job to gitlab

This changes the semantics a bit since we don't have
TRAVIS_COMMIT_RANGE anymore, instead we do per-commit linting for the
commits since the last merge commit.

4 files changed, 28 insertions, 33 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 108ecb5a04..596b51c3eb 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -260,6 +260,18 @@ windows32:
   except:
     - /^pr-.*$/
 
+lint:
+  image: docker:git
+  stage: test
+  script:
+    - apk add bash
+    - dev/lint-repository.sh
+  dependencies: []
+  before_script: []
+  variables:
+    # we need an unknown amount of history for per-commit linting
+    GIT_DEPTH: ""
+
 pkg:opam:
   stage: test
   # OPAM will build out-of-tree so no point in importing artifacts
diff --git a/.travis.yml b/.travis.yml
index 02b94f4a8e..855d36048d 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -28,17 +28,6 @@ env:
 
 matrix:
   include:
-    - env:
-      - TEST_TARGET="lint"
-      install: []
-      before_script: []
-      addons:
-      apt:
-        sources: []
-        packages: []
-      script:
-        - dev/lint-repository.sh
-
     - os: osx
       env:
       - TEST_TARGET="test-suite"
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index fa8962a06f..6663fbecf8 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -10,12 +10,14 @@ We are currently running tests on the following platforms:
 - GitLab CI is the main CI platform. It tests the compilation of Coq,
   of the documentation, and of CoqIDE on Linux with several versions
   of OCaml and with warnings as errors; it runs the test-suite and
-  tests the compilation of several external developments.
+  tests the compilation of several external developments. It also runs
+  a linter that checks whitespace discipline. A [pre-commit
+  hook](../tools/pre-commit) is automatically installed by
+  `./configure`. It should allow complying with this discipline
+  without pain.
 
 - Travis CI is used to test the compilation of Coq and run the test-suite on
-  macOS. It also runs a linter that checks whitespace discipline. A
-  [pre-commit hook](../tools/pre-commit) is automatically installed by
-  `./configure`. It should allow complying with this discipline without pain.
+  macOS.
 
 - AppVeyor is used to test the compilation of Coq and run the test-suite on
   Windows.
diff --git a/dev/lint-repository.sh b/dev/lint-repository.sh
index cd09b6d305..f588c20d02 100755
--- a/dev/lint-repository.sh
+++ b/dev/lint-repository.sh
@@ -4,33 +4,25 @@
 
 # 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.
+# also 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}" ] && [ "${TRAVIS_PULL_REQUEST}" != false ];
-then
-    # skip PRs from before the linter existed
-    if [ -z "$(git ls-tree --name-only "${TRAVIS_PULL_REQUEST_SHA}" dev/lint-commits.sh)" ];
-    then
-        1>&2 echo "Linting skipped: pull request older than the linter."
-        exit 0
-    fi
-
-    # 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
+# We assume that all merge commits are from the main branch
+# For Coq it is extremely rare for this assumption to be broken
+read -r base < <(git log -n 1 --merges --pretty='format:%H')
+head=$(git rev-parse HEAD)
+
+dev/lint-commits.sh "$base" "$head" || CODE=1
 
 # Check that the files with 'whitespace' gitattribute end in a newline.
 # xargs exit status is 123 if any file failed the test
+echo Checking end of file newlines
 find . "(" -path ./.git -prune ")" -o -type f -print0 |
     xargs -0 dev/tools/check-eof-newline.sh || CODE=1
 
+echo Checking overlays
 dev/tools/check-overlays.sh || CODE=1
 
 exit $CODE