Enrico Tassi (Sep 05 2023 at 08:37): Enrico Tassi (Sep 05 2023 at 08:37):Can I get a CI expert on https://github.com/coq/coq/pull/18011 ?
It seems the docker image is gone. CC @Maxime Dénès @Gaëtan Gilbert
Gaëtan Gilbert (Sep 05 2023 at 09:01):is that the first time CI is run on gitlab.inria for 8.18?
Gaëtan Gilbert (Sep 05 2023 at 09:06):I guess you need to run docker-boot for 8.18
If you have the rights you can manually run the pipeline with variable SKIP_DOCKER=false
otherwise I guess you can push a temporary commit removing
except:
variables:
- $SKIP_DOCKER == "true"
in the .gitlab-ci.yml
Gaëtan Gilbert (Sep 05 2023 at 09:06):(I currently don't seem to have the rights to run manual pipelines)
Enrico Tassi (Sep 05 2023 at 11:06):I'm sure maxime did that, and that this is not the first CI run on v8.18
Enrico Tassi (Sep 05 2023 at 11:06):Me neither, I tried yesterday and the button to run pipelines was gone
Gaëtan Gilbert (Sep 05 2023 at 11:18):I got powers, attempt https://gitlab.inria.fr/coq/coq/-/pipelines/852396
Gaëtan Gilbert (Sep 05 2023 at 11:19):why am I not owner in the group though
Gaëtan Gilbert (Sep 05 2023 at 11:30):it's not picking up a runner and I can't see what runners we have because I'm not owner
Gaëtan Gilbert (Sep 05 2023 at 11:36):I guess it's just waiting for an available runner
Maxime Dénès (Sep 05 2023 at 12:26):You're now an owner of the group, aren't you?
Gaëtan Gilbert (Sep 05 2023 at 12:33):yes
Gaëtan Gilbert (Sep 05 2023 at 19:00):docker passed
Jason Gross (Sep 05 2023 at 22:45):Is this related to https://github.com/mit-plv/fiat/pull/93 still failing (my guess is the dev docker image hasn't been updated, but I haven't investigated carefully)
Théo Zimmermann (Sep 06 2023 at 09:16):Probably related to the lack of webhook added to trigger the Docker-Coq rebuild. I will add it despite what @Erik Martin-Dorel answered in #Coq devs & plugin devs > Migration to Inria GitLab for CI (instead of GitLab.com).
Erik Martin-Dorel (Sep 06 2023 at 12:38):Hi @Théo Zimmermann, I didn't fully understand your comment :sweat_smile:
I thought you had already added the webhook, given my last comment https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/Migration.20to.20Inria.20GitLab.20for.20CI.20.28instead.20of.20GitLab.2Ecom.29/near/388535925
Théo Zimmermann (Sep 06 2023 at 12:39):Sorry, it looks like I had missed your second comment! Now this is fixed!
Erik Martin-Dorel (Sep 06 2023 at 12:40):FWIW, you can always easily inspect the contents of a remote Docker image by going to URL
https://explore.ggcr.dev/?image=$IMAGE_TAG
e.g.
https://explore.ggcr.dev/?image=coqorg/coq:dev
Then click on the first link in config.digest:
Which currently shows:
"Env": [
"PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin",
"OPAM_VERSION=2.1.3",
"NJOBS=2",
"OPAMPRECISETRACKING=1",
"COMPILER=4.13.1+flambda",
"OCAMLFIND_VERSION=1.9.6",
"DUNE_VERSION=3.9.1",
"ZARITH_VERSION=1.12",
"COQ_EXTRA_OPAM=coq-bignums",
"COQ_VERSION=dev"
],
"Labels": {
"maintainer": "erik@martin-dorel.org",
"org.label-schema.build-date": "2023-09-06T11:04:14Z",
"org.label-schema.description": "Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.",
"org.label-schema.name": "The Coq Proof Assistant",
"org.label-schema.schema-version": "1.0",
"org.label-schema.url": "https://coq.inria.fr/",
"org.label-schema.vcs-ref": "afaecfd",
"org.label-schema.vcs-url": "https://github.com/coq/coq",
"org.label-schema.vendor": "The Coq Development Team",
"org.label-schema.version": "dev"
},
In particular, we can get the timestamp and the coq master SHA1 inside the labels: afaecfd
Erik Martin-Dorel (Sep 06 2023 at 12:41):Théo Zimmermann said:
Sorry, it looks like I had missed your second comment! Now this is fixed!
OK ! thanks Théo :-)
Last updated: Dec 05 2023 at 12:01 UTC