diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index 8b844e33c7..44ba1ec508 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -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 /_output/ with /.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 '
Failing tests' + echo + echo '```' + head -c 40000 /tmp/gh-aw/agent/fstar-artifact/logs/failing-tests.txt + echo '```' + echo + echo '
' + 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,