| Age | Commit message (Collapse) | Author |
|---|
|
They should not be necessary today as they date from the shareable
pre-artifact epoch, an incur in an slowdown.
|
|
|
|
This allows to use fixed commits and not just branches or tags.
We keep using git clone when $FORCE_GIT is set (for projects on
gforge.inria.fr and projects pulling dependencies through git submodules).
fiat-parsers also calls git submodule, but inside its own Makefile.
|
|
|
|
In the original Travis CI setup, the per-job time limit was an
issue. However, Gitlab has much improved this problem due to
a) Coq not being built for each contrib,
b) user-configurable time limit.
We thus disable the expensive builds from Travis:
`fiat-crypto`, `formal-topology`, `geocoq`, `iris-lambda-rust`,
`math-comp`, `unimath`, `vst`
and instruct Gitlab to build [`geocoq`, `math-comp`, `unimath`, `vst`]
in full.
We also update the `math-comp` script as the `odd-order` theorem lives
in a separate repository and it is a key CI case.
|
|
|
|
See also GeoCoq/GeoCoq#7.
|
|
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
```
|
|
|
|
We need to agree a bit more with upstream.
|
|
|
