mirror of
https://github.com/Z3Prover/z3
synced 2026-06-10 19:07:18 +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>
195 lines
8.1 KiB
YAML
195 lines
8.1 KiB
YAML
name: Build FStar master with Z3 master
|
|
|
|
on:
|
|
schedule:
|
|
- cron: "9 4 * * *"
|
|
workflow_dispatch:
|
|
inputs:
|
|
z3_ref:
|
|
description: Z3 ref to checkout and build
|
|
required: false
|
|
default: master
|
|
z3_cmake_args:
|
|
description: Extra CMake arguments for Z3 build
|
|
required: false
|
|
default: ""
|
|
z3_runtime_args:
|
|
description: "Extra Z3 runtime args (example: smt.ho_matching=true)"
|
|
required: false
|
|
default: "smt.ho_matching=true"
|
|
fstar_ref:
|
|
description: FStar ref to checkout and build
|
|
required: false
|
|
default: _nik_higher_order_smt
|
|
fstar_opam_switch:
|
|
description: OCaml switch for FStar build
|
|
required: false
|
|
default: "4.14.2"
|
|
fstar_otherflags:
|
|
description: "Extra FStar OTHERFLAGS"
|
|
required: false
|
|
default: "--split_queries --log_failing_queries --ext higher_order_smt --proof_recovery"
|
|
discussion_category:
|
|
description: Discussion category name
|
|
required: false
|
|
default: "Agentic Workflows"
|
|
|
|
permissions:
|
|
contents: read
|
|
discussions: write
|
|
|
|
concurrency:
|
|
group: ${{ github.workflow }}
|
|
cancel-in-progress: false
|
|
|
|
jobs:
|
|
build-and-report:
|
|
runs-on: ubuntu-latest
|
|
timeout-minutes: 180
|
|
env:
|
|
Z3_REF: ${{ github.event.inputs.z3_ref || 'master' }}
|
|
Z3_CMAKE_ARGS: ${{ github.event.inputs.z3_cmake_args || '' }}
|
|
Z3_RUNTIME_ARGS: ${{ github.event.inputs.z3_runtime_args || 'smt.ho_matching=true' }}
|
|
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 || '' }}
|
|
DISCUSSION_CATEGORY: ${{ github.event.inputs.discussion_category || 'Agentic Workflows' }}
|
|
steps:
|
|
- name: Checkout Z3
|
|
uses: actions/checkout@v6.0.3
|
|
with:
|
|
ref: ${{ env.Z3_REF }}
|
|
fetch-depth: 1
|
|
|
|
- name: Install dependencies
|
|
run: |
|
|
set -euo pipefail
|
|
sudo apt-get update -y
|
|
sudo apt-get install -y cmake ninja-build python3 git curl unzip opam m4 pkg-config libgmp-dev
|
|
|
|
- name: Build Z3
|
|
run: |
|
|
set -euo pipefail
|
|
mkdir -p /tmp/gh-aw/agent
|
|
cmake -S . -B build/release -G Ninja -DCMAKE_BUILD_TYPE=Release $Z3_CMAKE_ARGS
|
|
ninja -C build/release z3
|
|
./build/release/z3 --version | tee /tmp/gh-aw/agent/z3-version.txt
|
|
printf '(check-sat)\n' | ./build/release/z3 $Z3_RUNTIME_ARGS -in | tee /tmp/gh-aw/agent/z3-runtime-check.txt
|
|
|
|
- name: Prepare Z3 aliases for FStar
|
|
run: |
|
|
set -euo pipefail
|
|
mkdir -p /tmp/gh-aw/agent/z3-bin
|
|
ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3
|
|
ln -sf "$GITHUB_WORKSPACE/build/release/z3" /tmp/gh-aw/agent/z3-bin/z3-4.8.5
|
|
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
|
|
|
|
- name: Build FStar
|
|
id: build_fstar
|
|
continue-on-error: true
|
|
run: |
|
|
set -euo pipefail
|
|
rm -rf /tmp/gh-aw/agent/FStar
|
|
git clone --depth=1 --recurse-submodules --branch "$FSTAR_REF" https://github.com/FStarLang/FStar.git /tmp/gh-aw/agent/FStar
|
|
cd /tmp/gh-aw/agent/FStar
|
|
echo "FStar commit: $(git rev-parse HEAD)" | tee /tmp/gh-aw/agent/fstar-commit.txt
|
|
|
|
opam init --disable-sandboxing --yes
|
|
opam switch create "$FSTAR_OPAM_SWITCH" --yes || opam switch "$FSTAR_OPAM_SWITCH"
|
|
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
|
|
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: 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 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 = 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;
|
|
const repo = context.repo.repo;
|
|
const categoryName = process.env.DISCUSSION_CATEGORY;
|
|
|
|
const categoryQuery = await github.graphql(
|
|
`query($owner:String!, $repo:String!) {
|
|
repository(owner:$owner, name:$repo) {
|
|
id
|
|
discussionCategories(first:50) {
|
|
nodes { id name }
|
|
}
|
|
}
|
|
}`,
|
|
{ owner, repo }
|
|
);
|
|
|
|
const categories = categoryQuery.repository.discussionCategories.nodes || [];
|
|
const normalized = categoryName.trim().toLowerCase();
|
|
const category = categories.find(c => c.name.toLowerCase() === normalized);
|
|
if (!category) {
|
|
throw new Error(`Discussion category '${categoryName}' not found`);
|
|
}
|
|
|
|
const body = [
|
|
`### Build status`,
|
|
`- ✅ Z3 build completed`,
|
|
`- ${fstarStatus}`,
|
|
``,
|
|
`### Inputs used`,
|
|
`- z3_ref: \`${process.env.Z3_REF}\``,
|
|
`- z3_cmake_args: \`${process.env.Z3_CMAKE_ARGS}\``,
|
|
`- z3_runtime_args: \`${process.env.Z3_RUNTIME_ARGS}\``,
|
|
`- fstar_ref: \`${process.env.FSTAR_REF}\``,
|
|
`- fstar_opam_switch: \`${process.env.FSTAR_OPAM_SWITCH}\``,
|
|
`- fstar_otherflags: \`${process.env.FSTAR_OTHERFLAGS}\``,
|
|
``,
|
|
`### Produced versions`,
|
|
`- Z3: \`${z3VersionText}\``,
|
|
`- FStar: \`${fstarVersionText}\``,
|
|
`- FStar commit: \`${fstarCommit}\``,
|
|
``,
|
|
`### Run`,
|
|
`- Workflow run: ${process.env.RUN_URL}`
|
|
].join('\n');
|
|
|
|
await github.graphql(
|
|
`mutation($repositoryId:ID!, $categoryId:ID!, $title:String!, $body:String!) {
|
|
createDiscussion(input:{
|
|
repositoryId:$repositoryId,
|
|
categoryId:$categoryId,
|
|
title:$title,
|
|
body:$body
|
|
}) {
|
|
discussion { url }
|
|
}
|
|
}`,
|
|
{
|
|
repositoryId: categoryQuery.repository.id,
|
|
categoryId: category.id,
|
|
title: `FStar build with configurable Z3 inputs — ${date}`,
|
|
body
|
|
}
|
|
);
|