From dcd567854191ad4e1abd293ddecd2a8df1048d8d Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 12 Nov 2023 22:12:59 -0800
Subject: [PATCH] Only test full amd64 files in Docker CI (#1722)

We remove the slow test from debian CI, hopefully speeding up CI
execution significantly, replacing them with the lite-amd64 tests, and
add the lite-amd64 tests to alpine.
---
 .github/workflows/coq-alpine.yml |  3 +++
 .github/workflows/coq-debian.yml | 39 ++++----------------------------
 .github/workflows/coq-docker.yml |  2 +-
 3 files changed, 8 insertions(+), 36 deletions(-)

diff --git a/.github/workflows/coq-alpine.yml b/.github/workflows/coq-alpine.yml
index 6ab7f719ae..80fe39aa46 100644
--- a/.github/workflows/coq-alpine.yml
+++ b/.github/workflows/coq-alpine.yml
@@ -86,6 +86,9 @@ jobs:
         name: ExtractionHaskell-${{ matrix.alpine }}
         path: src/ExtractionHaskell
       if: always ()
+    - name: only-test-amd64-files-lite
+      shell: alpine.sh {0}
+      run: make TIMED=1 TIMING=1 -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
     - name: display timing info
       run: cat time-of-build-pretty.log || true
     - name: display per-line timing info
diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
index 774f3725bd..1c9b945732 100644
--- a/.github/workflows/coq-debian.yml
+++ b/.github/workflows/coq-debian.yml
@@ -78,51 +78,20 @@ jobs:
         name: ExtractionHaskell-${{ matrix.env.DEBIAN }}
         path: src/ExtractionHaskell
       if: always ()
+    - name: only-test-amd64-files-lite
+      shell: in-debian-chroot.sh {0}
+      run: etc/ci/github-actions-make.sh -j2 only-test-amd64-files-lite SLOWEST_FIRST=1
     - 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
 
-  test-amd64:
-
-    runs-on: ubuntu-latest
-    env: { DEBIAN: "sid" }
-
-    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@v4
-      with:
-        submodules: recursive
-    - name: setup Debian chroot
-      run: etc/ci/setup-debian-chroot.sh "$DEBIAN"
-    - name: Download a Build Artifact
-      uses: actions/download-artifact@v3
-      with:
-        name: ExtractionOCaml-sid
-        path: src/ExtractionOCaml
-    - name: make binaries executable
-      run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x
-    - name: make only-test-amd64-files
-      shell: in-debian-chroot.sh {0}
-      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]
+    needs: [build]
     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-docker.yml b/.github/workflows/coq-docker.yml
index 9ec9954229..7d015e3236 100644
--- a/.github/workflows/coq-docker.yml
+++ b/.github/workflows/coq-docker.yml
@@ -126,7 +126,7 @@ jobs:
         name: ExtractionOCaml-master
         path: src/ExtractionOCaml
     - name: make binaries executable
-      run: chmod +x src/ExtractionOCaml/*
+      run: git check-ignore src/ExtractionOCaml/* | grep -v '\.' | xargs chmod +x
     - name: only-test-amd64-files
       run: etc/ci/github-actions-make.sh -f Makefile.examples -j2 only-test-amd64-files SLOWEST_FIRST=1
       env: