diff options
| author | Gaëtan Gilbert | 2019-06-05 09:58:07 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-06-06 17:59:07 +0200 |
| commit | 8d2b88c80ec77090928a9da3d6b00e25a5ed6fb1 (patch) | |
| tree | a9704c7b12081688b8dce597a33fae2b67fb7ec6 | |
| parent | 90c1084ba489415f8df588c43e088491bc6be450 (diff) | |
CI: Test ml compilation of each commit in a PR in lint job
| -rw-r--r-- | .gitlab-ci.yml | 10 | ||||
| -rwxr-xr-x | 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 |