From d49c389a695f3070faccf18ddb377e42df853dda Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 28 Jul 2026 13:45:44 -0700 Subject: [PATCH] CI: run FStar test suite in fstar-master-build workflow Build FStar only type-checks the compiler and ulib. Running `make test` afterwards exercises the tests/examples suite, which sends many more SMT queries to the freshly built Z3 and produces more logged failing queries for the existing .smt2 collection step. The new step runs in the FStar clone with the same opam env, PATH to the Z3 aliases and OTHERFLAGS as the build. It is gated on a new fstar_run_tests input (default true) and on the build succeeding, and is continue-on-error so a test failure does not hide the build result or skip reporting. The discussion summary reports the test outcome and the tail of the test log; the SMT2 preview budget is reduced accordingly to stay below the discussion body size limit. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- .github/workflows/fstar-master-build.yml | 47 +++++++++++++++++++++++- 1 file changed, 46 insertions(+), 1 deletion(-) diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml index bfee2fc48c..8b844e33c7 100644 --- a/.github/workflows/fstar-master-build.yml +++ b/.github/workflows/fstar-master-build.yml @@ -29,6 +29,10 @@ on: description: "Extra FStar OTHERFLAGS" required: false default: "--split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery" + fstar_run_tests: + description: "Run the FStar test suite (make test) after the build" + required: false + default: "true" discussion_category: description: Discussion category name required: false @@ -53,6 +57,7 @@ jobs: FSTAR_REF: ${{ github.event.inputs.fstar_ref || 'master' }} FSTAR_OPAM_SWITCH: ${{ github.event.inputs.fstar_opam_switch || '4.14.2' }} FSTAR_OTHERFLAGS: ${{ github.event.inputs.fstar_otherflags || '--split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery' }} + FSTAR_RUN_TESTS: ${{ github.event.inputs.fstar_run_tests || 'true' }} DISCUSSION_CATEGORY: ${{ github.event.inputs.discussion_category || 'Agentic Workflows' }} steps: - name: Checkout Z3 @@ -107,6 +112,20 @@ jobs: 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 + - name: Run FStar test suite + id: test_fstar + if: env.FSTAR_RUN_TESTS == 'true' && steps.build_fstar.outcome == 'success' + continue-on-error: true + run: | + set -euo pipefail + 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="--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 if: always() @@ -160,6 +179,7 @@ jobs: env: 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 }} with: script: | @@ -176,10 +196,31 @@ jobs: const fstarStatus = fstarBuildSucceeded ? '✅ FStar build completed' : `⚠️ FStar build ${fstarBuildOutcome} (pipeline continued)`; + const fstarTestOutcome = process.env.FSTAR_TEST_OUTCOME || 'skipped'; + const fstarTestStatus = fstarTestOutcome === 'success' + ? '✅ FStar test suite (`make test`) passed' + : fstarTestOutcome === 'skipped' + ? 'ℹ️ FStar test suite (`make test`) skipped' + : `⚠️ FStar test suite (\`make test\`) ${fstarTestOutcome} (pipeline continued)`; + const testLog = readIfExists('/tmp/gh-aw/agent/fstar-test.log') ?? ''; + const maxTestLogChars = 8000; + let testLogTail = testLog ? testLog.split('\n').slice(-200).join('\n') : ''; + if (testLogTail.length > maxTestLogChars) { + testLogTail = `... (truncated)\n${testLogTail.slice(-maxTestLogChars)}`; + } + const testSection = testLog + ? [ + `### FStar test suite (last 200 log lines)`, + ``, + '```', + testLogTail, + '```' + ].join('\n') + : ''; const smt2ArtifactId = (process.env.SMT2_ARTIFACT_ID || '').trim(); const smt2ArtifactUrl = smt2ArtifactId ? `${process.env.RUN_URL}/artifacts/${smt2ArtifactId}` : ''; const smt2PreviewFile = '/tmp/gh-aw/agent/smt2-preview.md'; - const maxPreviewChars = 55000; // Keep below GitHub's 65536-character discussion body limit, leaving room for non-preview sections. + const maxPreviewChars = 45000; // Keep below GitHub's 65536-character discussion body limit, leaving room for the test log tail and other sections. let smt2Preview = readIfExists(smt2PreviewFile) ?? ''; const smt2PreviewChars = Array.from(smt2Preview); if (smt2PreviewChars.length > maxPreviewChars) { @@ -227,6 +268,7 @@ jobs: `### Build status`, `- ✅ Z3 build completed`, `- ${fstarStatus}`, + `- ${fstarTestStatus}`, ``, `### Inputs used`, `- z3_ref: \`${process.env.Z3_REF}\``, @@ -235,6 +277,7 @@ jobs: `- fstar_ref: \`${process.env.FSTAR_REF}\``, `- fstar_opam_switch: \`${process.env.FSTAR_OPAM_SWITCH}\``, `- fstar_otherflags: \`${process.env.FSTAR_OTHERFLAGS}\``, + `- fstar_run_tests: \`${process.env.FSTAR_RUN_TESTS}\``, ``, `### Produced versions`, `- Z3: \`${z3VersionText}\``, @@ -243,6 +286,8 @@ jobs: ``, smt2Section, ``, + testSection, + ``, `### Run`, `- Workflow run: ${process.env.RUN_URL}` ].join('\n');