From fdf2f92ed5e2e838ffb11183c00f724e4e7c3a51 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 24 Nov 2020 19:31:56 +0100
Subject: [ci] separate oddorder and fourcolor from mathcomp

In this way interval does not have to wait too much
---
 .gitlab-ci.yml         | 20 ++++++++++++++++++++
 Makefile.ci            |  4 ++++
 dev/ci/ci-fourcolor.sh |  8 ++++++++
 dev/ci/ci-mathcomp.sh  |  8 --------
 dev/ci/ci-oddorder.sh  |  8 ++++++++
 5 files changed, 40 insertions(+), 8 deletions(-)
 create mode 100755 dev/ci/ci-fourcolor.sh
 create mode 100755 dev/ci/ci-oddorder.sh

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 32299d49d6..9fb0fc581c 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -808,6 +808,26 @@ library:ci-interval:
   - library:ci-mathcomp
   - plugin:ci-bignums
 
+library:ci-oddorder:
+  extends: .ci-template-flambda
+  stage: stage-3
+  needs:
+  - build:edge+flambda
+  - library:ci-mathcomp
+  dependencies:
+  - build:edge+flambda
+  - library:ci-mathcomp
+
+library:ci-fourcolor:
+  extends: .ci-template-flambda
+  stage: stage-3
+  needs:
+  - build:edge+flambda
+  - library:ci-mathcomp
+  dependencies:
+  - build:edge+flambda
+  - library:ci-mathcomp
+
 library:ci-corn:
   extends: .ci-template-flambda
   stage: stage-4
diff --git a/Makefile.ci b/Makefile.ci
index d95ffa53e8..fd41884e5c 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -34,6 +34,7 @@ CI_TARGETS= \
     ci-fiat_crypto_ocaml \
     ci-fiat_parsers \
     ci-flocq \
+    ci-fourcolor \
     ci-geocoq \
     ci-coqhammer \
     ci-hott \
@@ -44,6 +45,7 @@ CI_TARGETS= \
     ci-menhir \
     ci-metacoq \
     ci-mtac2 \
+    ci-oddorder \
     ci-paramcoq \
     ci-perennial \
     ci-quickchick \
@@ -81,6 +83,8 @@ ci-fiat_crypto: ci-coqprime ci-rewriter
 ci-fiat_crypto_ocaml: ci-fiat_crypto
 
 ci-interval: ci-mathcomp ci-flocq ci-coquelicot ci-bignums
+ci-fourcolor: ci-mathcomp
+ci-oddorder: ci-mathcomp
 
 ci-simple_io: ci-ext_lib
 ci-quickchick: ci-ext_lib ci-simple_io
diff --git a/dev/ci/ci-fourcolor.sh b/dev/ci/ci-fourcolor.sh
new file mode 100755
index 0000000000..72a1567398
--- /dev/null
+++ b/dev/ci/ci-fourcolor.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download fourcolor
+
+( cd "${CI_BUILD_DIR}/fourcolor" && make && make install )
diff --git a/dev/ci/ci-mathcomp.sh b/dev/ci/ci-mathcomp.sh
index b1aa56ec4e..f170b35327 100755
--- a/dev/ci/ci-mathcomp.sh
+++ b/dev/ci/ci-mathcomp.sh
@@ -7,11 +7,3 @@ ci_dir="$(dirname "$0")"
 git_download mathcomp
 
 ( cd "${CI_BUILD_DIR}/mathcomp/mathcomp" && make && make test-suite && make install )
-
-git_download fourcolor
-
-( cd "${CI_BUILD_DIR}/fourcolor" && make && make install )
-
-git_download oddorder
-
-( cd "${CI_BUILD_DIR}/oddorder" && make )
diff --git a/dev/ci/ci-oddorder.sh b/dev/ci/ci-oddorder.sh
new file mode 100755
index 0000000000..b2da32ad61
--- /dev/null
+++ b/dev/ci/ci-oddorder.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download oddorder
+
+( cd "${CI_BUILD_DIR}/oddorder" && make && make install )
-- 
cgit v1.2.3