From c174df4071783ca81c03e38bf8ceccc18f196c05 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Mon, 8 Jun 2026 11:21:54 -0700
Subject: [PATCH] Allow FStar build failures without blocking build-and-report
 workflow progression (#9769)

`build-and-report` was failing hard when the `Build FStar` step hit
prover regressions, preventing downstream reporting from running. This
change makes FStar failures non-blocking and ensures the reporting path
still executes with an explicit FStar outcome.

- **Workflow failure propagation**
  - Marked `Build FStar` as non-blocking:
    - added `id: build_fstar`
    - added `continue-on-error: true`

- **Guaranteed reporting execution**
- Made the summary step unconditional with `if: always()` so it runs
even when FStar fails.

- **Robust summary generation**
  - Passed step outcome into the script (`FSTAR_BUILD_OUTCOME`).
  - Hardened file reads for missing FStar artifacts/version files.
- Report body now reflects actual FStar outcome (`success` vs
non-success) while preserving pipeline continuity.

```yaml
- name: Build FStar
  id: build_fstar
  continue-on-error: true
  run: |
    # existing FStar build commands

- name: Create discussion summary
  if: always()
  env:
    FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
  uses: actions/github-script@v9
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 .github/workflows/fstar-master-build.yml | 20 +++++++++++++++-----
 1 file changed, 15 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml
index 4b674fc33..f5b9417f2 100644
--- a/.github/workflows/fstar-master-build.yml
+++ b/.github/workflows/fstar-master-build.yml
@@ -86,6 +86,8 @@ jobs:
           /tmp/gh-aw/agent/z3-bin/z3 --version
 
       - name: Build FStar
+        id: build_fstar
+        continue-on-error: true
         run: |
           set -euo pipefail
           rm -rf /tmp/gh-aw/agent/FStar
@@ -106,18 +108,26 @@ jobs:
           /tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt
 
       - name: Create discussion summary
+        if: always()
         uses: actions/github-script@v9
         env:
           RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
         with:
           script: |
             const fs = require('fs');
 
-            const z3VersionText = fs.readFileSync('/tmp/gh-aw/agent/z3-version.txt', 'utf8').trim();
-            const fstarVersionFile = fs.readFileSync('/tmp/gh-aw/agent/fstar-version.txt', 'utf8').trim();
+            const readIfExists = (path) => fs.existsSync(path) ? fs.readFileSync(path, 'utf8').trim() : null;
+            const z3VersionText = readIfExists('/tmp/gh-aw/agent/z3-version.txt') ?? 'unknown';
+            const fstarVersionFile = readIfExists('/tmp/gh-aw/agent/fstar-version.txt') ?? '';
             const fstarVersionText = fstarVersionFile ? fstarVersionFile.split('\n')[0] : 'unknown';
-            const fstarCommitLine = fs.readFileSync('/tmp/gh-aw/agent/fstar-commit.txt', 'utf8').trim();
-            const fstarCommit = fstarCommitLine.replace(/^FStar commit:\s*/, '');
+            const fstarCommitLine = readIfExists('/tmp/gh-aw/agent/fstar-commit.txt') ?? '';
+            const fstarCommit = fstarCommitLine ? fstarCommitLine.replace(/^FStar commit:\s*/, '') : 'unknown';
+            const fstarBuildOutcome = process.env.FSTAR_BUILD_OUTCOME || 'unknown';
+            const fstarBuildSucceeded = fstarBuildOutcome === 'success';
+            const fstarStatus = fstarBuildSucceeded
+              ? '✅ FStar build completed'
+              : `⚠️ FStar build ${fstarBuildOutcome} (pipeline continued)`;
             const date = new Date().toISOString().slice(0, 10);
 
             const owner = context.repo.owner;
@@ -146,7 +156,7 @@ jobs:
             const body = [
               `### Build status`,
               `- ✅ Z3 build completed`,
-              `- ✅ FStar build completed`,
+              `- ${fstarStatus}`,
               ``,
               `### Inputs used`,
               `- z3_ref: \`${process.env.Z3_REF}\``,