aboutsummaryrefslogtreecommitdiff
path: root/.gitlab-ci.yml
AgeCommit message (Collapse)Author
2021-04-21Add mczify to CIKazuhiko Sakaguchi
2021-04-17Pin docutils to 0.16.Théo Zimmermann
Docutils 0.17 creates problem with our Sphinx rtd theme.
2021-04-14[ci] update elpi to 1.13.1Enrico Tassi
2021-03-14[ci] [gitlab] Remove ad-hoc mathcomp install macrosEmilio Jesus Gallego Arias
They should not be necessary today as they date from the shareable pre-artifact epoch, an incur in an slowdown.
2021-03-11Add deriving lib to CI.Arthur Azevedo de Amorim
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
We introduce a new package structure for Coq: - `coq-core`: Coq's OCaml tools code and plugins - `coq-stdlib`: Coq's stdlib [.vo files] - `coq`: meta-package that pulls `coq-{core,stdlib}` This has several advantages, in particular it allows to install Coq without the stdlib which is useful in several scenarios, it also open the door towards a versioning of the stdlib at the package level. The main user-visible change is that Coq's ML development files now live in `$lib/coq-core`, for compatibility in the regular build we install a symlink and support both setups for a while. Note that plugin developers and even `coq_makefile` should actually rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust. There is a transient state where we actually look for both `$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support the non-ocamlfind plus custom variables. This will be much improved once #13617 is merged (which requires this PR first), then, we will introduce a `coq.boot` library so finally `coqdep`, `coqchk`, etc... can share the same path setup code. IMHO the plan should work fine.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:01:14 +0000