From eb9e5bcfffdd157e63a5776fcbefe5275f8d6448 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <saemi472@gmail.com>
Date: Sat, 12 Aug 2023 15:09:21 -0400
Subject: [PATCH] update CI to Coq 8.16, and remove Ubuntu LTS because we now
 have Debian

---
 .github/workflows/coq-macos.yml        |   2 +-
 .github/workflows/coq-opam-package.yml |   2 +-
 .github/workflows/coq-windows.yml      |   2 +-
 .github/workflows/coq.yml              | 110 -------------------------
 4 files changed, 3 insertions(+), 113 deletions(-)
 delete mode 100644 .github/workflows/coq.yml

diff --git a/.github/workflows/coq-macos.yml b/.github/workflows/coq-macos.yml
index c343973641..d8643a7fb7 100644
--- a/.github/workflows/coq-macos.yml
+++ b/.github/workflows/coq-macos.yml
@@ -19,7 +19,7 @@ jobs:
 
     env:
       NJOBS: "2"
-      COQ_VERSION: "8.15.2" # minimal major version required for bedrock2 components
+      COQ_VERSION: "8.16.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 9e7d872ae6..44cf205762 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.15.2']
+        coq-version: ['dev', '8.16.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 5439a21934..b234a69a4b 100644
--- a/.github/workflows/coq-windows.yml
+++ b/.github/workflows/coq-windows.yml
@@ -22,7 +22,7 @@ jobs:
 
     env:
       NJOBS: "2"
-      COQ_VERSION: "8.15.2" # https://packages.debian.org/testing/coq
+      COQ_VERSION: "8.16.0" # https://packages.debian.org/testing/coq
       COQEXTRAFLAGS: "-async-proofs-j 1"
       COQCHKEXTRAFLAGS: ""
       OPAMYES: "true"
diff --git a/.github/workflows/coq.yml b/.github/workflows/coq.yml
deleted file mode 100644
index 37de4f832c..0000000000
--- a/.github/workflows/coq.yml
+++ /dev/null
@@ -1,110 +0,0 @@
-name: CI (Coq)
-
-on:
-  push:
-    branches: [ master , sp2019latest , v8.6 , v8.8 , v8.10 ]
-  pull_request:
-  workflow_dispatch:
-  schedule:
-    - cron: '0 0 1 * *'
-
-jobs:
-  build:
-
-    strategy:
-      fail-fast: false
-      matrix:
-        include:
-        - env: { COQ_VERSION: "Ubuntu LTS", COQ_PACKAGE: "coq libcoq-ocaml-dev"     , SKIP_VALIDATE: "1", COQCHKEXTRAFLAGS: ""                      , PPA: "" }
-          os: 'ubuntu-22.04'
-
-    runs-on: ${{ matrix.os }}
-    env: ${{ matrix.env }}
-    name: ${{ matrix.env.COQ_VERSION }}
-
-    concurrency:
-      group: ${{ github.workflow }}-${{ matrix.env.COQ_VERSION }}-${{ github.head_ref || github.run_id }}
-      cancel-in-progress: true
-
-    steps:
-    - uses: actions/checkout@v3
-      with:
-        submodules: recursive
-    - name: install Coq
-      run: |
-        if [ ! -z "$PPA" ]; then sudo add-apt-repository "$PPA" -y; fi
-        sudo apt-get -o Acquire::Retries=30 update -q
-        sudo apt-get -o Acquire::Retries=30 install ocaml-findlib $COQ_PACKAGE -y --allow-unauthenticated
-    - uses: haskell/actions/setup@v2
-      with:
-        ghc-version: 'latest'
-        cabal-version: 'latest'
-    - name: echo build params
-      run: etc/ci/describe-system-config.sh
-    - name: deps
-      run: etc/ci/github-actions-make.sh -j2 deps
-    - name: all-except-generated
-      run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 all-except-generated
-    - name: generated-files
-      run: etc/ci/github-actions-make.sh ${EXTRA_GH_REPORTIFY} -j2 generated-files
-      if: github.event_name == 'pull_request' || ${{ matrix.env.COQ_VERSION }} != 'master'
-    - run: tar -czvf generated-files.tgz fiat-*/
-      if: ${{ failure() }}
-    - name: upload generated files
-      uses: actions/upload-artifact@v3
-      with:
-        name: generated-files-${{ matrix.env.COQ_VERSION }}
-        path: generated-files.tgz
-      if: ${{ failure() }}
-    - name: upload OCaml files
-      uses: actions/upload-artifact@v3
-      with:
-        name: ExtractionOCaml-${{ matrix.env.COQ_VERSION }}
-        path: src/ExtractionOCaml
-      if: always ()
-    - name: standalone-haskell
-      run: etc/ci/github-actions-make.sh -j1 standalone-haskell GHCFLAGS='+RTS -M6G -RTS'
-    - name: upload Haskell files
-      uses: actions/upload-artifact@v3
-      with:
-        name: ExtractionHaskell-${{ matrix.env.COQ_VERSION }}
-        path: src/ExtractionHaskell
-      if: always ()
-    - name: display timing info
-      run: cat time-of-build-pretty.log
-    - name: display per-line timing info
-      run: etc/ci/github-actions-display-per-line-timing.sh
-#    - name: upload timing and .vo info
-#      uses: actions/upload-artifact@v3
-#      with:
-#        name: build-outputs-${{ matrix.env.COQ_VERSION }}
-#        path: .
-#      if: always ()
-    - name: validate
-      run: make TIMED=1 validate COQCHKFLAGS="-o ${COQCHKEXTRAFLAGS}"
-      if: matrix.env.SKIP_VALIDATE == '' && github.event_name != 'pull_request'
-  test-amd64:
-
-    runs-on: ubuntu-latest
-
-    concurrency:
-      group: ${{ github.workflow }}-test-amd64-${{ github.head_ref || github.run_id }}
-      cancel-in-progress: true
-    needs: build
-
-    steps:
-    - name: checkout repo
-      uses: actions/checkout@v3
-      with:
-        submodules: recursive
-    - name: Download a Build Artifact
-      uses: actions/download-artifact@v3
-      with:
-        name: "ExtractionOCaml-Ubuntu LTS"
-        path: src/ExtractionOCaml
-    - name: make binaries executable
-      run: chmod +x src/ExtractionOCaml/*
-    - name: make only-test-amd64-files
-      run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files SLOWEST_FIRST=1
-      env: 
-        ALLOW_DIFF: 1