experimental upgrade to Dune Coq 0.8 to enable composition

runtimeverification · Jul 3, 2023 · 9c348ce · 9c348ce
1 parent 0e1937b
commit 9c348ce
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 4 deletions.
diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
@@ -14,14 +14,18 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:8.16-ocaml-4.14-flambda'
+          - 'coqorg/coq:8.17-ocaml-4.14-flambda'
       fail-fast: false
     steps:
       - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-vlsm.opam'
           custom_image: ${{ matrix.image }}
-
+          before_install: |
+            startGroup "Print opam config and unpin dune"
+              opam config list; opam repo list; opam list; opam pin remove dune -y
+            endGroup
 
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme

diff --git a/coq-vlsm.opam b/coq-vlsm.opam
@@ -15,7 +15,7 @@ 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.8.2"}
   "coq" {>= "8.16"}
   "coq-stdpp" {>= "1.8.0"}
   "coq-itauto" 

diff --git a/dune-project b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 3.8)
+(using coq 0.8)
 (name VLSM)
diff --git a/meta.yml b/meta.yml
@@ -65,6 +65,7 @@ dependencies:
 
 tested_coq_opam_versions:
 - version: '8.16-ocaml-4.14-flambda'
+- version: '8.17-ocaml-4.14-flambda'
 
 namespace: VLSM
 

diff --git a/theories/VLSM/dune b/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))