Drop CI testing of 8.16

In preparation for mit-plv/coqutil#102

.github/workflows/coq-debian.yml

@@ -17,7 +17,7 @@ jobs:
       matrix:
         include:
         - env: { DEBIAN: "sid" }
-        - env: { DEBIAN: "bookworm" }
+        #- env: { DEBIAN: "bookworm" }# restore once 8.17 lands in Debian stable
 
     runs-on: 'ubuntu-22.04'
     env: ${{ matrix.env }}
@@ -104,3 +104,17 @@ jobs:
       run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files SLOWEST_FIRST=1
       env:
         ALLOW_DIFF: 1
+
+  debian-check-all:
+    runs-on: ubuntu-latest
+    needs: [build, test-amd64]
+    if: always()
+    steps:
+    - run: echo 'build passed'
+      if: ${{ needs.build.result == 'success' }}
+    - run: echo 'test-amd64 passed'
+      if: ${{ needs.test-amd64.result == 'success' }}
+    - run: echo 'build failed' && false
+      if: ${{ needs.build.result != 'success' }}
+    - run: echo 'test-amd64 failed' && false
+      if: ${{ needs.test-amd64.result != 'success' }}

.github/workflows/coq-macos.yml

@@ -20,7 +20,7 @@ jobs:
 
     env:
       NJOBS: "2"
-      COQ_VERSION: "8.16.0" # minimal major version required for bedrock2 components
+      COQ_VERSION: "8.17.0" # minimal major version required for bedrock2 components
       COQCHKEXTRAFLAGS: ""
       SKIP_BEDROCK2: "0"
 

.github/workflows/coq-opam-package.yml

@@ -16,7 +16,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        coq-version: ['dev', '8.16.0']
+        coq-version: ['dev', '8.18.0', '8.17.0']
         ocaml-compiler: ['4.11.1']
         os: ['ubuntu-latest', 'macos-latest', 'windows-latest']
         coq-extra-flags: ['-async-proofs-j 1', '']

.github/workflows/coq-windows.yml

@@ -23,7 +23,7 @@ jobs:
 
     env:
       NJOBS: "2"
-      COQ_VERSION: "8.16.0" # https://packages.debian.org/testing/coq
+      COQ_VERSION: "8.18.0" # pick a version not tested on other platforms
       COQEXTRAFLAGS: "-async-proofs-j 1"
       COQCHKEXTRAFLAGS: ""
       OPAMYES: "true"

README.md

@@ -20,7 +20,7 @@ Building
 [pkg.go-shield]: https://pkg.go.dev/badge/github.com/mit-plv/fiat-crypto/fiat-go.svg
 [pkg.go-link]: https://pkg.go.dev/github.com/mit-plv/fiat-crypto/fiat-go
 
-This repository requires [Coq](https://coq.inria.fr/) [8.16](https://github.com/coq/coq/releases/tag/V8.16.0) or later.
+This repository requires [Coq](https://coq.inria.fr/) [8.17](https://github.com/coq/coq/releases/tag/V8.17.0) or later.
 Note that if you install Coq from Ubuntu aptitude packages, you need `libcoq-ocaml-dev` in addition to `coq`.
 Note that in some cases (such as installing Coq via homebrew on Mac), you may also need to install `ocaml-findlib` (for `ocamlfind`).
 The extracted OCaml code for the standalone binaries requires [OCaml](https://ocaml.org/) [4.08](https://ocaml.org/p/ocaml/4.08.0) or later.