Mark trivial set_option backward.* files as viewed in a GitHub PR

mark-set-option-viewed.sh

#!/usr/bin/env bash
# Mark as "viewed" any file in a PR whose diff only adds/removes
# "set_option backward.isDefEq.respectTransparency false in" or
# "set_option backward.whnf.reducibleClassField false in".
# Usage: ./mark-set-option-viewed.sh [owner/repo] [pr-number]
# Requires: gh (GitHub CLI), python3

REPO="${1:-leanprover-community/mathlib4-nightly-testing}"
PR="${2:-201}"

# Get the PR's GraphQL node ID
PR_ID=$(gh api graphql -f query="
  query {
    repository(owner: \"${REPO%/*}\", name: \"${REPO#*/}\") {
      pullRequest(number: $PR) { id }
    }
  }" --jq '.data.repository.pullRequest.id')

echo "PR node ID: $PR_ID"

# Get all changed files with patches, then filter to trivial set_option-only changes
TMPFILE=$(mktemp)
gh api "repos/$REPO/pulls/$PR/files" --paginate --jq '.[] | @json' | python3 -c "
import sys, json

TRIVIAL_LINES = {
    'set_option backward.isDefEq.respectTransparency false in',
    'set_option backward.whnf.reducibleClassField false in',
}

for line in sys.stdin:
    line = line.strip()
    if not line:
        continue
    obj = json.loads(line)
    patch = obj.get('patch', '')
    trivial = True
    for pl in patch.split('\n'):
        if pl.startswith('@@'):
            continue
        if pl.startswith('+') or pl.startswith('-'):
            content = pl[1:].strip()
            if content == '' or content in TRIVIAL_LINES:
                continue
            trivial = False
            break
    if trivial:
        print(obj['filename'])
" > "$TMPFILE"

COUNT=$(wc -l < "$TMPFILE" | tr -d ' ')
echo "Marking $COUNT files as viewed..."

while IFS= read -r path; do
  gh api graphql -f query="mutation { markFileAsViewed(input: { pullRequestId: \"$PR_ID\", path: \"$path\" }) { pullRequest { id } } }" > /dev/null
  echo "  ✓ $path"
done < "$TMPFILE"

rm -f "$TMPFILE"
echo "Done."