Add downstream-check CI and shared composite actions#1387
Open
shigoel wants to merge 6 commits into
Open
Conversation
Adds an advisory downstream-check workflow that builds each repo depending on Strata (Strata-Boole, Strata-Python, Strata-CLI) against a PR's code, catching cross-repo breakage before it lands on main. Results show up as per-downstream jobs on the PR; non-blocking. Also adds two composite actions reused by the downstream-check workflows in Strata-DDM, Strata-Python, and Strata-CLI (referenced cross-repo via @main): - downstream-gate: shared trigger/auth gate (non-draft PRs + collaborator !downstream-check comment), resolves the PR head SHA. - rewrite-require: fork-safe lakefile override (rewrites a require to a local path so the downstream builds against the PR checkout). The build recipe per downstream is currently inlined here. Next step (if the team is aligned): extract each downstream's build+test core into a composite action owned by that downstream repo, so its own ci.yml and this check share one source of truth and can't drift.
shigoel
added a commit
to strata-org/Strata-DDM
that referenced
this pull request
Jun 18, 2026
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).
shigoel
added a commit
to strata-org/Strata-Python
that referenced
this pull request
Jun 18, 2026
Advisory, non-blocking check: builds Strata-CLI against this PR's Strata-Python code (CLI requires StrataPython) to catch breakage before it lands on main. CLI has no lake testDriver, so it verifies via the binary + examples, mirroring CLI's own ci.yml. Reuses Strata's composite actions via @main. Depends on strata-org/Strata#1387 landing first.
github-actions
Bot
added
the
github_actions
shigoel
added a commit
to strata-org/Strata-CLI
that referenced
this pull request
Jun 18, 2026
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.
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
This was referenced Jun 18, 2026
The issue_comment (!downstream-check) path runs in the privileged default-branch context. Saving a cache after checking out untrusted PR code there could poison the base-branch cache scope that trusted runs restore from. Gate the cache save on github.event_name == 'pull_request' (isolated scope); the comment path is now restore-only.
The gate job uses the local ./.github/actions/downstream-gate composite
action but had no actions/checkout, so the action files weren't on disk
("Can't find action.yml"). Add a sparse checkout of .github. The gate only
reads the event payload, so no repo source is needed.
The issue_comment (!downstream-check) 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), and step-gating can't fix it. Drop the trigger and 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 (no local action to check out), reads the PR head SHA from the event payload, and uses python3 (not python) in rewrite-require for GitHub-runner portability.
No longer referenced after dropping the issue_comment trigger — the gate collapsed into a job-level draft check reading the PR head SHA from the event payload, so the shared gate action has no callers.
lake update ran before leanprover/lean-action (which provisions elan/lake), so lake wasn't on PATH yet (command not found, exit 127). Add an early lean-action step with auto-config: false — elan installs unconditionally, build/test are skipped — so the toolchain is ready before lake update.
robin-aws
reviewed
Jun 18, 2026
Contributor
There was a problem hiding this comment.
Definitely don't love this approach since a) it's potentially-brittle grepping through config files, and b) it would need to be expanded to support lakefile.lean files as well.
Here are two alternatives (which I should have thought of earlier!)
- Generate a package overrides file to point references to the package to the local path.
- Create a local reservoir-style image of the modified package as if it was deployed there, and set the
RESERVOIR_API_URLenvironment variable tofile:///...
1 is probably the way to go. I mention 2 for completeness (and because I think we can use it for other purposes).
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
3 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.
Advisory cross-repo CI: when a Strata PR is marked ready for review (and on every subsequent push), build each repo that depends on Strata — Strata-Boole, Strata-Python, Strata-CLI — against the PR's code, so we catch breakage before it lands on
main. Results appear as per-downstream jobs on the PR (Downstream / Strata-Boole, …). Non-blocking — advisory signal, not a merge gate.How it works
For each downstream, one matrix job:
require "Strata"to a localpathpointing at the PR checkout (via therewrite-requirecomposite action). This is fork-safe — it builds the PR's actual code without needing the head SHA to be fetchable from the remote, so it works for fork PRs too.lake update Strata+ build + test (Boole/Python run theirlake testsuites; CLI has no test driver, so it mirrors its own CI: build, thenlake exe strata --help+run_examples.sh).Runs only on
pull_requestfor non-draft PRs. Building PR code happens in GitHub's isolated, unprivilegedpull_requestcontext (read-only token, PR-scoped cache), which is the safe way to execute untrusted contributions.This PR also adds the
rewrite-requirecomposite action (+scripts/rewrite_require.py), reused by the sibling downstream-check workflows in the other upstream repos.Dependency graph
This PR covers the Strata → edges. Sibling PRs add the checks for the other upstream repos (Strata-DDM builds Strata; Strata-Python builds Strata-CLI; Strata-CLI builds Strata-Boogie). They reference the composite action added here, so this PR should land first.
Strata-Boole and Strata-Boogie get no workflow — they're leaves (nothing depends on them).
Known follow-ups (feedback welcome)
ci.ymland this check share one source of truth and can't drift. Holding off pending alignment on this approach — thoughts welcome.rev = "main". Pinning + an automated bump PR would make the advisory-only model fully honest. Deferred.Draft for early feedback.