Add downstream-check CI (builds Strata-CLI against Python PRs) #1
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 Strata-CLI against this PR's Strata-Python code, so | |
| # we catch breakage before it lands on main. Advisory only — visible on the PR | |
| # but does not gate merge. | |
| # | |
| # Mechanism: check out the PR's Strata-Python, clone Strata-CLI, rewrite | |
| # Strata-CLI's `require "StrataPython"` 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 StrataPython` + build + test. CLI's | |
| # other requires (Strata, StrataDDM at rev = "main") resolve from their remotes | |
| # as usual — only the StrataPython edge is overridden. | |
| # | |
| # Trigger: non-draft PRs only (ready_for_review + every push via synchronize). | |
| name: Downstream check | |
| on: | |
| pull_request: | |
| types: [ready_for_review, synchronize] | |
| concurrency: | |
| group: downstream-${{ github.event.pull_request.number }} | |
| cancel-in-progress: true | |
| permissions: | |
| contents: read | |
| jobs: | |
| downstream: | |
| if: ${{ !github.event.pull_request.draft }} | |
| runs-on: ubuntu-latest | |
| name: Strata-CLI | |
| steps: | |
| - name: Check out PR's Strata-Python | |
| uses: actions/checkout@v6 | |
| with: | |
| ref: ${{ github.event.pull_request.head.sha }} | |
| path: upstream | |
| - name: Clone Strata-CLI | |
| run: git clone --depth 1 https://github.com/strata-org/Strata-CLI.git downstream | |
| - name: Override StrataPython require -> local PR checkout | |
| uses: strata-org/Strata/.github/actions/rewrite-require@main | |
| with: | |
| lakefile: downstream/lakefile.toml | |
| package: StrataPython | |
| path: ../upstream | |
| # Strata-CLI links the full toolchain (cvc5 + z3), same as its own CI. | |
| - name: Install cvc5 | |
| uses: strata-org/Strata/.github/actions/install-cvc5@main | |
| - name: Install z3 | |
| uses: strata-org/Strata/.github/actions/install-z3@main | |
| - name: Restore lake cache | |
| uses: actions/cache/restore@v5 | |
| with: | |
| path: | | |
| downstream/.lake | |
| key: downstream-Strata-CLI-${{ runner.os }}-${{ github.event.pull_request.head.sha }} | |
| restore-keys: | | |
| downstream-Strata-CLI-${{ runner.os }}- | |
| - name: lake update StrataPython | |
| working-directory: downstream | |
| run: lake update StrataPython | |
| # Strata-CLI has no lake testDriver; its own CI builds, then exercises the | |
| # binary + examples. Mirror that so a green check means the same thing. | |
| - name: Build Strata-CLI | |
| uses: leanprover/lean-action@v1 | |
| with: | |
| lake-package-directory: downstream | |
| use-github-cache: false | |
| test: false | |
| - name: Run `strata` CLI | |
| working-directory: downstream | |
| run: lake exe strata --help | |
| - name: Validate examples against expected output | |
| working-directory: downstream | |
| run: ./scripts/run_examples.sh | |
| - name: Save lake cache | |
| if: always() | |
| uses: actions/cache/save@v5 | |
| with: | |
| path: | | |
| downstream/.lake | |
| key: downstream-Strata-CLI-${{ runner.os }}-${{ github.event.pull_request.head.sha }} |