aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/ci-compcert.sh
Commit message (Collapse)AuthorAge
* [ci] [docker] Pin specific versions of OPAM CI dependencies.Gravatar Emilio Jesus Gallego Arias2018-06-06
| | | | | | | | | | | | | Packages such as `menhir` or `elpi` are fragile w.r.t. updates, so allowing a non-deterministic install in the Dockefile seems risky. We have found trouble with Menhir in the past. We thus specify a concrete version for all `CI_OPAM` packages. cc: https://github.com/AbsInt/CompCert/issues/234 We also add remove `hevea` from `apt` dependencies as it hasn't been needed since #7466 and add `texlive-science` which is needed to build the `source-doc` target due to the `textgreek` package being used.
* [ci] Temporal fix for CompCertGravatar Emilio Jesus Gallego Arias2018-06-06
| | | | https://github.com/AbsInt/CompCert/issues/234
* [gitlab] [circleci] Use a Custom Docker Image as base CI setup.Gravatar Emilio Jesus Gallego Arias2018-05-05
| | | | | | | | | | | | | | | | | | | | We provide a custom `Dockerfile` for Coq's CI system, based on `ubuntu:bionic`. The image includes the required set of packages and OPAM switches. This greatly simplifies the Gitlab and Circle scripts, at the cost of having to push a Docker build for them to depend on. Travis is not included in this PR as it requires significant more refactoring due to lack of native Docker support. This is work in progress but ready, a build hook is used so the image is properly tagged in the Docker autobuilder. We need to improve the autobuilder setup but this last point requires some design on how to trigger it. Fixes #7383
* Improve shell scriptsGravatar zapashcanon2018-04-05
|
* Put default value for NJOBS in ci-common.Gravatar Gaëtan Gilbert2018-01-30
|
* Revert "[ci] Temporal workaround for checker non-backwards compatible change."Gravatar Théo Zimmermann2017-12-12
| | | | This reverts commit 5d4cf69a3d7d472b54b5decc8400164b87e9a73f.
* [ci] Temporal workaround for checker non-backwards compatible change.Gravatar Emilio Jesus Gallego Arias2017-12-10
|
* [ci] Test coqchk on the CompCert target.Gravatar Théo Zimmermann2017-11-30
|
* [travis] Remove CompCert version check hack.Gravatar Emilio Jesus Gallego Arias2017-07-05
| | | | | We now pass `-ignore-coq-version` to CompCert's configure (cf AbsInt/CompCert#188) , thanks to @xavierleroy .
* Remove -j ${NJOBS} from make invocations in the ciGravatar Jason Gross2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | According to https://www.gnu.org/software/make/manual/html_node/Options_002fRecursion.html#Options_002fRecursion it's not necessary, because we pass `-j ${NJOBS}` to the top-level `make` invocation in `.travis.yml`. Additionally, explicitly passing `-j` in, e.g., fiat-crypto, results in error messages such as ``` make[2]: *** write jobserver: Bad file descriptor. Stop. make[2]: *** Waiting for unfinished jobs.... make[2]: *** write jobserver: Bad file descriptor. Stop. make[1]: *** [coqprime] Error 2 make[1]: INTERNAL: Exiting with 1 jobserver tokens available; should be 2! make[1]: Leaving directory `/home/travis/build/JasonGross/coq/_build_ci/fiat-c ``` because the `-j` on the `make` in the `ci-fiat-crypto.sh` script disables jobserver mode, and the submake in fiat-crypto to make coqprime does not explicitly pass `-j`, and so reenables jobserver mode, and then `make` gets very confused. Commit made with ```bash cd dev/ci git grep --name-only -- 'make -j ${NJOBS}' | xargs sed s'/make -j \${NJOBS}/make/g' -i git grep --name-only -- 'make -f Makefile.coq -j ${NJOBS}' | xargs sed s'/make -f Makefile.coq -j \${NJOBS}/make -f Makefile.coq/g' -i ```
* [travis] [8.6.only] Backport latest changes from trunk.Gravatar Emilio Jesus Gallego Arias2017-03-22
|
* [travis] Backport trunk's travis support.Gravatar Emilio Jesus Gallego Arias2017-03-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 09:07:10 +0000