Skip to content

Add downstream-check CI (builds Strata-Boogie against CLI PRs)#6

Draft
shigoel wants to merge 2 commits into
mainfrom
add-downstream-check
Draft

Add downstream-check CI (builds Strata-Boogie against CLI PRs)#6
shigoel wants to merge 2 commits into
mainfrom
add-downstream-check

Conversation

@shigoel

@shigoel shigoel commented Jun 18, 2026

Copy link
Copy Markdown
Contributor

What

Advisory, non-blocking cross-repo check: when a Strata-CLI PR is ready (or a collaborator comments !downstream-check), build Strata-Boogie against this PR's Strata-CLI code to catch breakage before it lands on main. Result shows up as a Downstream / Strata-Boogie job on the PR.

Strata-Boogie is a .NET/C# project, not a Lake package — it doesn't require Strata-CLI in a lakefile. So this check mirrors Boogie's own ci.yml: build the strata binary from the PR's Strata-CLI, then run dotnet test against it via STRATA_VERIFIER_PATH. No lakefile rewrite needed.

Mechanism

Checks out the PR's Strata-CLI, clones Strata-Boogie, builds the strata binary from the PR checkout, then dotnet restore/build/test the Boogie integration tests. Reuses Strata's downstream-gate composite action via @main (no rewrite-require here — not a Lake dependency).

Depends on

⚠️ strata-org/Strata#1387 must land first (the composite actions must exist on Strata main). Until then this check will error (expected). See #1387 for the full design.

Draft for early feedback.

Advisory, non-blocking check: builds Strata-Boogie (a .NET project) against
this PR's Strata-CLI code by building the strata binary and running dotnet
test against it via STRATA_VERIFIER_PATH, mirroring Boogie's own ci.yml.
Reuses Strata's downstream-gate composite action via @main.

Depends on strata-org/Strata#1387 landing first.
Comment thread .github/workflows/downstream-check.yml Fixed
The issue_comment trigger runs in the privileged default-branch context;
building untrusted PR code there is a cache-poisoning / code-execution vector
(CodeQL actions/cache-poisoning/poisonable-step). Run only on pull_request,
which builds the same code in an isolated, unprivileged context.

Collapses the gate job into a job-level draft check and reads the PR head SHA
from the event payload (no shared gate action needed).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants