added data to enable ssr 2.3

.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:
@@ -23,31 +25,9 @@ jobs:
       - 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

README.md

@@ -45,7 +45,7 @@ that HTT implements Separation logic as a shallow embedding in Coq.
   - [MathComp algebra](https://math-comp.github.io)
   - [MathComp fingroup](https://math-comp.github.io)
   - [FCSL-PCM 2.0](https://github.com/imdea-software/fcsl-pcm)
-  - [Dune](https://dune.build) 2.5 or later
+  - [Dune](https://dune.build) 3.6 or later
 - Coq namespace: `htt`
 - Related publication(s):
   - [Structuring the verification of heap-manipulating programs](https://software.imdea.org/~aleks/papers/reflect/reflect.pdf) doi:[10.1145/1706299.1706331](https://doi.org/10.1145/1706299.1706331)

coq-htt-core.opam

@@ -3,7 +3,7 @@
 
 opam-version: "2.0"
 maintainer: "fcsl@software.imdea.org"
-version: "dev"
+version: "2.0.1"
 
 homepage: "https://github.com/imdea-software/htt"
 dev-repo: "git+https://github.com/imdea-software/htt.git"
@@ -35,7 +35,7 @@ build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
   "dune" {>= "3.6"}
   "coq" { (>= "8.19" & < "8.21~") | (= "dev") }
-  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.3~") | (= "dev") }
+  "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.4~") | (= "dev") }
   "coq-mathcomp-algebra" 
   "coq-mathcomp-fingroup" 
   "coq-fcsl-pcm" { (>= "2.0.0" & < "2.1~") | (= "dev") }

meta.yml

@@ -72,7 +72,7 @@ maintainers:
 
 opam-file-maintainer: fcsl@software.imdea.org
 
-opam-file-version: dev
+opam-file-version: 2.0.1
 
 license:
   fullname: Apache-2.0
@@ -94,7 +94,7 @@ tested_coq_opam_versions:
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{ (>= "2.2.0" & < "2.3~") | (= "dev") }'
+    version: '{ (>= "2.2.0" & < "2.4~") | (= "dev") }'
   description: |-
     [MathComp ssreflect 2.2](https://math-comp.github.io)
 - opam:

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"))