aboutsummaryrefslogtreecommitdiff
path: root/.gitlab-ci.yml
AgeCommit message (Collapse)Author
2021-02-26CI Windows: adjust branch name to Coq Platform branch renamingMichael Soegtrop
2021-02-16Only run windows job when WINDOWS=enabledGaëtan Gilbert
This seems to have been missed in https://github.com/coq/coq/pull/13598 (16cd0d5cfc0c4702b8220dad8e91f31a89d904ba)
2021-02-11[ci] elpi 1.13.0Enrico Tassi
2021-02-03CI: Switch coqhammer job to edge ocamlGaëtan Gilbert
This fixes CI from their using the Stdlib module.
2021-01-05[ci] windows job based on the platformEnrico Tassi
2020-12-26Set the locale in Docker so Python's default output encoding is utf-8Jim Fehrle
2020-12-02gitlab CI: remove redundant "dependencies" infoGaëtan Gilbert
When we started using "needs" for the acyclic graph scheduling we needed to duplicate dependencies and needs (I forgot if it was documented or just buggy). Nowadays gitlab doc https://docs.gitlab.com/ee/ci/yaml/#needs says >In GitLab 12.6 and later, you can’t combine the dependencies keyword with needs to control artifact downloads in jobs. dependencies is still valid in jobs that do not use needs. Some jobs in stage-1 had "dependencies: []" without a corresponding "needs", not sure why as the only job in a previous stage is docker-boot which has no artifacts to skip. We don't want "needs: []" as that would fail to wait for the docker image, so we just have nothing instead.
2020-11-30[ci] add job for gappaEnrico Tassi
2020-11-30[docker] install boost, mpfr, flex, bison, autoconf-archiveEnrico Tassi
2020-11-26CI: Use hash of dockerfile in CACHEKEYGaëtan Gilbert
Checked by the linter so we don't forget to update it. Also checked by before_script so we don't run jobs for nothing.
2020-11-26Merge PR #13467: [ci] add job for intervalcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: silene
2020-11-26[ci] coquelicot, depend on ssr properEnrico Tassi
2020-11-26[ci] separate oddorder and fourcolor from mathcompEnrico Tassi
In this way interval does not have to wait too much
2020-11-26[ci] bump elpi to 1.12.0Enrico Tassi
2020-11-26[ci] add job for intervalEnrico Tassi
2020-11-25[docker] don't install ocamlformatEnrico Tassi
2020-11-25[ci] make compcert use flocq and menhirEnrico Tassi
2020-11-25[ci] job for menhirEnrico Tassi
2020-11-20Build all_stdlib.v in test suite makefileGaëtan Gilbert
instead of recursive make
2020-10-23Force-delete pr branches.Théo Zimmermann
Fixup #13050.
2020-10-12elpi 1.11.4Enrico Tassi
2020-09-22Merge PR #13061: fix build:quick and build:base+async artifactscoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-22Merge PR #13050: [ci/gitlab/cachix] Avoid running in trouble when calling ↵coqbot-app[bot]
git fetch --unshallow Reviewed-by: SkySkimmer
2020-09-21fix build:quick and build:base+async artifactsGaëtan Gilbert
We put dmesg.txt in the artifact path for all build-template users, but only these 2 jobs produce it to avoid uploading unused data (see discussion in #13043).
2020-09-18Merge PR #13043: [ci] call dmesg after quick/async jobs to detect OOMcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-18[ci] [dmesg] save as artifactEnrico Tassi
2020-09-17[ci/gitlab/cachix] Avoid running in trouble when calling git fetch --unshallow.Théo Zimmermann
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
After #8743 we don't depend on `num` anymore in the codebase; thus we drop the dependency. This could create problems for plugins relying on this implicit linking.
2020-09-17Merge PR #13024: [CI] Always upload artifactscoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-17[ci] call dmesg after quick/async jobs to detect OOMEnrico Tassi
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58
2020-09-14[CI] Always upload artifactsJason Gross
In order to support the workflow where coqbot automatically turns failing CI jobs into minimized examples for the test-suite easily (https://github.com/coq/bot/issues/107), we want to be able to get all of the .v files and all of the generated .vo and .glob files in the artifact, even when the build fails.
2020-09-14[ci] [docker] Up testing to OCaml 4.11.1Emilio Jesus Gallego Arias
- `odoc` must be bumped to support 4.11
2020-09-02CI: build Iris examples instead of lambda-RustRalf Jung
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-08-25Move bench job definition to its own fileGaëtan Gilbert
This focuses review requests to bench-maintainers instead of sharing with ci-maintainers
2020-08-25Merge PR #12882: Perform a few tweaks to make the bench script work properly.coqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: ppedrot
2020-08-25Merge PR #12798: Change OUnit package name to ounit2.coqbot-app[bot]
Reviewed-by: ejgallego
2020-08-25Merge PR #12870: CI: stop testing 4.11+trunkcoqbot-app[bot]
Reviewed-by: ejgallego
2020-08-24Bench: artifact logsGaëtan Gilbert
2020-08-24Perform a few tweaks to make the bench script work properly.Pierre-Marie Pédrot
2020-08-24CI: stop testing 4.11+trunkGaëtan Gilbert
Now that 4.11.0 is released the trunk job doesn't work. 4.12 also doesn't work for separate reasons ("No rule found for kernel/byterun/byterun.a") We will separately update the edge switch in the docker image to use 4.11.0.
2020-08-20Special commit to start benchmarking.Maxime Dénès
2020-08-18Dockerfile: Update ounitGaëtan Gilbert
2020-07-21Add Coqtail to CIwhonore
2020-07-20CI: deploy make-built stdlib docGaëtan Gilbert
Workaround #12699 Alternative to #12700
2020-07-10Fix fiat_crypto(_ocaml) needs/dependenciesGaëtan Gilbert
It seems gitlab has issues with missing transitive dependencies, for instance in https://gitlab.com/coq/coq/-/pipelines/164834444 rewriter failed (missing overlay), fiat_crypto was skipped and fiat_crypto_ocaml was incorrectly started and so failed. May also fix (intermittent?) issue where it doesn't download the rewriter or bignum artifact and gets incompatible ocaml when compiling.
2020-07-01[ci] Disable the OCaml 4.12 targetEmilio Jesus Gallego Arias
Recent changes in Coqbot plus the unfortunate breakage OCaml upstream has make this too noisy. We will re-enable once https://github.com/ocaml/dune/pull/3585 is accepted upstream.
2020-06-27Merge PR #12518: [ci] [ocaml] Track OCaml 4.12Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-25[ci] [ocaml] Track OCaml 4.12Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 07:00:05 +0000