feat: add @[attribute] for registering custom attributes

[Kha]

This PR adds a new @[attribute] attribute that registers a constant of type Lean.AttributeImpl as a custom attribute, lifting the previous restriction that all attributes had to be registered via registerBuiltinAttribute from inside an initialize block. A new attributeExt environment extension stores the registered attributes, and getAttributeImpl now consults both it and the existing attributeExtension (which keeps serving builtin attributes and parser category builders).

Because @[attribute] registers eagerly during elaboration (via applicationTime := .afterCompilation) rather than at module load, custom attributes can be applied in modules that import the defining module — including in the same file as the orphan applications they target — without the artificial split that initialize-based registration forces. The attribute definition and the underlying environment extension, if any, however still need to be split.

The accompanying parser change registers attribute as a syntax kind in the attr category alongside the other keyword-named attribute forms (class, instance, macro, export).

[Kha]

!bench

[leanprover-radar]

Benchmark results for 944beb6 against fe3c739 are in. No significant results found. @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.

• Runner for run build has different system configurations between commits.
• Runner for run other has different system configurations between commits.

• 🟥 build//instructions: +6.6G (+0.05%)

Small changes (1✅, 4🟥)

• 🟥 build/module/Lean.Attributes//instructions: +506.3M (+8.98%) (reduced significance based on *//lines)
• 🟥 build/module/Lean.Parser.Attr//instructions: +64.2M (+3.24%) (reduced significance based on *//lines)
• 🟥 build/module/Std.Time.Date//instructions: +3.1M (+0.82%)
• ✅ compiled/parser//instructions: -14.4M (-0.04%)
• 🟥 misc/re-elab watchdog Init.Data.List.Sublist//task-clock: +1s (+3.18%)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-05-03 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-05-04 15:24:13)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-13629 has successfully built against this PR. (2026-05-04 16:21:30) View Log