diff options
| author | Emilio Jesus Gallego Arias | 2017-02-07 03:31:18 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-02-07 13:42:35 +0100 |
| commit | 62b3f78ee8cb16fcaa95ba7051d050c0e2913018 (patch) | |
| tree | 3b3ece5e94066f890c0ea837828c469fb01367ab | |
| parent | 86f23d20af6444d2837dc3d74a0265f47e8a571c (diff) | |
[travis] Make v8.5 build again
We also remove PFsection6 from build as it seems to be too close.
| -rw-r--r-- | .travis.yml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/.travis.yml b/.travis.yml index 2a18a54..6cb52d9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -23,20 +23,20 @@ env: - TEST_TARGET="v8.6" - TEST_TARGET="trunk" -matrix: - allow_failures: - # v8.5 is too slow to build mathcomp - - env: TEST_TARGET="v8.5" +# matrix: +# allow_failures: + # v8.5 was too slow to build mathcomp + # - env: TEST_TARGET="v8.5" install: -- "[ -e .opam ] || opam init -j ${NJOBS} --compiler=${COMPILER} -n -y" +- opam init -j ${NJOBS} --compiler=${COMPILER} -n -y - eval $(opam config env) - opam config var root - opam install -j ${NJOBS} -y ocamlfind camlp5 ${EXTRA_OPAM} - opam list # We could do "opam install coq=${TEST_TARGET}" but not so sure how # that does work for trunk. -- git clone -b ${TEST_TARGET} git://scm.gforge.inria.fr/coq/coq.git coq-${TEST_TARGET} +- git clone --depth 1 -b ${TEST_TARGET} git://scm.gforge.inria.fr/coq/coq.git coq-${TEST_TARGET} - cd coq-${TEST_TARGET} - ./configure -native-compiler no -local -coqide no - make -j ${NJOBS} @@ -48,10 +48,12 @@ script: - cd mathcomp # We lack a few minutes to be able to build the whole theorem. - sed -i.bak '/stripped_odd_order_theorem/d' Make -- sed -i.bak '/PFsection7.v/d' Make -- sed -i.bak '/PFsection8.v/d' Make -- sed -i.bak '/PFsection9.v/d' Make +- sed -i.bak '/PFsection6\.v/d' Make +- sed -i.bak '/PFsection7\.v/d' Make +- sed -i.bak '/PFsection8\.v/d' Make +- sed -i.bak '/PFsection9\.v/d' Make - sed -i.bak '/PFsection1.\.v/d' Make +- "if [ ${TEST_TARGET} = \"v8.5\" ]; then sed -i.bak '/primproj\\.v/d' Make ; sed -i.bak '/odd_order/d' Make ; fi" - make Makefile.coq - make -f Makefile.coq -j ${NJOBS} all - echo -en 'travis_fold:end:mathcomp.build\\r' |