Merge PR #10309: CI: Test ml compilation of each commit in a PR in lint job

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego

3 files changed, 34 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/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.
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