From 8713744c7afa3747184a914c01233df9010495ae Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 11 Jun 2024 20:33:49 -0700
Subject: [PATCH] [CI] [debian] Containerize testing of standalone

This should hopefully deal with https://github.com/mit-plv/fiat-crypto/issues/1394#issuecomment-2160967034
---
 .github/workflows/coq-debian.yml | 42 +++++++++++++++++++++++++-------
 1 file changed, 33 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/coq-debian.yml b/.github/workflows/coq-debian.yml
index cf066bf94d7..eb31dbc0c62 100644
--- a/.github/workflows/coq-debian.yml
+++ b/.github/workflows/coq-debian.yml
@@ -102,7 +102,7 @@ jobs:
     - name: display per-line timing info
       run: etc/ci/github-actions-display-per-line-timing.sh
 
-  test-standalone:
+  test-standalone-host:
     strategy:
       fail-fast: false
       matrix:
@@ -135,10 +135,30 @@ jobs:
           printf '::warning::Debian ${{ matrix.debian }} binary does not run on ubuntu: %s\n' \
             "$(etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto 2>&1 | tr '\n' '~' | sed 's/~/%0A/g')";
         }
-    - name: setup Debian chroot
-      run: etc/ci/setup-debian-chroot.sh "${{ matrix.debian }}"
+
+  test-standalone-container:
+    strategy:
+      fail-fast: false
+      matrix:
+        include:
+        - debian: sid
+        #- debian: bookworm # restore once 8.17 lands in Debian stable
+    runs-on: ubuntu-latest
+    container: debian:${{ matrix.debian }}
+    needs: build
+    steps:
+    - uses: actions/checkout@v4
+    - name: Download standalone ${{ matrix.debian }}
+      uses: actions/download-artifact@v4
+      with:
+        name: standalone-${{ matrix.debian }}
+        path: dist/
+    - name: List files
+      run: find dist
+    - run: chmod +x dist/fiat_crypto
+    - name: host build params
+      run: etc/ci/describe-system-config.sh
     - name: Test files (container)
-      shell: in-debian-chroot.sh {0}
       run: |
         echo "::group::file fiat_crypto"
         file dist/fiat_crypto
@@ -187,18 +207,22 @@ jobs:
 
   debian-check-all:
     runs-on: ubuntu-latest
-    needs: [build, test-standalone, publish-standalone-dry-run]
+    needs: [build, test-standalone-host, test-standalone-container, publish-standalone-dry-run]
     if: always()
     steps:
     - run: echo 'build passed'
       if: ${{ needs.build.result == 'success' }}
-    - run: echo 'test-standalone passed'
-      if: ${{ needs.test-standalone.result == 'success' }}
+    - run: echo 'test-standalone-host passed'
+      if: ${{ needs.test-standalone-host.result == 'success' }}
+    - run: echo 'test-standalone-container passed'
+      if: ${{ needs.test-standalone-container.result == 'success' }}
     - run: echo 'publish-standalone-dry-run passed'
       if: ${{ needs.publish-standalone-dry-run.result == 'success' }}
     - run: echo 'build failed' && false
       if: ${{ needs.build.result != 'success' }}
-    - run: echo 'test-standalone failed' && false
-      if: ${{ needs.test-standalone.result != 'success' }}
+    - run: echo 'test-standalone-host failed' && false
+      if: ${{ needs.test-standalone-host.result != 'success' }}
+    - run: echo 'test-standalone-container failed' && false
+      if: ${{ needs.test-standalone-container.result != 'success' }}
     - run: echo 'publish-standalone-dry-run failed' && false
       if: ${{ needs.publish-standalone-dry-run.result != 'success' }}