Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
36 changes: 36 additions & 0 deletions .github/workflows/abi-codegen-drift.yml
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,42 @@ jobs:
- name: Verify Idris is on PATH
run: idris2 --version

# Compiling an EXECUTABLE needs the Chez support tree
# (`<libdir>/support/chez/support.ss`); type-checking and building a
# LIBRARY does not. `verify-proofs.yml` only ever does the latter, so the
# cache this job deliberately shares with it was populated without that
# tree and this job died at
# INTERNAL ERROR: Can't find data file chez/support.ss
# on its very first run. Measured, not supposed: PR #811's gate run.
#
# `support/` is plain data (Scheme and C sources shipped in the Idris2
# repo); it needs no build, so a shallow clone is enough to repair it.
- name: Ensure the Chez support tree is installed
run: |
set -euo pipefail
libdir="$(idris2 --libdir)"
support="${libdir}/support"
if [ -f "${support}/chez/support.ss" ]; then
echo "chez support present: ${support}/chez/support.ss"
else
echo "chez support absent under ${support} -- installing from the Idris2 source tree"
rm -rf "${RUNNER_TEMP}/idris2-support-src"
git clone --depth 1 --branch "${IDRIS2_VERSION}" \
https://github.com/idris-lang/Idris2 "${RUNNER_TEMP}/idris2-support-src"
mkdir -p "${support}"
cp -R "${RUNNER_TEMP}/idris2-support-src/support/." "${support}/"
fi
# Assert, do not assume. A missing support tree previously surfaced as
# an opaque INTERNAL ERROR three steps later; fail here, by name.
if [ ! -f "${support}/chez/support.ss" ]; then
echo "::error::chez/support.ss still missing under ${support}"
if [ -d "${libdir}" ]; then
find "${libdir}" -maxdepth 3 -name 'support*' -print
fi
exit 1
fi
echo "support tree: ${support}"

- name: Build the generator
run: |
set -euo pipefail
Expand Down
26 changes: 20 additions & 6 deletions .github/workflows/zig.yml
Original file line number Diff line number Diff line change
Expand Up @@ -103,12 +103,26 @@ jobs:
zig test ffi/zig/src/unified-api-adapter.zig 2>&1 | tee "${RUNNER_TEMP}/zig-test.log"

# The denominator. `zig test` on a file containing no `test` blocks
# exits 0 -- a green tick that proves nothing. Insist that it says
# how many it ran, and that the number is not zero.
summary=$(grep -Eo '[0-9]+ of [0-9]+ test[s]? passed|All [0-9]+ tests passed' \
"${RUNNER_TEMP}/zig-test.log" | tail -1 || true)
count=$(printf '%s' "${summary}" | grep -Eo '[0-9]+' | tail -1 || true)
count=${count:-0}
# exits 0 and prints "All 0 tests passed." -- a green tick that proves
# nothing. Insist that it says how many it ran, and that it is not 0.
#
# awk, not `grep ... || true`: grep exits 1 when it matches nothing,
# which under `set -e` needs suppressing, and a suppressed exit code
# is indistinguishable from a masked failure to a reader or a
# scanner. awk exits 0 whether or not it matched, so the no-match
# case needs no suppression and the check below stays the only thing
# that can fail this step.
count=$(awk '
match($0, /All [0-9]+ tests passed/) ||
match($0, /[0-9]+ of [0-9]+ tests? passed/) { last = $0 }
END {
n = 0
while (match(last, /[0-9]+/)) {
n = substr(last, RSTART, RLENGTH)
last = substr(last, RSTART + RLENGTH)
}
print n + 0
}' "${RUNNER_TEMP}/zig-test.log")

echo "zig tests run: ${count}"
{
Expand Down
Loading