[loefflerd]

At present the "axiom audit" checker relies on parsing the Lean source to find the names of declarations to test. There are two separate issues with this:

1. the parser does not recognise section with modifiers (@[expose], noncomputable, etc); it ignores these section openings and hence misidentifies the corresponding end as closing the containing scope instead. If this is a namespace block, the result is that it records incorrect full names for subsequent declarations, and the axiom lookup for these fails.
2. In code using Lean's new module system, lemmas are private unless explicitly marked public. The axiom-audit parser does not realise this and attempts to look up these private names in a context where they aren't visible, again resulting in failures.

This PR fixes both problems by dropping the the source-code scan for declaration names and instead reading these from the compiled module metadata (as is already done by the option-manipulation audit). This should be more robust.

Update: the first version failed in CI because of helpers generated for structures with deriving Repr; I have adjusted it to screen out definitions marked as unsafe, with a regression test to check these are not used as back-doors to theorem proofs.

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium impact] The PR appears safe to merge; no actionable new defect was established.

Summary

Replaces source-based declaration lookup with a compiled Lean environment audit.

• The axiom audit checks compiled declarations instead of guessing names from source.

Review was based on source inspection; tests were not run.

_{Reviews (4) · Last reviewed commit: "Merge remote-tracking branch 'upstream/m..." · Reviewed by Greptile}

[Vilin97]

Reviewed all six complete changed files at e9e4f76, including the compiled audit fixture and parser/cache changes. Compiled enumeration addresses generated names and visibility while private dependencies remain in the transitive axiom check. The pinned Lean import defaults and narrow axiom-cache initialization support the no-project-initializer boundary. Output validation and failing subprocess exits fail closed. Unsafe independent roots are excluded, with a rejected-safe-proof fixture and the existing all-declaration backdoor audit retained. I found no isolated-head soundness defect from static review.

Replacing declaration discovery and adding a required workflow fixture changes protected gates, so this needs direct scoped authorization under the repository rules. When composing with #712, retain both fixture suites and update its exact-selector assertion; the extended selector currently breaks that assertion despite selecting the proof-plugin tests. I have not executed the compiler fixtures or qualified hosted CI. No queue or auto-merge was enabled.

[Vilin97]

Current-head source continuation at 1ef7ec4338c3ae86dc9c89f66edb0a595b32c2a8: I checked the six published files after the merge of main. The compiled audit implementation, its embedded Lean programs and existing fixtures retain the reviewed behavior. Of 66 top-level functions/classes in quality.py, only _project_card changes, and its body matches current main. The test merge retains both audit/card imports, the 61 previous test functions and all three main card tests, resolving the former import conflict. No new isolated-head soundness or maintenance defect was found by static review.

The two existing integration conditions in review5732747794 remain: direct scoped authorization for the protected audit/workflow change, and preservation of both fixture suites with the #712 exact-selector assertion updated when they are composed. The three current Lean fixture commands retain this PR’s expanded selector; that does not resolve the separate #712 composition requirement. This review grants no gate-change authority.

I have not run the compiled fixture locally or transferred old-head CI. Complete current-head validation remains separate. No queue, auto-merge or branch mutation was made for this PR.

[Vilin97]

Correction: the current repository worker assignment directly authorizes PR719’s protected audit code, workflow and fixture changes. That resolves the scoped authorization condition in the retained source review. I missed the updated assignment before my earlier queue removal; the replacement native entry is retained for normal protected validation.

The #712 fixture-selector composition requirement applies when #712 lands after this PR; it does not block #719. The favorable exact-head source review remains valid. Complete current candidate checks and normal protections still apply; this update supplies no CI credit or waiver.