diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-01 09:30:14 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-01 09:30:14 +0100 |
| commit | 565c2c2a56e118d9cf9b6b72b623055bcd68af60 (patch) | |
| tree | ec9267a3d090a256d859b6f1bf4f0ced0b09c5fd | |
| parent | 317a47249e666e2e11c6a8ac29f7c8370c861f8a (diff) | |
| parent | b16f9e8a17d2223e6045e57a11bef2aa44ffb6ff (diff) | |
Merge PR #6256: CI: better ocaml warning checks
| -rw-r--r-- | .gitlab-ci.yml | 2 | ||||
| -rw-r--r-- | .travis.yml | 13 | ||||
| -rw-r--r-- | Makefile.dev | 2 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 2 |
4 files changed, 10 insertions, 9 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index c0a01f3fd..20dac57a7 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -105,7 +105,7 @@ before_script: - set +e variables: &warnings-variables - EXTRA_CONF: "-native-compiler yes -coqide opt" + EXTRA_CONF: "-native-compiler yes -coqide byte -byte-only" EXTRA_PACKAGES: "$COQIDE_PACKAGES" EXTRA_OPAM: "$COQIDE_OPAM" diff --git a/.travis.yml b/.travis.yml index 1f6bb11e0..83a4e7fdd 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,6 +39,7 @@ env: - LABLGTK_BE="lablgtk.2.18.6 lablgtk-extras.1.6" - NATIVE_COMP="yes" - COQ_DEST="-local" + - MAIN_TARGET="world" # Main test suites matrix: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" @@ -139,8 +140,8 @@ matrix: # Ocaml warnings with two compilers - env: - - TEST_TARGET="coqocaml" - - EXTRA_CONF="-coqide opt -warn-error" + - MAIN_TARGET="coqocaml" + - EXTRA_CONF="-byte-only -coqide byte -warn-error" - EXTRA_OPAM="hevea ${LABLGTK}" # dummy target - BUILD_TARGET="clean" @@ -155,11 +156,11 @@ matrix: - libgtksourceview2.0-dev - env: - - TEST_TARGET="coqocaml" + - MAIN_TARGET="coqocaml" - COMPILER="${COMPILER_BE}" - FINDLIB_VER="${FINDLIB_VER_BE}" - CAMLP5_VER="${CAMLP5_VER_BE}" - - EXTRA_CONF="-coqide opt -warn-error" + - EXTRA_CONF="-byte-only -coqide byte -warn-error" - EXTRA_OPAM="num hevea ${LABLGTK_BE}" # dummy target - BUILD_TARGET="clean" @@ -224,11 +225,11 @@ script: - echo -en 'travis_fold:end:coq.config\\r' - echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r' -- make -j ${NJOBS} +- make -j ${NJOBS} ${MAIN_TARGET} - echo -en 'travis_fold:end:coq.build\\r' - echo 'Running tests...' && echo -en 'travis_fold:start:coq.test\\r' -- ${TW} make -j ${NJOBS} ${TEST_TARGET} +- if [ -n "${TEST_TARGET}" ]; then ${TW} make -j ${NJOBS} ${TEST_TARGET}; fi - echo -en 'travis_fold:end:coq.test\\r' - set +e diff --git a/Makefile.dev b/Makefile.dev index dc4ded397..d2a1e9235 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -98,7 +98,7 @@ pluginsopt: $(PLUGINSOPT) pluginsbyte: $(PLUGINS) # This should build all the ocaml code but not (most of) the .v files -coqocaml: tools coqbinaries pluginsopt coqide printers bin/votour +coqocaml: tools coqbinaries $(PLUGINSCMO:.cmo=$(DYNOBJ)) coqide printers bin/votour .PHONY: coqlight states miniopt minibyte pluginsopt pluginsbyte coqocaml diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index e9c0e171a..4e7d6b218 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -87,7 +87,7 @@ let call_compiler ?profile:(profile=false) ml_filename = [] in let flambda_args = - if Coq_config.caml_version_nums >= [4;3;0] then + if Coq_config.caml_version_nums >= [4;3;0] && Dynlink.is_native then (* We play safe for now, and use the native compiler with -Oclassic, however it is likely that `native_compute` users can benefit from tweaking here. |