diff options
| -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' |