bmc4j/github-actions

Reusable GitHub Actions for the bmc4j project.

proof-report

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.

Inputs

input	default	description
summary-root	summaries	Directory holding the *.jsonl proof-summary records (searched recursively).
marker	<!-- bmc4j-proof-results -->	HTML-comment marker used to find/update the bot's PR comment. Override to adopt an existing comment thread.
github-token	${{ github.token }}	Token used to read/post the PR comment. Needs pull-requests: write to comment.
head-sha	''	Commit SHA shown (first 7 chars) in the report header.
run-url	''	CI run URL shown in the report footer.

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.

Usage — sharded consumer

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 }}

Usage — single-job consumer

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.