diff options
Diffstat (limited to '.gitlab-ci.yml')
| -rw-r--r-- | .gitlab-ci.yml | 38 |
1 files changed, 1 insertions, 37 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 0ad68b508..be19a93a3 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -71,7 +71,7 @@ after_script: - echo 'end:coq.clean' - echo 'start:coq.config' - - ./configure -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE" + - ./configure -warn-error yes -prefix "$(pwd)/_install_ci" ${COQ_EXTRA_CONF}"$COQ_EXTRA_CONF_QUOTE" - echo 'end:coq.config' - echo 'start:coq.build' @@ -88,28 +88,6 @@ after_script: - set +e -.warnings-template: &warnings-template - # keep warnings in test stage so we can test things even when warnings occur - stage: test - script: - - set -e - - - echo 'start:coq.clean' - - make clean # ensure that `make clean` works on a fresh clone - - echo 'end:coq.clean' - - - echo 'start:coq.config' - - ./configure -local ${COQ_EXTRA_CONF} - - echo 'end:coq.config' - - - echo 'start:coq.build' - - make -j "$NJOBS" coqocaml - - echo 'end:coq:build' - - - set +e - variables: &warnings-variables - COQ_EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only -warn-error yes" - # every non build job must set dependencies otherwise all build # artifacts are used together and we may get some random Coq. To that # purpose, we add a spurious dependency `not-a-real-job` that must be @@ -264,20 +242,6 @@ pkg:nix: paths: - nix-build-coq.drv-0/*/test-suite/logs -warnings:base: - <<: *warnings-template - -# warnings:32bit: -# <<: *warnings-template -# variables: -# <<: *warnings-variables - -warnings:edge: - <<: *warnings-template - variables: - <<: *warnings-variables - OPAM_SWITCH: edge - documentation: <<: *doc-template dependencies: |