Merge PR coq#18888: Use gitlab.inria.fr shared runners for docker boot

Reviewed-by: ejgallego Co-authored-by: ejgallego <[email protected]>
Villetaneuse · Apr 15, 2024 · 1894462 · 1894462
2 parents 7b9f69f + fd9c9da
commit 1894462
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 2 deletions.
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
@@ -282,8 +282,8 @@ docker-boot:
   except:
     variables:
       - $SKIP_DOCKER == "true"
-  tags:
-    - docker
+  extends: .auto-use-docker-tags
+  timeout: 2h
 
 build:base:
   extends: .build-template

diff --git a/dev/ci/gitlab-modes/tagged-runners.yml b/dev/ci/gitlab-modes/tagged-runners.yml
@@ -1,3 +1,11 @@
 .auto-use-tags:
   tags:
     - $TAGGED_RUNNERS
+
+# making this configurable is too annoying if we want to support > 1 tag
+# and not sure small is enough
+# so just hardcode ci.inria.fr && medium
+.auto-use-docker-tags:
+  tags:
+    - ci.inria.fr
+    - medium
diff --git a/dev/ci/gitlab-modes/untagged-runners.yml b/dev/ci/gitlab-modes/untagged-runners.yml
@@ -1,2 +1,6 @@
 .auto-use-tags:
   tags: []
+
+.auto-use-docker-tags:
+  tags:
+    - docker