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

1 files changed, 25 insertions, 6 deletions

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