From b3fcfc7f2591b48930c8e78261a659c17c467cc6 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Sun, 20 Aug 2023 00:43:33 +0200
Subject: [PATCH] update CI and other boilerplate for 8.18

---
 .github/workflows/docker-action.yml | 5 ++++-
 .github/workflows/nix-action.yml    | 6 +++---
 coq-almost-full.opam                | 4 ++--
 dune-project                        | 4 ++--
 meta.yml                            | 6 ++++--
 5 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index 08e5ddb..745de79 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -18,6 +18,8 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.18'
+          - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.15'
           - 'coqorg/coq:8.14'
@@ -26,12 +28,13 @@ jobs:
           - 'coqorg/coq:8.11'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-almost-full.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo
diff --git a/.github/workflows/nix-action.yml b/.github/workflows/nix-action.yml
index b8502ec..a621024 100644
--- a/.github/workflows/nix-action.yml
+++ b/.github/workflows/nix-action.yml
@@ -32,15 +32,15 @@ jobs:
           else
             echo "tested_commit=${{ github.sha }}" >> $GITHUB_ENV
           fi
-      - uses: cachix/install-nix-action@v16
+      - uses: cachix/install-nix-action@v20
         with:
           nix_path: nixpkgs=channel:nixpkgs-unstable
-      - uses: cachix/cachix-action@v10
+      - uses: cachix/cachix-action@v12
         with:
           name: coq-community
           authToken: '${{ secrets.CACHIX_AUTH_TOKEN }}'
           extraPullNames: coq, math-comp
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
         with:
           ref: ${{ env.tested_commit }}
       - run: >
diff --git a/coq-almost-full.opam b/coq-almost-full.opam
index fc3bd82..c1d9134 100644
--- a/coq-almost-full.opam
+++ b/coq-almost-full.opam
@@ -17,8 +17,8 @@ Theorem, useful for proving termination."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [
-  "dune" {>= "2.5"}
-  "coq" {(>= "8.11" & < "8.17~") | (= "dev")}
+  "dune" {>= "3.5"}
+  "coq" {>= "8.11"}
 ]
 
 tags: [
diff --git a/dune-project b/dune-project
index 2a9d688..658d089 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.5)
-(using coq 0.2)
+(lang dune 3.5)
+(using coq 0.6)
 (name almost-full)
diff --git a/meta.yml b/meta.yml
index 48f77c5..1816a32 100644
--- a/meta.yml
+++ b/meta.yml
@@ -6,7 +6,7 @@ community: true
 action: true
 nix: true
 coqdoc: false
-dune: false
+dune: true
 doi: 10.1007/978-3-642-32347-8_17
 
 synopsis: >-
@@ -43,13 +43,15 @@ license:
 
 supported_coq_versions:
   text: 8.11 or later
-  opam: '{(>= "8.11" & < "8.17~") | (= "dev")}'
+  opam: '{>= "8.11"}'
 
 tested_coq_nix_versions:
 - coq_version: 'master'
 
 tested_coq_opam_versions:
 - version: dev
+- version: '8.18'
+- version: '8.17'
 - version: '8.16'
 - version: '8.15'
 - version: '8.14'