mirror of
https://github.com/Z3Prover/z3
synced 2026-06-10 10:57:15 +00:00
c174df4071
`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>
|
||
|---|---|---|
| .. | ||
| actions | ||
| agents | ||
| aw | ||
| prompts | ||
| scripts | ||
| skills | ||
| workflows | ||
| CI_MIGRATION.md | ||
| CI_TESTING.md | ||
| copilot-instructions.md | ||
| dependabot.yml | ||
| mcp.json | ||