aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/ci-bedrock2.sh
AgeCommit message (Collapse)Author
2020-11-20[CI] Deactivate native-compiler in some jobsPierre Roux
A few libraries in the CI don't compile with it (out of memory).
2019-11-27[ci] Split out the dependencies of fiat-cryptoJason Gross
2019-03-31Revert "iconv bedrock2 CI output to UTF-8"Jason Gross
This reverts commit 1eb8b9dc3ff0e464c9cd6c7f12a1c9db4fa57423. This commit is no longer necessary
2019-03-17iconv bedrock2 CI output to UTF-8Andres Erbsen
The timing diff script dies badly on non-utf8 input (https://github.com/coq/coq/issues/9767).
2019-02-09remove VERBOSE=1, gitlab log shows that `-async-proofs-tac-j 1` was indeed ↵Samuel Gruetter
passed https://gitlab.com/coq/coq/-/jobs/158737429
2019-02-08Workaround for CI not having enough RAM for bedrock2: `-async-proofs-tac-j 1`Samuel Gruetter
COQMF_ARGS is a bedrock2-specific name to pass extra arguments to coq_makefile, and we use VERBOSE=1 for better debuggability
2018-08-31Download tarball instead of cloning external projects (when $CI is set).Théo Zimmermann
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.
2018-06-27Add mit-plv/bedrock2-ci to CIAndres Erbsen
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:11:31 +0000