From 32077bbbe75e8e9376b001dad8252d40e1fedba7 Mon Sep 17 00:00:00 2001
From: Aleksandar Nanevski <aleks.nanevski@imdea.org>
Date: Tue, 8 Apr 2025 16:07:39 +0200
Subject: [PATCH] fixing the name for the docker image for rocq dev

---
 .github/workflows/docker-action.yml | 30 +++++------------------------
 README.md                           |  2 +-
 coq-htt-core.opam                   |  2 +-
 meta.yml                            |  8 ++++----
 theories/dune                       |  7 +++++++
 5 files changed, 18 insertions(+), 31 deletions(-)
 create mode 100644 theories/dune

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index cb1399b..23287ab 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -1,3 +1,5 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
 name: Docker CI
 
 on:
@@ -17,37 +19,15 @@ jobs:
         image:
           - 'mathcomp/mathcomp:2.2.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
-          - 'mathcomp/mathcomp:latest-coq-dev'
+          - 'mathcomp/mathcomp-dev:rocq-prover-dev'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
+          opam_file: 'coq-htt-core.opam'
           custom_image: ${{ matrix.image }}
-          custom_script: |
-            {{before_install}}
-            startGroup "Build htt-core dependencies"
-              opam pin add -n -y -k path coq-htt-core .
-              opam update -y
-              opam install -y -j $(nproc) coq-htt-core --deps-only
-            endGroup
-            startGroup "Build htt-core"
-              opam install -y -v -j $(nproc) coq-htt-core
-              opam list
-            endGroup
-            startGroup "Build htt dependencies"
-              opam pin add -n -y -k path coq-htt .
-              opam update -y
-              opam install -y -j $(nproc) coq-htt --deps-only
-            endGroup
-            startGroup "Build coq-htt"
-              opam install -y -v -j $(nproc) coq-htt
-              opam list
-            endGroup
-            startGroup "Uninstallation test"
-              opam remove -y coq-htt
-              opam remove -y coq-htt-core
-            endGroup
+
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
diff --git a/README.md b/README.md
index 3d79121..27468b0 100644
--- a/README.md
+++ b/README.md
@@ -39,7 +39,7 @@ that HTT implements Separation logic as a shallow embedding in Coq.
   - Alexander Gryzlov
   - Marcos Grandury
 - License: [Apache-2.0](LICENSE)
-- Compatible Coq versions: Coq 8.19 to 8.20
+- Compatible Coq versions: 8.19 or later
 - Additional dependencies:
   - [MathComp ssreflect 2.2-2.3](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)
diff --git a/coq-htt-core.opam b/coq-htt-core.opam
index 74837d7..df6f36a 100644
--- a/coq-htt-core.opam
+++ b/coq-htt-core.opam
@@ -34,7 +34,7 @@ that HTT implements Separation logic as a shallow embedding in Coq."""
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.6"}
-  "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
diff --git a/meta.yml b/meta.yml
index 63d75fc..7b459b5 100644
--- a/meta.yml
+++ b/meta.yml
@@ -80,16 +80,16 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.19 to 8.20
-  opam: '{ (>= "8.19" & < "8.21~") | (= "dev") }'
+  text: 8.19 or later
+  opam: '{ (>= "8.19" & < "9.1~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '2.2.0-coq-8.19'
   repo: 'mathcomp/mathcomp'
 - version: '2.3.0-coq-8.20'
   repo: 'mathcomp/mathcomp'
-- version: 'latest-coq-dev'
-  repo: 'mathcomp/mathcomp'
+- version: 'rocq-prover-dev'
+  repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
diff --git a/theories/dune b/theories/dune
new file mode 100644
index 0000000..8f51667
--- /dev/null
+++ b/theories/dune
@@ -0,0 +1,7 @@
+; This file was generated from `meta.yml`, please do not edit manually.
+; Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+(coq.theory
+ (name htt)
+ (package coq-htt-core)
+ (synopsis "Hoare Type Theory"))