Skip to main content

check-proof-statements.yml

Diff-scoped, warn-only check for two of the lab’s proof rules (psw#426, gha#1351).

Rules

  • Proof hidden from slides. A proof div inside ::: {.content-hidden when-format="revealjs"} (or .content-visible unless-format="revealjs"), or an include of a _prf- or _proof- subfile there, is flagged on the proof’s opening line. Every proof is shown on slides. The finding is reported when the pull request adds any line to the file, not only the proof’s own lines.
  • Reasoning in a theorem statement. “so”, “because”, “hence”, “therefore”, “thus” or “since”, or an aside such as “without loss of generality”, “moreover” or “furthermore”, on an added line inside a #thm-, #lem-, #cor- or #prp- div, outside the proof the div holds. A statement gives the result and its hypotheses; the proof gives the reasoning. Heuristic: “so that” and “so-called” pass, and words inside math are not read.

The check does not read a code fence or code span, an HTML comment, YAML front matter, or a line carrying, or following, <!-- check-proof-statements: allow -->.

Scope

There is no sweep: a file the pull request does not change is never reported, and the statement rule reports only lines the pull request adds. An added line whose exact text was also deleted in the same diff counts as moved rather than new.

With no base-ref, or when the diff cannot be computed (a shallow clone, an unresolvable ref), the check skips with a warning. It never falls back to a whole-tree scan. Set whole-tree: true to scan every tracked file in full on purpose.

Every run prints how many lines and files it examined.

Inputs

Input Type Default Description
globs string '*.qmd *.md' Space-separated git pathspecs of tracked files to check (recursive by default).
paths-ignore string '' Comma- or newline-separated glob patterns (relative paths) to skip. Supports *, ? and recursive **.
fail boolean false Fail the workflow when a hidden proof or statement reasoning is found. Warn-only by default.
whole-tree boolean false Scan every tracked file in full instead of only a PR’s added lines.
python-version string '3.x' Python version to set up.
runs-on string empty (CI_RUNNER variable, else ubuntu-latest) Runner label for the job. Use a self-hosted label only for a private repository; never for a public one, whose pull requests can run arbitrary code on it (#1167).

Permissions

Only contents: read (the default), so no permissions: block is needed.

Example

# Copy to .github/workflows/check-proof-statements.yml in your repo.
name: Check proof statements

on:
  push:
    branches:
      - main
  pull_request:
  workflow_dispatch:

jobs:
  check:
    uses: Morrison-Lab/gha/.github/workflows/check-proof-statements.yml@v3
    # with:
    #   globs: '*.qmd *.md'                     # pathspecs to check (recursive)
    #   paths-ignore: 'chapters/outtakes/**'    # skip known-noisy paths
    #   fail: true                              # block instead of warn (defaults to false)
    #   whole-tree: true                        # scan every line, not just a PR's additions
    #   runs-on: private-runner                # self-hosted runner label (private repositories only)

See examples/check-proof-statements.yml for the full caller stub.