Reusable GitHub Actions for the bmc4j project.

A composite action that aggregates bmc4j proof-summary JSONL records into a results table and posts it as a single marker comment on a pull request — or, on a non-PR event (push to a branch, merge group, dispatch), writes the same table to the run's job-summary page.

It renders a metrics table (proofs ran / expected shard-union / checked / cache hits / live solves / failed), a Failures table with separate why it fails (the ✗ <reason> line) and counterexample columns, lost-shard detection, and an UNKNOWN-kind flake tally.

The job needs permissions: { contents: read, pull-requests: write }. On a forked PR (read-only token) the comment 403 is swallowed and the table still lands on the job-summary page.

Each proof leg uploads a proof-summary-<leg>-<i>-of-<n> artifact; download them all into a dir, then point summary-root at it. The artifact dir names let the renderer recover leg + shard id and detect lost shards.

report:
 needs: [proofs]
 if: ${{ always() }}
 runs-on: ubuntu-latest
 permissions:
 contents: read
 pull-requests: write
 steps:
 - uses: actions/download-artifact@v6
 with:
 path: summaries
 pattern: proof-summary-*
 - uses: bmc4j/github-actions/proof-report@v1
 with:
 summary-root: summaries
 head-sha: ${{ github.event_name == 'pull_request' && github.event.pull_request.head.sha || github.sha }}
 run-url: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}

Run gradle with -Dbmc.summaryDir=<dir> so each proof writes its JSONL there, then point summary-root at that same dir. The renderer's legOfPath falls back to a single proofs leg for the non-artifact directory naming.

prove:
 runs-on: ubuntu-latest
 permissions:
 contents: read
 pull-requests: write
 steps:
 - uses: actions/checkout@v6
 - uses: actions/setup-java@v5
 with: { distribution: temurin, java-version: '21' }
 - uses: gradle/actions/setup-gradle@v4
 - name: Run proofs
 run: ./gradlew test --console=plain -Dbmc.summaryDir="$GITHUB_WORKSPACE/proof-summary"
 - name: Report proof results
 if: ${{ always() }}
 uses: bmc4j/github-actions/proof-report@v1
 with:
 summary-root: proof-summary
 marker: '<!-- bmc4j-proof-report -->'

Pin to the @v1 tag (it tracks the latest v1.x); never use @main.