Add downstream-check CI (builds Strata against DDM PRs)#3
Draft
shigoel wants to merge 2 commits into
Draft
Conversation
Advisory, non-blocking check: builds Strata against this PR's StrataDDM code to catch breakage before it lands on main. Reuses the downstream-gate and rewrite-require composite actions from strata-org/Strata via @main. Depends on strata-org/Strata#1387 landing first (the composite actions must exist on Strata main before this workflow can resolve them).
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
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
2 participants
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 StrataDDM PR is ready (or a collaborator comments
!downstream-check), build Strata against this PR's StrataDDM code to catch breakage before it lands onmain. Result shows up as aDownstream / Stratajob on the PR.Builds Strata with its full toolchain (cvc5 + z3 + .NET + ion-java jar) and runs
lake test, matching Strata's own CI, so a green check means the same thing.Mechanism
Checks out the PR's StrataDDM, clones Strata, rewrites Strata's
require "StrataDDM"to a local path (fork-safe), thenlake update StrataDDM+ build + test. Reuses thedownstream-gateandrewrite-requirecomposite actions fromstrata-org/Stratavia@main.Transitive breakage (DDM → Strata → Boole/Python/CLI) is intentionally not chased here — that's caught when the DDM rev is bumped in a Strata PR, which fires Strata's own check.
Depends on
mainuntil that PR merges. Until then this check will error (expected). Part of the same cross-repo rollout; see #1387 for the full design.Draft for early feedback.