From 8d2b88c80ec77090928a9da3d6b00e25a5ed6fb1 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 5 Jun 2019 09:58:07 +0200
Subject: CI: Test ml compilation of each commit in a PR in lint job

---
 .gitlab-ci.yml      | 10 +++-------
 dev/lint-commits.sh | 31 +++++++++++++++++++++++++------
 2 files changed, 28 insertions(+), 13 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1be10f91d0..8cf26ffaa6 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -295,16 +295,12 @@ windows32:
     - /^pr-.*$/
 
 lint:
-  image: docker:git
   stage: test
-  script:
-    - apk add bash
-    - dev/lint-repository.sh
+  script: dev/lint-repository.sh
   dependencies: []
-  before_script: []
   variables:
-    # we need an unknown amount of history for per-commit linting
-    GIT_DEPTH: ""
+    GIT_DEPTH: "" # we need an unknown amount of history for per-commit linting
+    OPAM_SWITCH: base
 
 pkg:opam:
   stage: test
diff --git a/dev/lint-commits.sh b/dev/lint-commits.sh
index 96c92e3162..539bb5f1f9 100755
--- a/dev/lint-commits.sh
+++ b/dev/lint-commits.sh
@@ -19,21 +19,40 @@ fi
 BASE_COMMIT="$1"
 HEAD_COMMIT="$2"
 
-bad=()
+bad_ws=()
+bad_compile=()
 while IFS= read -r commit; do
     echo Checking "$commit"
     # git diff --check
     # uses .gitattributes to know what to check
     if ! git diff --check "${commit}^" "$commit";
-    then
-        bad+=("$commit")
+    then bad_ws+=("$commit")
+    fi
+
+    if ! make -f Makefile.dune check
+    then bad_compile+=("$commit")
     fi
 done < <(git rev-list "$HEAD_COMMIT" --not "$BASE_COMMIT" --)
 
-if [ "${#bad[@]}" != 0 ]
+# report errors
+
+CODE=0
+
+if [ "${#bad_ws[@]}" != 0 ]
 then
     >&2 echo "Whitespace errors!"
-    >&2 echo "In commits ${bad[*]}"
+    >&2 echo "In commits ${bad_ws[*]}"
     >&2 echo "If you use emacs, you can prevent this kind of error from reoccurring by installing ws-butler and enabling ws-butler-convert-leading-tabs-or-spaces."
-    exit 1
+    >&2 echo
+    CODE=1
 fi
+
+if [ "${#bad_compile[@]}" != 0 ]
+then
+    >&2 echo "Compilation errors!"
+    >&2 echo "In commits ${bad_compile[*]}"
+    >&2 echo
+    CODE=1
+fi
+
+exit $CODE
-- 
cgit v1.2.3


From cc2a10f1cfed35cb1ef193d23144bb10b45bcf21 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 6 Jun 2019 15:56:35 +0200
Subject: Doc for per commit compile lint

---
 CONTRIBUTING.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index f0e17909c1..0d11d092ba 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -105,6 +105,12 @@ files end with newlines) is checked by the `lint` job on GitLab CI (using
 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`.
 
+Each commit in your pull request should compile (this makes bisecting
+easier). The `lint` job checks compilation of the OCaml files, please
+try to keep the rest of Coq in a functioning state as well.
+
+You may run the linter yourself with `dev/lint-repository.sh`.
+
 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.
-- 
cgit v1.2.3