feat: add @[trusted_axiom] attribute and linter.untrustedAxioms linter#14407
Open
Kha wants to merge 4 commits into
Open
feat: add @[trusted_axiom] attribute and linter.untrustedAxioms linter#14407Kha wants to merge 4 commits into
@[trusted_axiom] attribute and linter.untrustedAxioms linter#14407Kha wants to merge 4 commits into
Conversation
Member
Author
|
!bench |
|
Benchmark results for 3c2f4be against 8006bb0 are in. There are significant results. @Kha Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
Large changes (2🟥)
Medium changes (2🟥)
Small changes (1✅, 64🟥)
|
github-actions
Bot
added
toolchain-available
leanprover-bot
added
the
builds-manual
Collaborator
|
Reference manual CI status:
|
Member
Author
|
!bench |
|
Benchmark results for ee3ac10 against 8006bb0 are in. There are significant results. @Kha Warning These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.
Large changes (2🟥)
Medium changes (1✅, 12🟥)
Small changes (1✅, 56🟥)
|
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 16, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 16, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 16, 2026
mathlib-lean-pr-testing
Bot
added
the
breaks-mathlib
|
Mathlib CI status (docs):
|
…inter This PR adds a `@[trusted_axiom]` attribute for marking axioms as trusted and a new (default-off) `linter.untrustedAxioms` linter that warns when a declaration added to the environment transitively depends on an axiom not tagged `@[trusted_axiom]`. Co-Authored-By: Claude
`linter.untrustedAxioms` called `collectAxioms` with a fresh cache per declaration, re-walking the module-local dependency subgraph each time (up to +20% instructions on proof-heavy stdlib modules, which enable the linter via `set_option linter.all true`). `exportedAxiomsExt` is now `sync` and filled eagerly by `recordAxioms` from `addDecl`, so entries accumulate along the `checked` environment chain and each constant is walked only once per module; olean serialization reuses the recorded entries instead of recomputing them, making the eager fill instruction-neutral when the linter is off (`Std.Data.DTreeMap.Internal.WF.Lemmas` with export: linter off 40.29G → 40.31G instructions, linter on 48.85G → 42.01G; the remaining enabled-mode delta is mostly warning emission, which core axiom tagging will remove). Also, the `hasSorry` suppression check now runs only when `sorryAx` appears in the collected axioms, skipping the term traversal for sorry-free declarations. Co-Authored-By: Claude
The linter now runs only when `linter.untrustedAxioms` is set explicitly, instead of also being enabled by `linter.all`. The check is useful only with a curated set of `@[trusted_axiom]` declarations and comes with per-declaration cost, so it should not be implied by a blanket linter enable; in particular, the stdlib sets `set_option linter.all true` in many files, which flooded stdlib builds with warnings about the not-yet-tagged core axioms (with `@[trusted_axiom]` tags for them still pending on a stage0 update). `Std.Data.DTreeMap.Internal.WF.Lemmas` now builds warning-free at 40.30G instructions, matching the linter-off baseline. Co-Authored-By: Claude
Kha
force-pushed
the
untrusted-axioms-linter
branch
from
July 16, 2026 11:42
ee3ac10 to
b978969
Compare
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 16, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 16, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 16, 2026
mathlib-lean-pr-testing
Bot
added
builds-mathlib
…rded entries The per-run `seen` cache no longer copies entries answered by `exportedAxiomsExt`; it now contains exactly the constants walked by the run, forming a second layer over the recorded entries. `collectAndGet` answers imported and already-recorded constants directly, and `recordAxioms` inserts the walked constants wholesale instead of filtering every referenced constant. Measured neutral on elaboration benchmarks (the dominant eager-fill cost is the `getUsedConstants` term walk itself, which is accepted); reduces per-declaration allocation and map bookkeeping. Co-Authored-By: Claude
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Jul 17, 2026
mathlib-nightly-testing Bot
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Jul 17, 2026
leanprover-bot
added a commit
to leanprover/reference-manual
that referenced
this pull request
Jul 17, 2026
Member
Author
|
!bench mathlib |
|
Benchmark results for leanprover-community/mathlib4-nightly-testing@602a72a against leanprover-community/mathlib4-nightly-testing@7318bbb are in. No significant results found. @Kha
No significant changes detected. |
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
3 participants
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.
This PR adds a
@[trusted_axiom]attribute for marking axioms as "linter-trusted" and a new (default-off)linter.untrustedAxiomslinter that warns when a declaration added to the environment transitively depends on an axiom not tagged@[trusted_axiom].TODO: tag standard axioms as trusted after stage0 update