Merge PR #8041: [ci] Remove warning jobs in favor of default `-warn-error yes`

3 files changed, 5 insertions, 69 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:
diff --git a/.travis.yml b/.travis.yml
index 3301d97ce..53fbe5821 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -164,36 +164,6 @@ matrix:
           - avsm
           packages: *extra-packages
 
-    # Ocaml warnings with two compilers
-    - if: NOT (type = pull_request)
-      env:
-      - MAIN_TARGET="coqocaml"
-      - EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
-      - EXTRA_OPAM="${LABLGTK}"
-      addons:
-        apt:
-          sources:
-          - avsm
-          packages: &coqide-packages
-          - opam
-          - aspcud
-          - libgtk2.0-dev
-          - libgtksourceview2.0-dev
-
-    - if: NOT (type = pull_request)
-      env:
-      - MAIN_TARGET="coqocaml"
-      - COMPILER="${COMPILER_BE}"
-      - FINDLIB_VER="${FINDLIB_VER_BE}"
-      - CAMLP5_VER="${CAMLP5_VER_BE}"
-      - EXTRA_CONF="-byte-only -coqide byte -warn-error yes"
-      - EXTRA_OPAM="${LABLGTK_BE}"
-      addons:
-        apt:
-          sources:
-          - avsm
-          packages: *coqide-packages
-
     - os: osx
       env:
       - TEST_TARGET="test-suite"
@@ -260,7 +230,7 @@ script:
 - echo -en 'travis_fold:end:coq.clean\\r'
 
 - echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r'
-- ./configure ${COQ_DEST} -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
+- ./configure ${COQ_DEST} -warn-error yes -native-compiler ${NATIVE_COMP} ${EXTRA_CONF}
 - echo -en 'travis_fold:end:coq.config\\r'
 
 - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r'
diff --git a/configure.ml b/configure.ml
index 194f47c49..3a98e8892 100644
--- a/configure.ml
+++ b/configure.ml
@@ -647,8 +647,10 @@ let camltag = match caml_version_list with
     48: implicit elimination of optional arguments: too common
     50: unexpected documentation comment: too common and annoying to avoid
     56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3
+    58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9
+    59: "potential assignment to a non-mutable value": See Coq's issue #8043
 *)
-let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50"
+let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59"
 let coq_warn_error =
     if !prefs.warn_error
     then "-warn-error +a"