From 9c348ce12bcff5d2d29e6f825ebd6ca06e9e36d2 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Wed, 7 Jun 2023 21:46:01 +0200
Subject: [PATCH] experimental upgrade to Dune Coq 0.8 to enable composition

---
 .github/workflows/test-pr.yml | 6 +++++-
 coq-vlsm.opam                 | 2 +-
 dune-project                  | 4 ++--
 meta.yml                      | 1 +
 theories/VLSM/dune            | 1 +
 5 files changed, 10 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml
index 8c78855d..1664acf1 100644
--- a/.github/workflows/test-pr.yml
+++ b/.github/workflows/test-pr.yml
@@ -14,6 +14,7 @@ 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
@@ -21,7 +22,10 @@ jobs:
         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
index 2d377c91..7c50299f 100644
--- 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
index 97a36b24..d5184c0d 100644
--- 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
index 5d6649a5..24855f51 100644
--- 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
index f4e15206..1693a068 100644
--- 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))