Skip to content

feat(network): window-splitting 802.1Qbv GCL synthesis baseline (REQ-TSN-SYNTH-QBV-SPLIT-BASE-001) #137

feat(network): window-splitting 802.1Qbv GCL synthesis baseline (REQ-TSN-SYNTH-QBV-SPLIT-BASE-001)

feat(network): window-splitting 802.1Qbv GCL synthesis baseline (REQ-TSN-SYNTH-QBV-SPLIT-BASE-001) #137

name: Verification Gate
on:
pull_request:
branches: [main]
workflow_dispatch:
concurrency:
group: ${{ github.workflow }}-${{ github.head_ref || github.ref }}
cancel-in-progress: true
permissions:
contents: read
pull-requests: write
jobs:
rivet-verification:
name: Verification Gate (rivet-driven)
runs-on: [self-hosted, linux, x64, rust-cpu]
# 60m budget: TEST-PROOF-* steps run `cd proofs && lake build`, which
# against Mathlib on a cold elan cache takes 25–35 min. Once smithy
# adds Lake build-artifact caching across runs, this can drop back
# toward 20m. The dedicated "Lean proof typecheck" workflow has its
# own budget for the same step.
timeout-minutes: 60
env:
CARGO_TERM_COLOR: always
RUSTFLAGS: -D warnings
CARGO_INCREMENTAL: 0
steps:
- uses: actions/checkout@v4
- uses: dtolnay/rust-toolchain@stable
- uses: Swatinem/rust-cache@v2
- name: Install rivet
run: |
# Pin to rivet v0.7.0 (commit b7a17be) — the release that first ships
# `rivet list --filter <sexp>`, which this gate depends on. (The
# 4c06709 SHA I tried first is *etch*'s rev — etch is a sibling crate
# in the rivet workspace but unrelated to the CLI.)
# The rivet repo is a multi-package workspace; the trailing positional
# `rivet-cli` selects which crate owns the `rivet` binary, otherwise
# cargo errors with "multiple packages with binaries found:
# rivet-cli, rivet-fuzz".
cargo install --locked --git https://github.com/pulseengine/rivet \
--rev b7a17bef \
--bin rivet \
rivet-cli
- name: Pick verification filter (per-PR override via body)
id: pick
env:
PR_BODY: ${{ github.event.pull_request.body }}
run: |
# Default: every `type: feature` artifact whose status is currently
# `passing`. PRs may override by adding a single line to the body:
# Verify-Filter: (and (= type "feature") (has-tag "v093"))
# Default scope: current-milestone artifacts only (v0.9.x bug
# closeout + v0.10.x work). Running every `(= type "feature")`
# artifact would re-run ~124 cargo test invocations and blow the
# 30-minute job timeout. Per-PR override via `Verify-Filter:` line.
# rivet v0.7.0 supports: and/or/not/implies/excludes/=/!=/>/</has-tag/
# has-field/in/matches/contains/linked-* (no `has-status`).
DEFAULT='(and (= type "feature") (or (has-tag "v093") (has-tag "v0100")))'
OVERRIDE=$(printf '%s' "$PR_BODY" | grep -m1 -E '^Verify-Filter:' | sed 's/^Verify-Filter:[[:space:]]*//' || true)
if [ -n "${OVERRIDE:-}" ]; then
printf 'filter=%s\n' "$OVERRIDE" >>"$GITHUB_OUTPUT"
else
printf 'filter=%s\n' "$DEFAULT" >>"$GITHUB_OUTPUT"
fi
- name: Run rivet verification gate
id: verify
continue-on-error: true
env:
FILTER: ${{ steps.pick.outputs.filter }}
run: |
tools/run_verification.py \
--filter "$FILTER" \
--results-json verification-results.json
- name: Upload results artifact
if: always()
uses: actions/upload-artifact@v4
with:
name: verification-results
path: verification-results.json
if-no-files-found: warn
- name: Post sticky PR comment
if: github.event_name == 'pull_request' && always()
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
PR_NUMBER: ${{ github.event.pull_request.number }}
run: |
tools/post_verification_comment.py "$PR_NUMBER"
- name: Fail job if any verification artifact failed
if: steps.verify.outcome != 'success'
run: |
echo "::error::One or more verification artifacts failed; see PR comment for details"
exit 1