Adapt to Coq 8.19 and CompCert 3.13.1

PrincetonUniversity · Mar 19, 2024 · b0068a6 · b0068a6
1 parent 49dab45
commit b0068a6
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 8 deletions.
diff --git a/.github/workflows/coq-action.yml b/.github/workflows/coq-action.yml
@@ -21,20 +21,20 @@ jobs:
         # except for the "make_target" field and make_target related excludes
         coq_version:
           # See https://github.com/coq-community/docker-coq/wiki for supported images
-          - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
           - 'dev'
         bit_size:
           - 32
           - 64
         make_target:
           - vst
         exclude:   
-          - coq_version: 8.16
-            bit_size: 32
           - coq_version: 8.17
             bit_size: 32
+          - coq_version: 8.18
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
     steps:
@@ -53,7 +53,7 @@ jobs:
             endGroup
           install: |
             startGroup "Install dependencies"
-              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13' || 'coq-compcert.3.13' }}
+              opam install -y ${{ matrix.coq_version == 'dev' && 'coq-flocq' || matrix.bit_size == 32 && 'coq-compcert-32.3.13.1' || 'coq-compcert.3.13.1' }}
               # Required by test2
               opam install -y coq-ext-lib
             endGroup
@@ -89,9 +89,9 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-          - '8.16'
           - '8.17'
           - '8.18'
+          - '8.19'
           - 'dev' 
         make_target:
           - assumptions.txt
@@ -104,10 +104,10 @@ jobs:
           - 32
           - 64
         exclude:
-          - coq_version: 8.16
-            bit_size: 32
           - coq_version: 8.17
             bit_size: 32
+          - coq_version: 8.18
+            bit_size: 32
           - coq_version: dev
             bit_size: 32
           - bit_size: 64

diff --git a/Makefile b/Makefile
@@ -21,7 +21,7 @@ COQLIB=$(shell $(COQC) -where | tr -d '\r' | tr '\\' '/')
 
 # Check Coq version
 
-COQVERSION= 8.16.0 or-else 8.16.1 or-else 8.17+rc1 or-else 8.17 or-else 8.17.0 or-else 8.17.1 or-else 8.18.0
+COQVERSION= 8.17.0 or-else 8.17.1 or-else 8.18.0 or-else 8.19.1
 
 COQV=$(shell $(COQC) -v)
 ifneq ($(IGNORECOQVERSION),true)