| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
As discussed in #6930, we remove the warnings jobs and instead do
require the developers to submit a clean build.
|
| |
|
|
|
|
| |
- We update the OCaml version used in the base CI image.
- Windows / OSX image building is also updated to use newer OCaml.
- We also update Dune to 1.0.0.
|
| | |
|
| | |
|
| |
|
|
|
| |
This will allow for better reuse of the cache when the URL is different
but the archive is the same.
|
| | |
|
| |\ |
|
| | |
| |
| |
| | |
This can then be leveraged by @coqbot to know which builds to restart.
|
| |/
|
|
|
|
| |
We pin default.nix again to make the CI build predictable.
As in Windows builds, we need to override the default before_script.
As in other test-suite jobs, we export logs as artifacts on failure.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
This should help towards ensuring that the system only has the
packages we specify in the Dockerfile.
We were missing:
- `git`: used in the CI system itself!
- `rsync`: used in the test-suite
- `python3-setuptools`, `python3-wheel`: necessary to use pip3
properly to install the missing python package.
- `autoconf`, `automake`: a few CI contribs depend on them.
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
|
| |
Not all runners are equipped with docker services, thus we must add a
hard dependency on the `docker` tag for our Docker job.
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| |/
|
|
|
|
|
|
|
|
|
| |
The file `config/Makefile` doesn't exist unless we run `./configure`.
We shouldn't have to run `./configure` to run `make clean`. We now no
longer error in any case if `config/Makefile` doesn't exist; this is
simpler than only not erroring if the target is `clean`.
We also now test this property when building on CI.
This fixes #7542
|
| |\ |
|
| | | |
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
A docker-boot job is added which builds the docker image and pushes it
to the registry, the other jobs running on the image from the
registry.
The boot job reuses the already pushed image if it exists and matches,
this is important to cut down its runtime.
Making a new image takes 30min for all the switches
https://gitlab.com/SkySkimmer/coq/-/jobs/66650546
For testing I removed all jobs except boot and main build, and after
that run I built only the standard switch.
Building 1 switch takes around 20min
https://gitlab.com/SkySkimmer/coq/-/jobs/66656942
When the registry is up to date it takes 2min
https://gitlab.com/SkySkimmer/coq/-/jobs/66658790
(I don't know about all switches but probably no more than 5min)
Each pipeline pushes the image to $CI_REGISTRY_IMAGE:$CI_PIPELINE_ID
which is eg registry.gitlab.com/skyskimmer/coq:21557176 and is what
the other jobs use to run themselves.
For caching it pulls from and pushes to a constant name, in this test
$CI_REGISTRY_IMAGE:$CACHEKEY. We might also want to pull from the main
coq repo to avoid redoing work.
The question of having 1 image or 1 image/switch remains open.
Using the gitlab registry doesn't really work for circle CI, so the
dockerhub account would have to remain (or circle could return to an
opam-boot job, or be removed from our CI). There are similar concerns
with travis if we want to move it to docker.
|
| |\ \ |
|
| | |/
|/|
| |
| | |
We never actually used the -warn-error flag...
|
| | |
| |
| |
| | |
It's redundant as a dependency of formal-topology.
|
| |/
|
|
|
|
|
|
| |
We use a specific runner on Inria CloudStack. This allows us to have the
same build infrastructure setup for signed and unsigned binary packages.
The main Coq repository on Gitlab will produce unsigned binaries, using
a runner without secret. On my repository, a one-click operation will
sign the packages, making this part of the release process smoother.
|
| |
|
|
|
| |
I followed the code for fiat-crypto / fiat-parsers. I hope I didn't
miss anything.
|
| |
|
|
|
| |
Gains seem superior to 50%, but data is taken from Gitlab so no
reliable at all.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
We also introduce a bit more systematic job naming: `base/edge`.
In order to make the flambda switch selectable we update the Docker
image so all the dependencies are installed in that one.
Note the extra quote rule for the flambda parameters, but unless we
can assign arrays to Gitlab variables there is not a good way to do
this I'm afraid.
With this patch we are getting close to being able to remove most
builds from Travis.
|
| |
|
|
| |
This should help #6808.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We move gitlab runners to Ubuntu 18.04 "Bionic"; this allows us to
install most base dependencies using APT, and opens up the door to
saving quite a bit of time by creating a custom docker image
[c.f. #7383]
This change comes with an update of dependencies; we tweak them. Also:
- we add a more precise cache `key` constraint; this is still done
manually, we should develop an automated way in another PR. The
format is "$image-v$date-$hour-$minute"
- we export DEBIAN_FRONTEND=noninteractive as to avoid problems with
package installs that ask for interactive input.
- we install Sphinx Python packages using `apt` save for
python3-antlr4, which is still unpackaged [see
https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=897129]
|
| |
|
|
| |
AFAICS `imagemagick` `hacha` and `transfig` are not used anymore.
|
| |\ |
|
| | |
| |
| |
| |
| | |
Newer versions don't have the latex packages we want.
see eg https://gitlab.com/SkySkimmer/coq/-/jobs/65498131
|
| |/ |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Like circle CI we install every opam package in opam-boot jobs (one
per switch).
This should be more reliable with less issues from outdated cache.
Also avoid messing with symlinks through OPAMROOT (we can't
cache/artifact files outside the coq directory).
Avoid using "system" compiler (no risk of getting an upgrade through
the base image).
|
| |
|
|
|
|
|
|
|
|
| |
When `build` was made to build the doc it dropped `-coqide opt` and
dropped the environment variables for building coqide.
The combination means that when the cache had lablgtk in
opam (installed by some other job) configure would pick it up but the
system package wouldn't be there causing a failure. When lablgtk isn't
in the cache everything was fine.
|
| | |
|
| |
|
|
|
| |
Previously it was installed for the compilation jobs causing random
failures when the other jobs got a cache without it.
|
Emilio Jesus Gallego Arias
Théo Zimmermann
Gaëtan Gilbert
Andres Erbsen
Enrico Tassi
Leonidas Lampropoulos
Jason Gross
Maxime Dénès
Beta Ziliani
Anton Trunov