diff --git a/.github/workflows/lean_action_ci.yml b/.github/workflows/lean_action_ci.yml index 28aefa7633..849849f809 100644 --- a/.github/workflows/lean_action_ci.yml +++ b/.github/workflows/lean_action_ci.yml @@ -42,8 +42,6 @@ permissions: contents: read pages: write id-token: write - # Needed by proof-profile to post a sticky comment on the PR. - pull-requests: write jobs: build: @@ -124,212 +122,3 @@ jobs: .lake/packages .lake/build key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - - proof-profile: - runs-on: ubuntu-latest - name: Proof profile (advisory) - continue-on-error: true - steps: - - name: Checkout project - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd - with: - fetch-depth: 0 - - - name: Restore caches - uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae - with: - path: | - ~/.elan - .lake/packages - .lake/build - key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }} - restore-keys: | - Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- - - - name: Install Lean - uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 - with: - auto-config: false - use-github-cache: false - use-mathlib-cache: false - - - name: Install Mathlib cache - run: | - if [ ! -d ".lake/packages/mathlib" ]; then - ~/.elan/bin/lake exe cache get - else - echo "Mathlib already present from cache" - fi - - - name: Determine new and modified Lean files - id: files - run: | - set -euo pipefail - base="${{ github.event.pull_request.base.sha }}" - if [ -z "$base" ]; then - # push to main, or workflow_dispatch — compare against previous commit - base="HEAD~1" - fi - files=$(git diff --name-only --diff-filter=AM "$base"...HEAD -- LeanPool \ - | grep '\.lean$' \ - | tr '\n' ' ' || true) - echo "files=$files" >> "$GITHUB_OUTPUT" - if [ -z "$files" ]; then - echo "No new or modified Lean files in this diff; profile job will no-op." - else - echo "Will profile: $files" - fi - - - name: Build project so profile imports resolve - if: steps.files.outputs.files != '' - run: ~/.elan/bin/lake build LeanPool - - - name: Profile new and modified files - if: steps.files.outputs.files != '' - run: | - : > proof-profile.log - for file in ${{ steps.files.outputs.files }}; do - { - echo "## $file" - # Errors here are logged but never fail the job — this is advisory. - ~/.elan/bin/lake env lean --profile "$file" || true - echo - } >> proof-profile.log 2>&1 - done - - - name: Render profile summary - if: steps.files.outputs.files != '' - run: | - python3 <<'PY' - import os - import re - from pathlib import Path - - log_path = Path("proof-profile.log") - rendered_path = Path("proof-profile.md") - summary_path = Path(os.environ["GITHUB_STEP_SUMMARY"]) - run_url = ( - f"{os.environ['GITHUB_SERVER_URL']}/{os.environ['GITHUB_REPOSITORY']}" - f"/actions/runs/{os.environ['GITHUB_RUN_ID']}" - ) - - # Lean's `cumulative profiling times:` block is one indented - # ` ms` per line. The phase name can contain - # spaces, parens, and hyphens (`compilation (IR)`, - # `let-to-have transformation`, ...). Lean only emits a phase if - # it accumulated nonzero time, so the set of phases differs per - # file and per run; the renderer captures every phase rather than - # cherry-picking known names. - metric_re = re.compile( - r"^[ \t]+(.+?)\s+([0-9]+(?:\.[0-9]+)?)\s*ms\s*$" - ) - - out = ["## Proof profile (new / modified Lean files)\n\n"] - log_text = log_path.read_text() if log_path.exists() else "" - if not log_text.strip(): - out.append("_No proof profile output._\n") - rendered_path.write_text("".join(out)) - summary_path.write_text("".join(out)) - raise SystemExit(0) - - # Split the log into one section per profiled file (delimited by - # `## ` markers written by the profile loop). - sections: list[tuple[str, str]] = [] - name = None - buf: list[str] = [] - for line in log_text.splitlines(): - header = re.match(r"^## (.+)$", line) - if header: - if name is not None: - sections.append((name, "\n".join(buf).rstrip())) - name = header.group(1) - buf = [] - elif name is not None: - buf.append(line) - if name is not None: - sections.append((name, "\n".join(buf).rstrip())) - - if not sections: - out.append("_No files profiled._\n") - else: - # Summary table: cumulative ms = sum over reported phases. - summary_rows = [] - for fname, body in sections: - total = 0.0 - phases = 0 - errors = 0 - for line in body.splitlines(): - if "error:" in line: - errors += 1 - continue - m = metric_re.match(line) - if m: - total += float(m.group(2)) - phases += 1 - summary_rows.append((fname, total, phases, errors)) - summary_rows.sort(key=lambda r: -r[1]) - out.append("| File | Cumulative (ms) | Phases | Errors |\n") - out.append("|---|---:|---:|---:|\n") - for fname, total, phases, errors in summary_rows: - out.append( - f"| `{fname}` | {total:.1f} | {phases} | {errors} |\n" - ) - out.append("\n") - - # Full per-file output, collapsed by default so the comment - # stays scannable when many files are profiled. - out.append("
Per-file profile output\n\n") - for fname, body in sections: - out.append(f"#### `{fname}`\n\n") - out.append("```text\n") - out.append(body if body.strip() else "(empty)") - out.append("\n```\n\n") - out.append("
\n") - - out.append( - "\n_Advisory only — never blocks merge. " - f"[Full log]({run_url}) uploaded as the `proof-profile` " - "artifact._\n" - ) - - rendered = "".join(out) - rendered_path.write_text(rendered) - with summary_path.open("a") as f: - f.write(rendered) - PY - - - name: Post sticky PR comment with profile - if: | - github.event_name == 'pull_request' && - steps.files.outputs.files != '' - env: - GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} - PR_NUMBER: ${{ github.event.pull_request.number }} - REPO: ${{ github.repository }} - run: | - set -euo pipefail - # Marker so we can find and update the same comment on subsequent - # runs instead of stacking new ones. - marker="" - { - printf '%s\n' "$marker" - cat proof-profile.md - } > comment-body.md - - existing=$(gh api "repos/$REPO/issues/$PR_NUMBER/comments" --paginate \ - --jq "[.[] | select(.body | startswith(\"$marker\"))] | first | .id // empty") - - if [ -n "$existing" ]; then - jq -n --rawfile body comment-body.md '{body: $body}' \ - | gh api -X PATCH "repos/$REPO/issues/comments/$existing" --input - - else - gh pr comment "$PR_NUMBER" --body-file comment-body.md - fi - - - name: Upload proof profile - if: always() && steps.files.outputs.files != '' - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 - with: - name: proof-profile - path: proof-profile.log - if-no-files-found: ignore diff --git a/.github/workflows/proof-profile.yml b/.github/workflows/proof-profile.yml new file mode 100644 index 0000000000..b40628e3c2 --- /dev/null +++ b/.github/workflows/proof-profile.yml @@ -0,0 +1,275 @@ +name: Proof Profile + +# Same triggering model as LLM Review: profile once when a PR is opened, and +# again on demand when someone comments `/profile` on the PR. No `synchronize` +# trigger — the profile is advisory, so re-run it by hand after a push if you +# want a fresh one. workflow_dispatch takes an explicit PR number. +on: + pull_request: + types: [opened] + issue_comment: + types: [created] + workflow_dispatch: + inputs: + pr_number: + description: "PR number to profile" + required: true + type: string + +permissions: + contents: read + pull-requests: write + +concurrency: + group: >- + proof-profile-${{ github.event.pull_request.number || + github.event.issue.number || inputs.pr_number }} + cancel-in-progress: true + +jobs: + profile: + runs-on: ubuntu-latest + name: Proof profile (advisory) + # Run on a fresh PR or a workflow_dispatch unconditionally; for issue + # comments, only when the body starts with `/profile` AND the commenter + # has write access. This job checks out and *runs* the PR's Lean code, + # so an untrusted commenter must not be able to trigger it on a fork PR. + if: >- + github.event_name == 'workflow_dispatch' || + github.event_name == 'pull_request' || + (github.event_name == 'issue_comment' && + github.event.issue.pull_request != null && + startsWith(github.event.comment.body, '/profile') && + contains(fromJSON('["OWNER","MEMBER","COLLABORATOR"]'), github.event.comment.author_association)) + steps: + - name: Resolve PR number, head SHA, base SHA + id: pr + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + REPO: ${{ github.repository }} + EVENT_NAME: ${{ github.event_name }} + DISPATCH_PR: ${{ inputs.pr_number }} + PR_FROM_PR_EVENT: ${{ github.event.pull_request.number }} + PR_FROM_COMMENT: ${{ github.event.issue.number }} + run: | + set -euo pipefail + case "$EVENT_NAME" in + workflow_dispatch) pr="$DISPATCH_PR" ;; + pull_request) pr="$PR_FROM_PR_EVENT" ;; + issue_comment) pr="$PR_FROM_COMMENT" ;; + *) echo "::error::Unexpected event $EVENT_NAME"; exit 1 ;; + esac + if [ -z "$pr" ]; then echo "::error::Could not resolve PR number"; exit 1; fi + shas=$(gh api "repos/$REPO/pulls/$pr" --jq '"\(.head.sha) \(.base.sha)"') + head_sha=${shas%% *} + base_sha=${shas##* } + { + echo "number=$pr" + echo "head_sha=$head_sha" + echo "base_sha=$base_sha" + } >> "$GITHUB_OUTPUT" + echo "Resolved PR #$pr — head $head_sha, base $base_sha" + + - name: Checkout PR head + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + with: + ref: ${{ steps.pr.outputs.head_sha }} + fetch-depth: 0 + persist-credentials: false + + - name: Restore caches + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: | + ~/.elan + .lake/packages + .lake/build + key: Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}-${{ steps.pr.outputs.head_sha }} + restore-keys: | + Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json') }}- + + - name: Install Lean + uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 + with: + auto-config: false + use-github-cache: false + use-mathlib-cache: false + + - name: Install Mathlib cache + run: | + if [ ! -d ".lake/packages/mathlib" ]; then + ~/.elan/bin/lake exe cache get + else + echo "Mathlib already present from cache" + fi + + - name: Determine new and modified Lean files + id: files + env: + BASE_SHA: ${{ steps.pr.outputs.base_sha }} + run: | + set -euo pipefail + files=$(git diff --name-only --diff-filter=AM "$BASE_SHA"...HEAD -- LeanPool \ + | grep '\.lean$' \ + | tr '\n' ' ' || true) + echo "files=$files" >> "$GITHUB_OUTPUT" + if [ -z "$files" ]; then + echo "No new or modified Lean files in this diff; profile will no-op." + else + echo "Will profile: $files" + fi + + - name: Build project so profile imports resolve + if: steps.files.outputs.files != '' + run: ~/.elan/bin/lake build LeanPool + + - name: Profile new and modified files + if: steps.files.outputs.files != '' + env: + FILES: ${{ steps.files.outputs.files }} + run: | + : > proof-profile.log + # shellcheck disable=SC2086 # FILES is a space-separated list on purpose + for file in $FILES; do + { + echo "## $file" + # Errors here are logged but never fail the job — this is advisory. + ~/.elan/bin/lake env lean --profile "$file" || true + echo + } >> proof-profile.log 2>&1 + done + + - name: Render profile summary + if: steps.files.outputs.files != '' + run: | + python3 <<'PY' + import os + import re + from pathlib import Path + + log_path = Path("proof-profile.log") + rendered_path = Path("proof-profile.md") + summary_path = Path(os.environ["GITHUB_STEP_SUMMARY"]) + run_url = ( + f"{os.environ['GITHUB_SERVER_URL']}/{os.environ['GITHUB_REPOSITORY']}" + f"/actions/runs/{os.environ['GITHUB_RUN_ID']}" + ) + + # Lean's `cumulative profiling times:` block is one indented + # ` ms` per line. The phase name can contain + # spaces, parens, and hyphens (`compilation (IR)`, + # `let-to-have transformation`, ...). Lean only emits a phase if + # it accumulated nonzero time, so the set of phases differs per + # file and per run; the renderer captures every phase rather than + # cherry-picking known names. + metric_re = re.compile( + r"^[ \t]+(.+?)\s+([0-9]+(?:\.[0-9]+)?)\s*ms\s*$" + ) + + out = ["## Proof profile (new / modified Lean files)\n\n"] + log_text = log_path.read_text() if log_path.exists() else "" + if not log_text.strip(): + out.append("_No proof profile output._\n") + rendered_path.write_text("".join(out)) + summary_path.write_text("".join(out)) + raise SystemExit(0) + + # Split the log into one section per profiled file (delimited by + # `## ` markers written by the profile loop). + sections: list[tuple[str, str]] = [] + name = None + buf: list[str] = [] + for line in log_text.splitlines(): + header = re.match(r"^## (.+)$", line) + if header: + if name is not None: + sections.append((name, "\n".join(buf).rstrip())) + name = header.group(1) + buf = [] + elif name is not None: + buf.append(line) + if name is not None: + sections.append((name, "\n".join(buf).rstrip())) + + if not sections: + out.append("_No files profiled._\n") + else: + # Summary table: cumulative ms = sum over reported phases. + summary_rows = [] + for fname, body in sections: + total = 0.0 + phases = 0 + errors = 0 + for line in body.splitlines(): + if "error:" in line: + errors += 1 + continue + m = metric_re.match(line) + if m: + total += float(m.group(2)) + phases += 1 + summary_rows.append((fname, total, phases, errors)) + summary_rows.sort(key=lambda r: -r[1]) + out.append("| File | Cumulative (ms) | Phases | Errors |\n") + out.append("|---|---:|---:|---:|\n") + for fname, total, phases, errors in summary_rows: + out.append( + f"| `{fname}` | {total:.1f} | {phases} | {errors} |\n" + ) + out.append("\n") + + # Full per-file output, collapsed by default so the comment + # stays scannable when many files are profiled. + out.append("
Per-file profile output\n\n") + for fname, body in sections: + out.append(f"#### `{fname}`\n\n") + out.append("```text\n") + out.append(body if body.strip() else "(empty)") + out.append("\n```\n\n") + out.append("
\n") + + out.append( + "\n_Advisory only — never blocks merge. " + f"[Full log]({run_url}) uploaded as the `proof-profile` " + "artifact._\n" + ) + + rendered = "".join(out) + rendered_path.write_text(rendered) + with summary_path.open("a") as f: + f.write(rendered) + PY + + - name: Post sticky PR comment with profile + if: steps.files.outputs.files != '' + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + PR_NUMBER: ${{ steps.pr.outputs.number }} + REPO: ${{ github.repository }} + run: | + set -euo pipefail + # Marker so we can find and update the same comment on subsequent + # runs instead of stacking new ones. + marker="" + { + printf '%s\n' "$marker" + cat proof-profile.md + } > comment-body.md + + existing=$(gh api "repos/$REPO/issues/$PR_NUMBER/comments" --paginate \ + --jq "[.[] | select(.body | startswith(\"$marker\"))] | first | .id // empty") + + if [ -n "$existing" ]; then + jq -n --rawfile body comment-body.md '{body: $body}' \ + | gh api -X PATCH "repos/$REPO/issues/comments/$existing" --input - + else + gh pr comment "$PR_NUMBER" --body-file comment-body.md + fi + + - name: Upload proof profile + if: always() && steps.files.outputs.files != '' + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: proof-profile + path: proof-profile.log + if-no-files-found: ignore diff --git a/python/lean_pool/quality.py b/python/lean_pool/quality.py index 40f7968993..49644a3424 100644 --- a/python/lean_pool/quality.py +++ b/python/lean_pool/quality.py @@ -34,6 +34,11 @@ r"(?:@\[[^\n\]]+\]\s+)*" r"(?:(?:private|protected|noncomputable|scoped)\s+)*" ) +# A (possibly dotted) Lean identifier: a leading letter or `_`, then letters / +# digits / `_` / `'` / `.`. `\w` and `\W` are Unicode-aware in Python 3, so +# this matches names with subscripts or Greek letters (`c₀`, `α`) that an +# ASCII-only `[A-Za-z0-9_'.]` pattern would truncate. +LEAN_IDENT = r"[^\W\d][\w'.]*" FORBIDDEN_DIAGNOSTICS = re.compile( r"^\s*#(?:check|print|eval!?|reduce|guard_msgs|lint)\b" @@ -340,19 +345,17 @@ def _parse_declarations(root: Path) -> list[_Declaration]: # subsequent `#print axioms` audit would fail with `unknown constant`. decl_pattern = re.compile( rf"^\s*{DECLARATION_PREFIX}({keyword_pattern})\s+" - rf"([A-Za-z_][A-Za-z0-9_'.]*)(?![A-Za-z0-9_'.])" + rf"({LEAN_IDENT})(?![\w'.])" ) for path in _lean_content_files(root): namespace_stack: list[str] = [] stripped = _strip_lean_comments(path.read_text()) for line_number, line in enumerate(stripped.splitlines(), start=1): - namespace_match = re.match( - r"^\s*namespace\s+([A-Za-z_][A-Za-z0-9_'.]*)\s*$", line - ) + namespace_match = re.match(rf"^\s*namespace\s+({LEAN_IDENT})\s*$", line) if namespace_match: namespace_stack.append(namespace_match.group(1)) continue - if re.match(r"^\s*end(?:\s+[A-Za-z_][A-Za-z0-9_'.]*)?\s*$", line): + if re.match(rf"^\s*end(?:\s+{LEAN_IDENT})?\s*$", line): if namespace_stack: namespace_stack.pop() continue @@ -373,6 +376,11 @@ def _is_private_declaration_line(line: str) -> bool: def _qualify_name(namespace_stack: list[str], name: str) -> str: + if name.startswith("_root_."): + # `_root_.Foo.bar` declares `Foo.bar` at the top level regardless of + # the enclosing namespace; strip the escape so the audit emits + # `#print axioms _root_.Foo.bar`, not `_root_._root_.Foo.bar`. + return name.removeprefix("_root_.") if "." in name or not namespace_stack: return name return ".".join([*namespace_stack, name]) diff --git a/python/tests/test_quality.py b/python/tests/test_quality.py index 1cb4d93dfa..eb5a37a0d5 100644 --- a/python/tests/test_quality.py +++ b/python/tests/test_quality.py @@ -135,6 +135,38 @@ def test_quality_check_parses_declaration_with_prime_suffix(tmp_path: Path) -> N assert not any(declaration.name == "foo" for declaration in declarations) +def test_quality_check_parses_unicode_declaration_name(tmp_path: Path) -> None: + """Unicode in declaration names (subscripts, Greek) must not be truncated. + + Regression: an ASCII-only `[A-Za-z0-9_'.]` name pattern parsed `c₀_pos` + as `c`, so the `#print axioms` audit then failed with `unknown constant`. + """ + _write_minimal_repo(tmp_path, "theorem c₀_pos (n : Nat) : n = n := rfl\n") + + declarations = _parse_declarations(tmp_path) + + assert any(declaration.name == "c₀_pos" for declaration in declarations) + assert not any(declaration.name == "c" for declaration in declarations) + + +def test_quality_check_strips_root_escape_from_declaration_name(tmp_path: Path) -> None: + """`theorem _root_.Foo.bar` is recorded as `Foo.bar`, not the escaped form. + + Regression: the escape prefix was kept, so the audit emitted + `#print axioms _root_._root_.Foo.bar` and failed. + """ + _write_minimal_repo( + tmp_path, + "namespace Ns\ntheorem _root_.Foo.bar : True := trivial\nend Ns\n", + ) + + names = {declaration.name for declaration in _parse_declarations(tmp_path)} + + assert "Foo.bar" in names + assert "_root_.Foo.bar" not in names + assert "Ns.Foo.bar" not in names + + def test_quality_check_rejects_oversized_file(tmp_path: Path) -> None: """Files over the 10000-line cap fail; there is no waiver.""" _write_minimal_repo(tmp_path)