Skip to content

quality.py declaration-name fixes + proof-profile own workflow #35

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Vilin97 merged 2 commits into from
May 10, 2026
Merged

quality.py declaration-name fixes + proof-profile own workflow #35

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
af32eec
quality.py: parse Unicode and _root_.-escaped declaration names
Vilin97 May 10, 2026
db735ca
Move proof profile to its own workflow, triggered like LLM review
Vilin97 May 10, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
211 changes: 0 additions & 211 deletions .github/workflows/lean_action_ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
# `<phase name> <number>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
# `## <file>` 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("<details><summary>Per-file profile output</summary>\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("</details>\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="<!-- proof-profile-comment -->"
{
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
Loading
Loading