upgrade to Dune Coq 0.6, add Coq 8.18 to CI

.github/workflows/test-pr.yml

@@ -15,6 +15,7 @@ jobs:
         image:
           - 'coqorg/coq:8.16-ocaml-4.14-flambda'
           - 'coqorg/coq:8.17-ocaml-4.14-flambda'
+          - 'coqorg/coq:8.18-ocaml-4.14-flambda'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3

coq-vlsm.opam

@@ -15,9 +15,9 @@ contains a formalization of VLSMs and their theory in the Coq proof assistant.""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.5"}
+  "dune" {>= "3.5"}
   "coq" {>= "8.16"}
-  "coq-stdpp" {>= "1.8.0"}
+  "coq-stdpp" {= "1.8.0"}
   "coq-itauto" 
   "coq-equations" 
 ]

dune-project

@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 3.5)
+(using coq 0.6)
 (name VLSM)

meta.yml

@@ -3,7 +3,7 @@ fullname: VLSM
 shortname: vlsm
 organization: runtimeverification
 community: false
-dune: false
+dune: true
 action: true
 coqdoc: true
 
@@ -52,9 +52,9 @@ supported_coq_versions:
 dependencies:
 - opam:
     name: coq-stdpp
-    version: '{>= "1.8.0"}'
+    version: '{= "1.8.0"}'
   description: |-
-    [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/) 1.8.0 or later
+    [Coq-std++](https://gitlab.mpi-sws.org/iris/stdpp/) 1.8.0
 - opam:
     name: coq-itauto
   description: |-
@@ -67,6 +67,7 @@ dependencies:
 tested_coq_opam_versions:
 - version: '8.16-ocaml-4.14-flambda'
 - version: '8.17-ocaml-4.14-flambda'
+- version: '8.18-ocaml-4.14-flambda'
 
 namespace: VLSM
 

theories/VLSM/dune

@@ -2,6 +2,7 @@
  (name VLSM)
  (package coq-vlsm)
  (synopsis "Core definitions in Coq for VLSMs")
+ (theories stdpp Cdcl Equations)
  (flags :standard 
    -w -future-coercion-class-field
    -w -deprecated-tacopt-without-locality))