refactor: use create_justification in the quint specification as in the informal spec #1416
This file contains 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
| name: protobuf_compatibility | |
| on: | |
| pull_request: | |
| branches: ["*"] | |
| push: | |
| # protobuf compatibility is a transitive property, | |
| # but it requires all the transitions to be checked. | |
| # If we checked it just against the PR branches, | |
| # we may end up with conflicting PRs getting merged | |
| # (unless we improve our github setup). | |
| # Therefore on post-merge we will execute the | |
| # compatibility check as well (TODO: alerting). | |
| branches: ["main"] | |
| permissions: | |
| id-token: write | |
| contents: read | |
| env: | |
| CARGO_TERM_COLOR: always | |
| CARGO_INCREMENTAL: "0" | |
| RUSTFLAGS: "-C linker=clang -C link-arg=-fuse-ld=lld -C link-arg=-Wl,-z,nostart-stop-gc" | |
| RUSTC_WRAPPER: "sccache" | |
| SCCACHE_GHA_ENABLED: "true" | |
| RUST_BACKTRACE: "1" | |
| # github.base_ref -> github.head_ref for pull_request | |
| BASE: ${{ github.event.pull_request.base.sha || github.event.before }} | |
| # github.event.before -> github.event.after for push | |
| HEAD: ${{ github.event.pull_request.head.sha || github.event.after }} | |
| jobs: | |
| compatibility: | |
| runs-on: [ubuntu-22.04-github-hosted-16core] | |
| steps: | |
| - uses: mozilla-actions/[email protected] | |
| # before | |
| - uses: actions/checkout@v4 | |
| with: | |
| ref: ${{ env.BASE }} | |
| path: before | |
| fetch-depth: 0 # fetches all branches and tags, which is needed to compute the LCA. | |
| - name: checkout LCA | |
| run: git checkout $(git merge-base $BASE $HEAD) | |
| working-directory: ./before | |
| - name: compile before | |
| run: cargo build --all-targets | |
| working-directory: ./before/node | |
| - name: build before.binpb | |
| run: > | |
| perl -ne 'print "$1\n" if /PROTOBUF_DESCRIPTOR="(.*)"/' | |
| `find ./before/node/target/debug/build/*/output` | |
| | xargs cat > ./before.binpb | |
| # after | |
| - uses: actions/checkout@v4 | |
| with: | |
| ref: ${{ env.HEAD }} | |
| path: after | |
| - name: compile after | |
| run: cargo build --all-targets | |
| working-directory: ./after/node | |
| - name: build after.binpb | |
| run: > | |
| perl -ne 'print "$1\n" if /PROTOBUF_DESCRIPTOR="(.*)"/' | |
| `find ./after/node/target/debug/build/*/output` | |
| | xargs cat > ./after.binpb | |
| # compare | |
| - uses: bufbuild/buf-setup-action@v1 | |
| with: | |
| github_token: ${{ github.token }} | |
| - name: buf breaking | |
| run: buf breaking './after.binpb' --against './before.binpb' --config '{"version":"v1","breaking":{"use":["WIRE_JSON"]}}' --error-format 'github-actions' |