search

coq / opam

Archive for all Coq related OPAM packages organized in various repositories
https://coq.inria.fr/opam/www/
GNU Lesser General Public License v2.1
127 stars 166 forks source link

Introduce tags for Inria GitLab CI. #3181

Closed Zimmi48 closed 1 month ago

Zimmi48 commented 1 month ago

Following an issue with having hit our quotas on GitLab.com, and by request of @mattam82 in https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/GitLab.2Ecom.20subscription.20.2F.20compute.20minutes.

This PR introduces the tags that are needed to run jobs on Inria GitLab CI (using the shared runners there).

This PR should be merged just after coq/bot#324 is merged and deployed.

Zimmi48 commented 1 month ago

There's a pipeline for this branch at https://gitlab.inria.fr/coq/opam/-/pipelines/1049952.

Zimmi48 commented 1 month ago

Actually, testing on a branch is not a working solution. I should test-deploy the bot PR so that this is tested in normal PR conditions.

Zimmi48 commented 1 month ago

Actually, testing on a branch is not a working solution. I should test-deploy the bot PR so that this is tested in normal PR conditions.

I thought this was the problem, but I misinterpreted the error in the log. I got the same error when testing this in "normal PR conditions":

$ scripts/opam-coq-list-pr-files | xargs scripts/opam-coq-lint
PR head is: 3b80d02d8a40a562f3553c447b53347462c0d220
fatal: Not a valid object name origin/master

See https://gitlab.inria.fr/coq/opam/-/jobs/4842732

Zimmi48 commented 1 month ago

@gares I'm afraid I'll need help to debug this part.

Zimmi48 commented 1 month ago

Going to merge as suggested by @palmskog on Zulip.