From 906291a650c2fed7090b6d0702d56f03c3d44191 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Wed, 8 Nov 2023 15:46:13 -0800
Subject: [PATCH] Drop CI testing of 8.16

In preparation for https://github.com/mit-plv/coqutil/pull/102
---
 .github/workflows/coq-debian.yml       | 16 +++++++++++++++-
 .github/workflows/coq-macos.yml        |  2 +-
 .github/workflows/coq-opam-package.yml |  2 +-
 .github/workflows/coq-windows.yml      |  2 +-
 README.md                              |  2 +-
 5 files changed, 19 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
index 2c71c9950ae..7590d67ef93 100644
--- a/.github/workflows/coq-debian.yml
+++ b/.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' }}
diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml
index eddb87fd4a8..15a3f9e38df 100644
--- a/.github/workflows/coq-macos.yml
+++ b/.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"
 
diff --git a/.github/workflows/coq-opam-package.yml b/.github/workflows/coq-opam-package.yml
index 44cf2057627..bd891efb6ae 100644
--- a/.github/workflows/coq-opam-package.yml
+++ b/.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', '']
diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml
index 005728244c8..ec32deea6d0 100644
--- a/.github/workflows/coq-windows.yml
+++ b/.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"
diff --git a/README.md b/README.md
index 8b1f540939d..7e05e66e0c7 100644
--- a/README.md
+++ b/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.