ROADMAP.md is out of date (unchanged since June 2025) #916
This file contains hidden or 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: PR Review | |
| # Trusted CHATOPS-ONLY deployment of the consolidated OpenRouter review action | |
| # (lean4repo-utils/review@0.3). Invoked by a maintainer commenting `/review` on a PR. | |
| # The auto pull_request trigger is intentionally dropped for now. | |
| on: | |
| issue_comment: | |
| types: [created] | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.event.issue.number }} | |
| cancel-in-progress: false | |
| # Least privilege: the reviewer's lean_tools execute model-directed Lean IO and the | |
| # action builds the PR-head code, so a token exfiltrated there must not be able to push | |
| # or merge. Only what posting a review needs. | |
| permissions: | |
| contents: read | |
| pull-requests: write | |
| issues: write | |
| jobs: | |
| review: | |
| # Chatops only, gated to trusted members. NOTE: `/review` here is a coarse prefix | |
| # match — a member typing `/reviewer` would also match; harmless under the member | |
| # gate, tighten to a word boundary if this ever opens to untrusted commenters. | |
| if: >- | |
| github.event.issue.pull_request && | |
| startsWith(github.event.comment.body, '/review') && | |
| ( | |
| github.event.comment.author_association == 'OWNER' || | |
| github.event.comment.author_association == 'MEMBER' || | |
| github.event.comment.author_association == 'COLLABORATOR' | |
| ) | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 240 | |
| steps: | |
| # Parse the /review comment: `Internal:` lines → manual spec/KB refs, everything | |
| # under `External:`/`Comments:` → free-text instructions (the action auto-extracts | |
| # any URLs it mentions). Comment body is passed via env, never interpolated into | |
| # the run: body (GHA expression-injection guard). | |
| - name: Extract arguments from comment | |
| id: get_args | |
| env: | |
| COMMENT_BODY: ${{ github.event.comment.body }} | |
| shell: bash | |
| run: | | |
| EOF=$(openssl rand -hex 8) | |
| awk -v eof="$EOF" -v gh_out="$GITHUB_OUTPUT" ' | |
| BEGIN { spec=""; com=""; section="" } | |
| /^External:/ { section="com"; next } | |
| /^Internal:/ { section="spec"; next } | |
| /^Comments:/ { section="com"; next } | |
| { | |
| gsub(/\r/, "", $0); gsub(/^[ \t]+|[ \t]+$/, "", $0); | |
| if ($0 == "" || $0 == "/review") { next } | |
| if (section == "spec") { sub(/^- +/, ""); spec = (spec=="" ? $0 : spec "," $0) } | |
| else if (section == "com") { com = (com=="" ? $0 : com "\n" $0) } | |
| } | |
| END { | |
| printf "manual_spec_refs=%s\n", spec >> gh_out | |
| printf "additional_comments<<%s\n%s\n%s\n", eof, com, eof >> gh_out | |
| } | |
| ' <<< "$COMMENT_BODY" | |
| # Unguided KB grounding: map the PR''s changed .lean files to the papers they cite | |
| # (docs/kb/_generated/lean-citations.json) and pass those KB pages as spec_refs, so | |
| # a plain /review is grounded in the right paper summaries with no manual guidance. | |
| # Read the citation JOIN from the BASE ref (data-only, fork-safe); do NOT execute | |
| # any checked-out repo script. (The KB page CONTENT is read by the action from the | |
| # PR head — acceptable for this trusted, manually-inspected pilot; base-ref content | |
| # reading is part of the S2/S7 hardening.) | |
| - name: Resolve KB context (base-ref citation join) | |
| id: kb | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| PR_NUMBER: ${{ github.event.issue.number }} | |
| MANUAL_SPEC_REFS: ${{ steps.get_args.outputs.manual_spec_refs }} | |
| shell: bash | |
| run: | | |
| set -euo pipefail | |
| BASE_SHA="$(gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER" --jq '.base.sha')" | |
| gh api "repos/$GITHUB_REPOSITORY/pulls/$PR_NUMBER/files" --paginate --jq '.[].filename' > /tmp/changed.txt | |
| if gh api "repos/$GITHUB_REPOSITORY/contents/docs/kb/_generated/lean-citations.json?ref=$BASE_SHA" \ | |
| --jq '.content' 2>/dev/null | base64 -d > /tmp/citations.json; then :; else | |
| echo "No lean-citations.json on base ref; proceeding without KB spec_refs." | |
| echo '{}' > /tmp/citations.json | |
| fi | |
| # Join is pure data: filenames + JSON read from files, never interpolated. | |
| spec_refs="$(python3 - <<'PY' | |
| import json, os | |
| try: | |
| cites = json.load(open('/tmp/citations.json')).get('files', {}) | |
| except Exception: | |
| cites = {} | |
| changed = [l.strip() for l in open('/tmp/changed.txt') if l.strip().endswith('.lean')] | |
| keys = [] | |
| for f in changed: | |
| for k in cites.get(f, []): | |
| if k not in keys: | |
| keys.append(k) | |
| refs = [f"docs/kb/papers/{k}.md" for k in keys] | |
| # Merge any manual `Internal:` refs from the /review comment (dedup, keep order). | |
| for r in (os.environ.get("MANUAL_SPEC_REFS", "") or "").split(","): | |
| r = r.strip() | |
| if r and r not in refs: | |
| refs.append(r) | |
| print(",".join(refs)) | |
| PY | |
| )" | |
| echo "spec_refs=$spec_refs" >> "$GITHUB_OUTPUT" | |
| echo "Resolved KB spec_refs: ${spec_refs:-(none)}" | |
| - name: AI review | |
| uses: alexanderlhicks/lean4repo-utils/review@0.3 | |
| with: | |
| github_token: ${{ secrets.GITHUB_TOKEN }} | |
| api_key: ${{ secrets.OPENROUTER_KEY }} | |
| pr_number: ${{ github.event.issue.number }} | |
| # Auto-pulled KB paper pages for the changed files + any manual Internal: refs. | |
| spec_refs: ${{ steps.kb.outputs.spec_refs }} | |
| additional_comments: ${{ steps.get_args.outputs.additional_comments }} | |
| # Coverage-first budget control: this sizes/trims prompts for large PRs, | |
| # but advisory mode does not stop later files from being reviewed. | |
| # Source these from workflow config, never PR content. | |
| # llm_max_run_tokens: "400000" | |
| # llm_budget_mode: advisory | |
| # model: omitted → the action's default OpenRouter slug. Set an explicit slug | |
| # here if you want a specific model for the pilot. | |
| # lean_tools defaults true (full-quality, compiler-grounded review — trusted | |
| # pilot). enable_web_search defaults false (web-search fees are not token-bounded). |