Add downstream-check CI and shared composite actions #4
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
| # Copyright Strata Contributors | |
| # SPDX-License-Identifier: Apache-2.0 OR MIT | |
| # | |
| # Downstream check: builds each repo that depends on Strata against this PR's | |
| # code, so we catch breakage before it lands on main. Advisory only — these | |
| # checks are visible on the PR but do not gate merge. | |
| # | |
| # Mechanism: check out the PR's Strata, clone each downstream, rewrite the | |
| # downstream's `require "Strata"` to a local path pointing at the checked-out | |
| # PR code (fork-safe: no need for the PR head SHA to exist on the strata-org | |
| # remote), then `lake update Strata` + build + test. | |
| # | |
| # Trigger: non-draft PRs only (ready_for_review + every push via synchronize). | |
| # We deliberately do NOT support an issue_comment (`!downstream-check`) trigger: | |
| # that runs in the privileged default-branch context, and building untrusted PR | |
| # code there is a cache-poisoning / code-execution vector (CodeQL | |
| # actions/cache-poisoning/poisonable-step). pull_request runs the same build in | |
| # an isolated, unprivileged context, which is safe. If on-demand checks are | |
| # wanted later, add them via label-indirection (a privileged workflow turns a | |
| # comment into a label; `pull_request: types: [labeled]` does the build | |
| # unprivileged) — never by reintroducing issue_comment here. | |
| name: Downstream check | |
| on: | |
| pull_request: | |
| types: [ready_for_review, synchronize] | |
| # One in-flight run per PR; a new push cancels the previous downstream check. | |
| concurrency: | |
| group: downstream-${{ github.event.pull_request.number }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| jobs: | |
| downstream: | |
| # Non-draft PRs only. (The `types` filter already restricts to | |
| # ready_for_review/synchronize.) | |
| if: ${{ !github.event.pull_request.draft }} | |
| runs-on: ubuntu-latest | |
| strategy: | |
| # Don't let one broken downstream hide the status of the others. | |
| fail-fast: false | |
| matrix: | |
| include: | |
| # Boole and Python define a lake testDriver, so `test: true` builds | |
| # and runs their suites. | |
| - repo: Strata-Boole | |
| test: true | |
| - repo: Strata-Python | |
| test: true | |
| # Strata-CLI has no testDriver; mirror its own CI — build, then | |
| # exercise the binary + examples via post_build (run below). | |
| - repo: Strata-CLI | |
| test: false | |
| post_build: | | |
| lake exe strata --help | |
| ./scripts/run_examples.sh | |
| # The job name is what reviewers see in the PR's Checks tab: | |
| # "Downstream / Strata-Boole", etc. | |
| name: ${{ matrix.repo }} | |
| steps: | |
| - name: Check out PR's Strata | |
| uses: actions/checkout@v6 | |
| with: | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| path: upstream | |
| - name: Clone downstream (${{ matrix.repo }}) | |
| run: git clone --depth 1 https://github.com/strata-org/${{ matrix.repo }}.git downstream | |
| - name: Override Strata require -> local PR checkout | |
| uses: ./upstream/.github/actions/rewrite-require | |
| with: | |
| lakefile: downstream/lakefile.toml | |
| package: Strata | |
| path: ../upstream | |
| - name: Install cvc5 | |
| uses: ./upstream/.github/actions/install-cvc5 | |
| - name: Install z3 | |
| uses: ./upstream/.github/actions/install-z3 | |
| # Cache keyed on upstream head SHA + downstream repo. The restore-keys | |
| # fallback lets a new push reuse the previous build for this PR; lake | |
| # rebuilds the modules whose (overridden, local) Strata source changed. | |
| # Trades a small stale-result risk for ~15-30 min, matching Strata CI's | |
| # PR caching posture. This is advisory CI, so the trade is acceptable. | |
| - name: Restore lake cache | |
| uses: actions/cache/restore@v5 | |
| with: | |
| path: | | |
| downstream/.lake | |
| key: downstream-${{ matrix.repo }}-${{ runner.os }}-${{ github.event.pull_request.head.sha }} | |
| restore-keys: | | |
| downstream-${{ matrix.repo }}-${{ runner.os }}- | |
| - name: lake update Strata | |
| working-directory: downstream | |
| run: lake update Strata | |
| - name: Build downstream | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: downstream | |
| use-github-cache: false | |
| test: ${{ matrix.test }} | |
| # Repos without a lake testDriver verify via their own post-build steps. | |
| - name: Post-build checks (${{ matrix.repo }}) | |
| if: matrix.post_build != '' | |
| working-directory: downstream | |
| run: ${{ matrix.post_build }} | |
| - name: Save lake cache | |
| if: always() | |
| uses: actions/cache/save@v5 | |
| with: | |
| path: | | |
| downstream/.lake | |
| key: downstream-${{ matrix.repo }}-${{ runner.os }}-${{ github.event.pull_request.head.sha }} |