Repository navigation
quality.py declaration-name fixes + proof-profile own workflow - #35
Merged
Merged
Conversation
The axiom-audit declaration parser used ASCII-only identifier regexes, so a name like `c₀_pos` was truncated to `c` (then `#print axioms` failed with 'unknown constant'), and `theorem _root_.Foo.bar` was kept verbatim (the audit then emitted the doubled `#print axioms _root_._root_.Foo.bar`). Make the identifier patterns Unicode-aware and strip the `_root_.` escape in _qualify_name. Adds regression tests.
Extract the advisory proof-profile job out of lean_action_ci.yml into proof-profile.yml. It now runs once when a PR is opened and re-runs only on a `/profile` comment (from a write-access commenter), mirroring llm-review.yml — instead of on every push. Drops the now-unneeded `pull-requests: write` permission from lean_action_ci.yml.
There was a problem hiding this comment.
Pull request overview
This PR makes two targeted maintenance improvements: it fixes the Python-side axiom-audit declaration parser so it correctly handles Unicode identifiers and _root_.-escaped names, and it moves the (advisory) proof profiling job out of the main Lean CI workflow into its own on-demand workflow to reduce unnecessary runs and tighten permissions.
Changes:
- Update
quality.pydeclaration parsing to be Unicode-aware and to strip_root_.escapes so generated#print axiomscommands resolve. - Add regression tests covering Unicode declaration names and
_root_.Foo.barparsing behavior. - Introduce a dedicated
Proof Profileworkflow triggered on PR open and/profilecomments; remove the old job and unneeded permissions fromlean_action_ci.yml.
Fit: good_fit
Level: undergraduate
Branch: tooling / CI
Mode: mixed
Obscure problem: false
Code quality: 4/5
Significance: Improves correctness of the axiom audit (avoiding false “unknown constant” failures) and reduces CI load by making proof profiling opt-in/advisory instead of running on every push.
Verdict: request_changes
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| python/lean_pool/quality.py | Unicode-aware identifier parsing and _root_. escape stripping for axiom audit declaration collection. |
| python/tests/test_quality.py | Regression tests for Unicode declaration names and _root_-escaped declarations. |
| .github/workflows/proof-profile.yml | New standalone proof profiling workflow with PR-open and /profile triggers plus sticky comment + artifact output. |
| .github/workflows/lean_action_ci.yml | Removes the embedded proof-profile job and drops now-unneeded PR write permission. |
Comment on lines
+40
to
+43
| (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)) |
| jobs: | ||
| profile: | ||
| runs-on: ubuntu-latest | ||
| name: Proof profile (advisory) |
| PY | ||
|
|
||
| - name: Post sticky PR comment with profile | ||
| if: steps.files.outputs.files != '' |
Vilin97
added a commit
that referenced
this pull request
May 10, 2026
…mment The two 'Comment when ...' steps in llm-review.yml ran 'gh pr comment' without --repo or a checkout, so they failed 'not a git repository' on PRs that hit those branches (no .lean files, or Lean CI not green) — this made the 'review' check red on PR #35. Add REPO env + --repo to both. Also remove the now-inert '-- size-limit-ok:' comment from LeanPool/FelConjecture/Solution.lean (the waiver was removed in 702b453; the comment only misleads).
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Two independent changes (the second was requested explicitly):
1.
quality.py: parse Unicode and_root_.-escaped declaration names. The axiom-audit parser's identifier regexes were ASCII-only, sotheorem c₀_poswas parsed asc(then#print axiomsfailed with 'unknown constant' — this is what forced the Kakeya import to renamecoeff_top_eval₂_…), andtheorem _root_.Foo.barwas kept verbatim (audit then emitted#print axioms _root_._root_.Foo.bar). Now Unicode-aware (\w/\Ware Unicode in Py3) and_qualify_namestrips the_root_.escape. Regression tests added.2. Proof profile → its own workflow. Moved the advisory
proof-profilejob out oflean_action_ci.ymlintoproof-profile.yml, triggered on PR-open and on a/profilecomment (from a write-access commenter — the job runs the PR's Lean code, so untrusted comment-triggers are gated), mirroringllm-review.yml. Previously it ran on every push. Also drops the orphanedpull-requests: writepermission fromlean_action_ci.yml.🤖 Opened by Claude Code.