Skip to content

Commit 73e5945

Browse files
authored
Allow host libc to mismatch debian container libc when testing binary (#1893)
* Use older version of ubuntu on debian to fix libc issues cf https://github.com/mit-plv/fiat-crypto/actions/runs/8990595838/job/24703815722?pr=1891#step:6:22 * Allow failure of binary on host for debian
1 parent 724035e commit 73e5945

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

.github/workflows/coq-debian.yml

+6-1
Original file line numberDiff line numberDiff line change
@@ -121,6 +121,8 @@ jobs:
121121
- name: List files
122122
run: find dist
123123
- run: chmod +x dist/fiat_crypto
124+
- name: host build params
125+
run: etc/ci/describe-system-config.sh
124126
- name: Test files (host)
125127
run: |
126128
echo "::group::file fiat_crypto"
@@ -129,7 +131,10 @@ jobs:
129131
echo "::group::ldd fiat_crypto"
130132
ldd dist/fiat_crypto
131133
echo "::endgroup::"
132-
etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto
134+
etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto || {
135+
printf '::warning::Debian ${{ matrix.debian }} binary does not run on ubuntu: %s\n' \
136+
"$(etc/ci/test-run-fiat-crypto.sh dist/fiat_crypto 2>&1 | tr '\n' '~' | sed 's/~/%0A/g')";
137+
}
133138
- name: setup Debian chroot
134139
run: etc/ci/setup-debian-chroot.sh "${{ matrix.debian }}"
135140
- name: Test files (container)

0 commit comments

Comments
 (0)