Add downstream-check CI (builds Strata-Boogie against CLI PRs)#6
Draft
shigoel wants to merge 2 commits into
Draft
Add downstream-check CI (builds Strata-Boogie against CLI PRs)#6shigoel wants to merge 2 commits into
shigoel wants to merge 2 commits into
Conversation
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.
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).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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 onmain. Result shows up as aDownstream / Strata-Boogiejob on the PR.Strata-Boogie is a .NET/C# project, not a Lake package — it doesn't
requireStrata-CLI in a lakefile. So this check mirrors Boogie's ownci.yml: build thestratabinary from the PR's Strata-CLI, then rundotnet testagainst it viaSTRATA_VERIFIER_PATH. No lakefile rewrite needed.Mechanism
Checks out the PR's Strata-CLI, clones Strata-Boogie, builds the
stratabinary from the PR checkout, thendotnet restore/build/testthe Boogie integration tests. Reuses Strata'sdownstream-gatecomposite action via@main(norewrite-requirehere — not a Lake dependency).Depends on
main). Until then this check will error (expected). See #1387 for the full design.Draft for early feedback.