diff options
| -rw-r--r-- | .travis.yml | 27 | ||||
| -rw-r--r-- | README.ci | 77 |
2 files changed, 99 insertions, 5 deletions
diff --git a/.travis.yml b/.travis.yml index ab59cf6bf7..14573e2952 100644 --- a/.travis.yml +++ b/.travis.yml @@ -1,6 +1,7 @@ dist: trusty sudo: required -language: ocaml +# Until Ocaml becomes a language, we set a known one. +language: c cache: apt: true directories: @@ -14,8 +15,9 @@ addons: - aspcud env: global: - - NJOBS=1 - - COMPILER="4.02.3" + - NJOBS=2 + # system is == 4.02.3 + - COMPILER="system" # Main test suites matrix: - TEST_TARGET="validate" TW="travis_wait" @@ -24,7 +26,12 @@ env: - TEST_TARGET="contrib-compcert" matrix: - # Extra is Full COQ build and test-suite with two compilers + + allow_failures: + - env: TEST_TARGET="ci-cpdt" + + # Full Coq test-suite with two compilers + # [TODO: use yaml refs and avoid duplication for packages list] include: - env: - TEST_TARGET="test-suite" @@ -75,12 +82,22 @@ matrix: - imagemagick 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 camlp5 ocamlfind ${EXTRA_OPAM} - opam list + script: + +- echo 'Configuring Coq...' && echo -en 'travis_fold:start:coq.config\\r' - ./configure -local -usecamlp5 -native-compiler yes ${EXTRA_CONF} +- echo -en 'travis_fold:end:coq.config\\r' + +- echo 'Building Coq...' && echo -en 'travis_fold:start:coq.build\\r' - make -j ${NJOBS} +- 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} +- echo -en 'travis_fold:end:coq.test\\r' diff --git a/README.ci b/README.ci new file mode 100644 index 0000000000..ed2ba9126e --- /dev/null +++ b/README.ci @@ -0,0 +1,77 @@ +**WARNING:** This document is a work in progress and intended as a RFC. +If you are not a Coq Developer, don't follow this instructions yet. + +Introduction +============ + +The Coq Travis CI infrastructure is meant to provide lightweight +automatics testing of pull requests. + +More comprehensive testing is the responsability of Coq's [Jenkins CI +server](https://ci.inria.fr/coq/) see, [XXX: add document] for +instructions on how to add your development to Jenkins. + +How to submit your development for Coq Travis CI +================================================ + +Travis CI provides a convenient way to perform testing of Coq changes +versus a set of curated libraries. + +Are you an author of a Coq library who would be interested in having +the latest Coq changes validated against your development? + +If so, keep reading! Getting Coq changes tested against your library +is easy, all that you need to do is: + +1.- Put you development in a public repository tracking coq trunk. +2.- Make sure that your development builds in less than 35 minutes. +3.- Submit a PR adding you development. +4.- ? +5.- Profit! Your library is now part of Coq's continous integration! + +Note that by partipating in this program, you assume a reasonable +compromise to discuss and eventually integrate compatibility changes +upstream. + +Get in touch with us to discuss any special need your development may +have. + +Maintaining your contribution manually [current method] +====================================== + +To add your contribution to the Coq Travis CI set, add a script for +building your library to `tools/ci/`, update `.travis.yml` and +`Makefile.ci`. Then, submit a PR. + +Maintaining your contribution as an OPAM package [work in progress] [to be implemented] +================================================ + +You can also provide an opam package for your contribution XXX at +https://github.com/coq/opam-coq-archive + +Then, add a `ci-opam-XXX` target to the `.travis.yml` file, the +package XXX.dev will be tested against each Coq commit and pull +request. + +- TODO: The main question here is what to do with `.opam` caching. We + could disable it altogether, however this will have an impact. We + could install a dummy Coq package, but `coq-*` dependencies will be + botched too. Need to think more. + +PR Overlays [work in progress] [to be implemented] +=========== + +It is common for PR to break some of the external tests. To this +purpose, we provide a method for particular PR to overlay the +repositories of some of the tests so they can provide fixed +developments. + +The general idea is that the PR author will drop a file +`tools/ci/overlays/$branch.overlay` where branch name is taken from +`${TRAVIS_PULL_REQUEST_BRANCH:-$TRAVIS_BRANCH}` +that is to say, the name of the original branch for the PR. + +The `.overlay` file will contain a set of variables that will be used +to do the corresponding `opam pin` or to overload the corresponding +git repositories, etc... + |