From 832787e00857627a5c49e03fb9d6b19d722f0dd1 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Wed, 24 Jul 2024 13:39:48 +0200
Subject: [PATCH] switch Docker CI cron to weekly, explicit dependency on HB

---
 .github/workflows/docker-action.yml |  2 +-
 README.md                           |  3 ++-
 coq-fourcolor.opam                  |  5 +++--
 meta.yml                            | 15 ++++++++++-----
 4 files changed, 16 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index e11c8b9..3a20fb9 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -4,7 +4,7 @@ name: Docker CI
 
 on:
   schedule:
-    - cron: '0 5 * * *'
+    - cron: '0 5 * * 0'
   push:
     branches:
       - master
diff --git a/README.md b/README.md
index a64b7b5..c317c4c 100644
--- a/README.md
+++ b/README.md
@@ -37,8 +37,9 @@ basic plane topology definitions, and a theory of combinatorial hypermaps.
 - License: [CeCILL-B](LICENSE)
 - Compatible Coq versions: 8.16 or later
 - Additional dependencies:
-  - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
+  - [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.5.0 or later
 - Coq namespace: `fourcolor`
 - Related publication(s):
   - [Formal Proof—The Four-Color Theorem](https://www.ams.org/notices/200811/tx081101382p.pdf) 
diff --git a/coq-fourcolor.opam b/coq-fourcolor.opam
index bd63f91..94846bf 100644
--- a/coq-fourcolor.opam
+++ b/coq-fourcolor.opam
@@ -20,9 +20,10 @@ basic plane topology definitions, and a theory of combinatorial hypermaps."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.16" & < "8.20~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "2.1.0" & < "2.3~") | (= "dev")}
+  "coq" {>= "8.16"}
+  "coq-mathcomp-ssreflect" {>= "2.1.0"}
   "coq-mathcomp-algebra" 
+  "coq-hierarchy-builder" {>= "1.5.0"}
 ]
 
 tags: [
diff --git a/meta.yml b/meta.yml
index acde421..e84bc28 100644
--- a/meta.yml
+++ b/meta.yml
@@ -37,7 +37,7 @@ license:
 
 supported_coq_versions:
   text: 8.16 or later
-  opam: '{(>= "8.16" & < "8.20~") | (= "dev")}'
+  opam: '{>= "8.16"}'
 
 tested_coq_opam_versions:
 - version: '2.1.0-coq-8.16'
@@ -55,20 +55,25 @@ tested_coq_opam_versions:
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
 
-# test master every day at 05:00 UTC
+# test master every Sunday at 05:00 UTC
 # (mathcomp/mathcomp-dev is rebuilt every day at 04:00 Paris time)
-ci_cron_schedule: '0 5 * * *'
+ci_cron_schedule: '0 5 * * 0'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.1.0" & < "2.3~") | (= "dev")}'
+    version: '{>= "2.1.0"}'
   description: |-
-    [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
   description: |-
     [MathComp algebra](https://math-comp.github.io)
+- opam:
+    name: coq-hierarchy-builder
+    version: '{>= "1.5.0"}'
+  description: |-
+    [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) 1.5.0 or later
 
 namespace: fourcolor