mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 06:28:18 +00:00
Code Activity

CI: collect F* test suite failure artifacts (#10390)

Browse source 
Fixes #10375.

## Analysis of [run
30786942559](https://github.com/Z3Prover/z3/actions/runs/30786942559)

The job is green, but `make test` exited 2. Every failing test is an
**expected-output mismatch**, and all 70 of them differ only by the
`--proof_recovery` banner:

```
   - The SMT solver could not prove the query.
+  - This query was retried due to the --proof_recovery option, yet it still
+    failed on all attempts.
```

That text comes from `--proof_recovery` in the workflow's own
`fstar_otherflags` default, which F*'s `.expected` files do not carry —
so these are configuration mismatches, not Z3 regressions. There are
also failures that never reach the solver (`hello.__all`, `dune`,
extraction diffs on `RemoveUnusedTypars_B.fs` / `Bug3865.out`).

None of that was reconstructible from the artifact: the run uploaded 526
`.smt2` files, almost all logged failing queries from negative tests
that are *supposed* to fail, and nothing else. No logs, no produced
output, no `.expected` oracle, no diff.

## Changes

* **`Resolve FStar options`** — computes `OTHERFLAGS` once (removing the
duplicated `--z3version` extraction) and enforces
`--log_failing_queries`. Scheduled runs get no `workflow_dispatch`
inputs, so the options that make F* emit `.smt2` files are hard-wired
instead of assumed to come from the inputs. The effective flags are
recorded in the artifact, the job summary and the discussion.
* **`Build FStar`** now tees to a log, as the test step already did.
* **`Collect FStar failure artifacts`** replaces `Collect generated SMT2
files` and produces:
* `logs/` — build log, test log, versions, commit, effective flags, and
a `failing-tests.txt` summary of mismatched outputs plus failed make
targets;
  * `smt2/` — the logged failing queries, as before;
* `test-output/` — for every expected-output test whose result differs
from its oracle: `<name>.actual`, `<name>.expected` and a unified
`<name>.diff`.
* **Upload always runs.** Previously, if no `.smt2` file existed the
collect step short-circuited and the upload was skipped, so the hardest
failures produced no artifact at all.
* The failure summary is surfaced in the **job summary** and in the
**discussion**, so a mismatch is visible without downloading anything.

Applied to the run above, `test-output/` would hold the
actual/expected/diff triple for each of the 70 mismatches and
`failing-tests.txt` would list them alongside `hello.__all` and the
other non-SMT failures.

## Validation

The workflow parses as YAML; every `run:` block passes `bash -n` and the
`github-script` body passes `node --check`. The new steps were executed
locally against a fixture reproducing the run's failure shapes:

* mismatched `.output` / `.json_output` / `.ideout` / `.fs` / `.out`
files are collected with correct diffs; the generated diff for
`Basic.fst.output` reproduces the annotation in the run exactly;
* matching outputs, `_output` files with no `.expected`, and files over
4 MB are correctly skipped;
* failed make targets are parsed from both logs;
* with no F* tree at all (build failed before clone) the collector still
exits 0 and the artifact still contains the logs;
* option resolution was checked with the default flags, with
`--log_failing_queries` absent, with empty flags, and with an
unparseable `z3 --version`;
* the rendered discussion body is 53 040 characters in the worst case,
below GitHub's 65 536 limit.

Behaviour deliberately unchanged: the build and test steps keep
`continue-on-error`, so a broken F* master still does not block the
report.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This commit is contained in:
Lev Nachmanson 2026-08-05 09:03:37 -07:00 • committed by GitHub
parent 650e2a4e5a
commit 249778137d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 150 additions and 47 deletions
Download patch file Download diff file Expand all files Collapse all files

197
.github/workflows/fstar-master-build.yml vendored
View file

@ -90,6 +90,25 @@ jobs:
ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3-4.13.3
/tmp/gh-aw/agent/z3-bin/z3 --version
# Scheduled runs receive no workflow_dispatch inputs, so the effective F* options
# come from the hard-wired env defaults above. Resolve them once here, and make sure
# the options that cause F* to emit .smt2 files are always present: without them the
# build and the test suite fail without leaving any query behind to analyse.
- name: Resolve FStar options
run: |
set -euo pipefail
Z3_VERSION="$(sed -E -n 's/^Z3 version ([0-9]+\.[0-9]+\.[0-9]+).*/\1/p' /tmp/gh-aw/agent/z3-version.txt | head -1)"
test -n "$Z3_VERSION" || { echo "Error: Failed to extract Z3 version from /tmp/gh-aw/agent/z3-version.txt (expected: 'Z3 version X.Y.Z')"; cat /tmp/gh-aw/agent/z3-version.txt || true; exit 1; }
OTHERFLAGS="--z3version $Z3_VERSION $FSTAR_OTHERFLAGS"
case " $OTHERFLAGS " in
*" --log_failing_queries "*) ;;
*) OTHERFLAGS="$OTHERFLAGS --log_failing_queries" ;;
esac
echo "FSTAR_EFFECTIVE_OTHERFLAGS=$OTHERFLAGS" >> "$GITHUB_ENV"
printf '%s\n' "$OTHERFLAGS" | tee /tmp/gh-aw/agent/fstar-otherflags.txt
- name: Build FStar
id: build_fstar
continue-on-error: true
@ -105,10 +124,7 @@ jobs:
eval "$(opam env --switch="$FSTAR_OPAM_SWITCH")"
opam install --deps-only . --yes
Z3_VERSION="$(sed -E -n 's/^Z3 version ([0-9]+\.[0-9]+\.[0-9]+).*/\1/p' /tmp/gh-aw/agent/z3-version.txt | head -1)"
test -n "$Z3_VERSION" || { echo "Error: Failed to extract Z3 version from /tmp/gh-aw/agent/z3-version.txt (expected: 'Z3 version X.Y.Z')"; cat /tmp/gh-aw/agent/z3-version.txt || true; exit 1; }
PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="--z3version $Z3_VERSION $FSTAR_OTHERFLAGS" make -j"$(nproc)" -k
PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="$FSTAR_EFFECTIVE_OTHERFLAGS" make -j"$(nproc)" -k 2>&1 | tee /tmp/gh-aw/agent/fstar-build.log
test -x /tmp/gh-aw/agent/FStar/out/bin/fstar.exe || { echo "Error: FStar binary not found or not executable at /tmp/gh-aw/agent/FStar/out/bin/fstar.exe"; exit 1; }
/tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt
@ -121,58 +137,129 @@ jobs:
cd /tmp/gh-aw/agent/FStar
eval "$(opam env --switch="$FSTAR_OPAM_SWITCH")"
Z3_VERSION="$(sed -E -n 's/^Z3 version ([0-9]+\.[0-9]+\.[0-9]+).*/\1/p' /tmp/gh-aw/agent/z3-version.txt | head -1)"
test -n "$Z3_VERSION" || { echo "Error: Failed to extract Z3 version from /tmp/gh-aw/agent/z3-version.txt (expected: 'Z3 version X.Y.Z')"; exit 1; }
PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="$FSTAR_EFFECTIVE_OTHERFLAGS" make -j"$(nproc)" -k test 2>&1 | tee /tmp/gh-aw/agent/fstar-test.log
PATH="/tmp/gh-aw/agent/z3-bin:$PATH" OTHERFLAGS="--z3version $Z3_VERSION $FSTAR_OTHERFLAGS" make -j"$(nproc)" -k test 2>&1 | tee /tmp/gh-aw/agent/fstar-test.log
- name: Collect generated SMT2 files
id: collect_smt2
# Collect everything needed to triage a failure offline: the logs, the failing SMT2
# queries, and - for every expected-output test - the produced output, the .expected
# oracle and a unified diff between them. Test suite failures otherwise leave nothing
# behind, since only .smt2 files used to be uploaded.
- name: Collect FStar failure artifacts
id: collect_artifacts
if: always()
run: |
set -euo pipefail
rm -rf /tmp/gh-aw/agent/smt2-artifact
mkdir -p /tmp/gh-aw/agent/smt2-artifact
SMT2_PREVIEW=/tmp/gh-aw/agent/smt2-preview.md
SMT2_HEAD_LINES=1000
> "$SMT2_PREVIEW"
FSTAR_DIR=/tmp/gh-aw/agent/FStar
OUT=/tmp/gh-aw/agent/fstar-artifact
rm -rf "$OUT"
mkdir -p "$OUT/logs" "$OUT/smt2" "$OUT/test-output"
if [ -d /tmp/gh-aw/agent/FStar ]; then
mapfile -t SMT2_FILES < <(find /tmp/gh-aw/agent/FStar -type f -name '*.smt2' | sort)
else
SMT2_FILES=()
fi
if [ "${#SMT2_FILES[@]}" -eq 0 ]; then
echo "has_files=false" >> "$GITHUB_OUTPUT"
exit 0
fi
for file in "${SMT2_FILES[@]}"; do
rel="${file#/tmp/gh-aw/agent/FStar/}"
target="/tmp/gh-aw/agent/smt2-artifact/${rel}"
mkdir -p "$(dirname "$target")"
cp "$file" "$target"
{
printf '#### `%s`\n\n' "$rel"
printf '```smt2\n'
head -n "$SMT2_HEAD_LINES" "$file"
printf '\n```\n\n'
} >> "$SMT2_PREVIEW"
for name in z3-version.txt z3-runtime-check.txt fstar-version.txt fstar-commit.txt fstar-otherflags.txt fstar-build.log fstar-test.log; do
if [ -f "/tmp/gh-aw/agent/$name" ]; then
cp "/tmp/gh-aw/agent/$name" "$OUT/logs/$name"
fi
done
echo "has_files=true" >> "$GITHUB_OUTPUT"
SMT2_PREVIEW=/tmp/gh-aw/agent/smt2-preview.md
SMT2_HEAD_LINES=1000
: > "$SMT2_PREVIEW"
- name: Upload generated SMT2 artifact
id: upload_smt2
if: always() && steps.collect_smt2.outputs.has_files == 'true'
MISMATCH_LIST="$OUT/logs/mismatched-outputs.txt"
: > "$MISMATCH_LIST"
SMT2_COUNT=0
MISMATCH_COUNT=0
if [ -d "$FSTAR_DIR" ]; then
while IFS= read -r file; do
rel="${file#"$FSTAR_DIR"/}"
target="$OUT/smt2/${rel}"
mkdir -p "$(dirname "$target")"
cp "$file" "$target"
{
printf '#### `%s`\n\n' "$rel"
printf '```smt2\n'
head -n "$SMT2_HEAD_LINES" "$file"
printf '\n```\n\n'
} >> "$SMT2_PREVIEW"
SMT2_COUNT=$((SMT2_COUNT + 1))
done < <(find "$FSTAR_DIR" -type f -name '*.smt2' | sort)
# An expected-output test compares <dir>/_output/<name> with <dir>/<name>.expected.
while IFS= read -r file; do
expected="$(dirname "$(dirname "$file")")/$(basename "$file").expected"
[ -f "$expected" ] || continue
if cmp -s "$file" "$expected"; then continue; fi
rel="${file#"$FSTAR_DIR"/}"
target="$OUT/test-output/${rel}"
mkdir -p "$(dirname "$target")"
cp "$file" "$target.actual"
cp "$expected" "$target.expected"
diff -u "$expected" "$file" > "$target.diff" || true
printf '%s\n' "$rel" >> "$MISMATCH_LIST"
MISMATCH_COUNT=$((MISMATCH_COUNT + 1))
done < <(find "$FSTAR_DIR" -type f -path '*/_output/*' -size -4M \
\( -name '*.output' -o -name '*.json_output' -o -name '*.ideout' -o -name '*.out' \
-o -name '*.fs-out' -o -name '*.err' -o -name '*.ml' -o -name '*.fs' -o -name '*.krml' \) | sort)
fi
FAILING="$OUT/logs/failing-tests.txt"
{
printf 'Mismatched expected outputs: %s\n' "$MISMATCH_COUNT"
sed 's/^/ /' "$MISMATCH_LIST"
printf '\nFailed make targets:\n'
for log in /tmp/gh-aw/agent/fstar-build.log /tmp/gh-aw/agent/fstar-test.log; do
[ -f "$log" ] || continue
grep -oE 'make(\[[0-9]+\])?: \*\*\* \[[^]]*\] Error [0-9]+' "$log" || true
done | sed -E 's/.*\[([^]]*)\] Error [0-9]+$/ \1/' | sort -u
} > "$FAILING"
{
echo "smt2_count=$SMT2_COUNT"
echo "mismatch_count=$MISMATCH_COUNT"
} >> "$GITHUB_OUTPUT"
echo "Collected $SMT2_COUNT .smt2 file(s) and $MISMATCH_COUNT mismatched test output(s)."
cat "$FAILING"
- name: Upload FStar failure artifacts
id: upload_artifacts
if: always()
uses: actions/upload-artifact@v7
with:
name: fstar-generated-smt2-${{ github.run_id }}
path: /tmp/gh-aw/agent/smt2-artifact
if-no-files-found: error
name: fstar-artifacts-${{ github.run_id }}
path: /tmp/gh-aw/agent/fstar-artifact
if-no-files-found: warn
retention-days: 7
- name: Job summary
if: always()
env:
BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
TEST_OUTCOME: ${{ steps.test_fstar.outcome }}
SMT2_COUNT: ${{ steps.collect_artifacts.outputs.smt2_count }}
MISMATCH_COUNT: ${{ steps.collect_artifacts.outputs.mismatch_count }}
run: |
set -euo pipefail
{
echo "## FStar master build"
echo
echo "- FStar build: \`${BUILD_OUTCOME:-unknown}\`"
echo "- FStar test suite: \`${TEST_OUTCOME:-skipped}\`"
echo "- Effective OTHERFLAGS: \`$(cat /tmp/gh-aw/agent/fstar-otherflags.txt 2>/dev/null || echo unknown)\`"
echo "- Logged failing queries: ${SMT2_COUNT:-unknown}"
echo "- Mismatched expected outputs: ${MISMATCH_COUNT:-unknown}"
echo
if [ -f /tmp/gh-aw/agent/fstar-artifact/logs/failing-tests.txt ]; then
echo '<details><summary>Failing tests</summary>'
echo
echo '```'
head -c 40000 /tmp/gh-aw/agent/fstar-artifact/logs/failing-tests.txt
echo '```'
echo
echo '</details>'
fi
} >> "$GITHUB_STEP_SUMMARY"
- name: Create discussion summary
if: always()
uses: actions/github-script@v9
@ -180,7 +267,7 @@ jobs:
RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
FSTAR_TEST_OUTCOME: ${{ steps.test_fstar.outcome }}
SMT2_ARTIFACT_ID: ${{ steps.upload_smt2.outputs.artifact-id }}
SMT2_ARTIFACT_ID: ${{ steps.upload_artifacts.outputs.artifact-id }}
with:
script: |
const fs = require('fs');
@ -219,8 +306,21 @@ jobs:
: '';
const smt2ArtifactId = (process.env.SMT2_ARTIFACT_ID || '').trim();
const smt2ArtifactUrl = smt2ArtifactId ? `${process.env.RUN_URL}/artifacts/${smt2ArtifactId}` : '';
const failingTests = readIfExists('/tmp/gh-aw/agent/fstar-artifact/logs/failing-tests.txt') ?? '';
const maxFailingChars = 6000;
const failingSection = [
`### Failing tests`,
``,
'```',
failingTests
? (failingTests.length > maxFailingChars
? `${failingTests.slice(0, maxFailingChars)}\n... (truncated, see artifact logs/failing-tests.txt)`
: failingTests)
: 'No failure summary was produced.',
'```'
].join('\n');
const smt2PreviewFile = '/tmp/gh-aw/agent/smt2-preview.md';
const maxPreviewChars = 45000; // Keep below GitHub's 65536-character discussion body limit, leaving room for the test log tail and other sections.
const maxPreviewChars = 38000; // Keep below GitHub's 65536-character discussion body limit, leaving room for the failure summary, test log tail and other sections.
let smt2Preview = readIfExists(smt2PreviewFile) ?? '';
const smt2PreviewChars = Array.from(smt2Preview);
if (smt2PreviewChars.length > maxPreviewChars) {
@ -229,7 +329,7 @@ jobs:
const smt2Section = smt2ArtifactId
? [
`### Generated SMT2 files`,
`- Artifact: ${smt2ArtifactUrl}`,
`- Artifact (logs, failing \`.smt2\` queries, and mismatched test outputs with diffs): ${smt2ArtifactUrl}`,
``,
`First 1000 lines per generated \`.smt2\` file:`,
``,
@ -278,12 +378,15 @@ jobs:
`- fstar_opam_switch: \`${process.env.FSTAR_OPAM_SWITCH}\``,
`- fstar_otherflags: \`${process.env.FSTAR_OTHERFLAGS}\``,
`- fstar_run_tests: \`${process.env.FSTAR_RUN_TESTS}\``,
`- effective OTHERFLAGS: \`${readIfExists('/tmp/gh-aw/agent/fstar-otherflags.txt') ?? 'unknown'}\``,
``,
`### Produced versions`,
`- Z3: \`${z3VersionText}\``,
`- FStar: \`${fstarVersionText}\``,
`- FStar commit: \`${fstarCommit}\``,
``,
failingSection,
``,
smt2Section,
``,
testSection,