diff options
| -rw-r--r-- | .travis.yml | 20 | ||||
| -rw-r--r-- | README.md | 2 | ||||
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 4 |
3 files changed, 21 insertions, 5 deletions
diff --git a/.travis.yml b/.travis.yml index 196f4b22ad..8d70e346ad 100644 --- a/.travis.yml +++ b/.travis.yml @@ -39,6 +39,7 @@ env: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" - TEST_TARGET="validate" TW="travis_wait" - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" + - TEST_TARGET="validate" COMPILER="4.05.0+flambda" CAMLP5_VER="7.01" NATIVE_COMP="no" EXTRA_CONF="-flambda-opts -O3" NATIVE_COMP="no" - TEST_TARGET="ci-bignums TIMED=1" - TEST_TARGET="ci-color TIMED=1" - TEST_TARGET="ci-compcert TIMED=1" @@ -103,6 +104,21 @@ matrix: - avsm packages: *extra-packages + # Full test-suite with flambda + - env: + - TEST_TARGET="test-suite" + - COMPILER="4.05.0+flambda" + - FINDLIB_VER="1.7.3" + - CAMLP5_VER="7.01" + - NATIVE_COMP="no" + - EXTRA_CONF="-coqide opt -with-doc yes -flambda-opts -O3" + - EXTRA_OPAM="lablgtk-extras hevea" + addons: + apt: + sources: + - avsm + packages: *extra-packages + # Ocaml warnings with two compilers - env: - TEST_TARGET="coqocaml" @@ -143,7 +159,7 @@ matrix: - NATIVE_COMP="no" - COQ_DEST="-local" before_install: - - brew update --debug --verbose + - brew update - brew install opam gnu-time - if: NOT (type = pull_request) @@ -157,7 +173,7 @@ matrix: - EXTRA_CONF="-coqide opt -warn-error" - EXTRA_OPAM="lablgtk-extras" before_install: - - brew update --debug --verbose + - brew update - brew install opam gnu-time gtk+ expat gtksourceview libxml2 gdk-pixbuf python3 - pip3 install macpack before_deploy: @@ -1,6 +1,6 @@ # Coq -[](https://travis-ci.org/coq/coq/builds) [](https://gitter.im/coq/coq) +[](https://travis-ci.org/coq/coq/builds) [](https://ci.appveyor.com/project/coq/coq/branch/master) [](https://gitter.im/coq/coq) Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 545846da58..e76f283706 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -76,8 +76,8 @@ ######################################################################## # CompCert ######################################################################## -: ${CompCert_CI_BRANCH:=less_init_plugins} -: ${CompCert_CI_GITURL:=https://github.com/letouzey/CompCert.git} +: ${CompCert_CI_BRANCH:=master} +: ${CompCert_CI_GITURL:=https://github.com/AbsInt/CompCert.git} ######################################################################## # VST |