From 1097f580f9bba8683d336d60083894b8fb7d8bf8 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Thu, 9 Nov 2023 11:05:10 -0800
Subject: [PATCH] Drop CI testing of 8.16 (#1708)

Drop CI testing of 8.16

In preparation for https://github.com/mit-plv/coqutil/pull/102

On Windows, add default opam repo as per issues described at https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/8.2E18.20missing.20from.20opam.3F/near/401077134
---
 .github/workflows/coq-debian.yml  | 2 +-
 .github/workflows/coq-macos.yml   | 2 +-
 .github/workflows/coq-windows.yml | 5 ++++-
 README.md                         | 2 +-
 4 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
index 8cd7324dbf..7590d67ef9 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 }}
diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml
index eddb87fd4a..31e03924cd 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.18.0" # pick a version not tested on other platforms
       COQCHKEXTRAFLAGS: ""
       SKIP_BEDROCK2: "0"
 
diff --git a/.github/workflows/coq-windows.yml b/.github/workflows/coq-windows.yml
index 005728244c..83e482c62d 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.17.0" # minimal major version required for bedrock2 components
       COQEXTRAFLAGS: "-async-proofs-j 1"
       COQCHKEXTRAFLAGS: ""
       OPAMYES: "true"
@@ -41,6 +41,9 @@ jobs:
       uses: ocaml/setup-ocaml@v2
       with:
         ocaml-compiler: 4.11.1
+        opam-repositories: |
+          opam-repository-mingw: https://github.com/ocaml-opam/opam-repository-mingw.git#sunset
+          default: https://github.com/ocaml/opam-repository.git
     - run: opam depext coq.${{ env.COQ_VERSION }}
     - run: opam pin add --kind=version coq ${{ env.COQ_VERSION }}
 
diff --git a/README.md b/README.md
index 8b1f540939..7e05e66e0c 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.