From b0a01acd904cbfcaf47d821b3b5e72098b9efb07 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Tue, 3 Sep 2019 17:07:44 +0200
Subject: Add (meet|join)_(l|r), some renamings, and small cleanups

New lemmas:
- meet_l, meet_r, join_l, join_r.

Renamings:
- Order.BLatticeTheory.lexUl -> disjoint_lexUl,
- Order.BLatticeTheory.lexUr -> disjoint_lexUr,
- Order.TBLatticeTheory.lexIl -> cover_leIxl,
- Order.TBLatticeTheory.lexIr -> cover_leIxr.

Use `Order.TTheory` instead of `Order.Theory` if applicable
---
 .gitlab-ci.yml | 60 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 60 insertions(+)

(limited to '.gitlab-ci.yml')

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index ef0b240..b366d39 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -143,6 +143,9 @@ coq-dev:
   script:
     - make -j "${NJOBS}"
     - make install
+  except:
+    - /^experiment\/order$/
+    - /^pr-(270|383)$/
 
 ci-fourcolor-8.7:
   extends: .ci-fourcolor
@@ -169,6 +172,33 @@ ci-fourcolor-dev:
   variables:
     COQ_VERSION: "dev"
 
+.ci-fourcolor-270:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/pi8027/fourcolor.git"
+    CONTRIB_VERSION: fix-mathcomp-270
+  script:
+    - make -j "${NJOBS}"
+    - make install
+  only:
+    - /^experiment\/order$/
+    - /^pr-(270|383)$/
+
+ci-fourcolor-8.7-270:
+  extends: .ci-fourcolor-270
+  variables:
+    COQ_VERSION: "8.7"
+
+ci-fourcolor-8.8-270:
+  extends: .ci-fourcolor-270
+  variables:
+    COQ_VERSION: "8.8"
+
+ci-fourcolor-dev-270:
+  extends: .ci-fourcolor-270
+  variables:
+    COQ_VERSION: "dev"
+
 # The Odd Order Theorem
 .ci-odd-order:
   extends: .ci
@@ -178,6 +208,9 @@ ci-fourcolor-dev:
   script:
     - make -j "${NJOBS}"
     - make install
+  except:
+    - /^experiment\/order$/
+    - /^pr-(270|383)$/
 
 ci-odd-order-8.7:
   extends: .ci-odd-order
@@ -204,6 +237,33 @@ ci-odd-order-dev:
   variables:
     COQ_VERSION: "dev"
 
+.ci-odd-order-270:
+  extends: .ci
+  variables:
+    CONTRIB_URL: "https://github.com/pi8027/odd-order.git"
+    CONTRIB_VERSION: fix-mathcomp-270
+  script:
+    - make -j "${NJOBS}"
+    - make install
+  only:
+    - /^experiment\/order$/
+    - /^pr-(270|383)$/
+
+ci-odd-order-8.7-270:
+ extends: .ci-odd-order-270
+ variables:
+   COQ_VERSION: "8.7"
+
+ci-odd-order-8.8-270:
+ extends: .ci-odd-order-270
+ variables:
+   COQ_VERSION: "8.8"
+
+ci-odd-order-dev-270:
+  extends: .ci-odd-order-270
+  variables:
+    COQ_VERSION: "dev"
+
 # The Lemma Overloading library
 .ci-lemma-overloading:
   extends: .ci
-- 
cgit v1.2.3