Skip to content

feat: add warning when applying global attribute using in#13223

Merged
wkrozowski merged 4 commits intoleanprover:masterfrom
wkrozowski:wojciech/global_attribute_in
Apr 8, 2026
Merged

feat: add warning when applying global attribute using in#13223
wkrozowski merged 4 commits intoleanprover:masterfrom
wkrozowski:wojciech/global_attribute_in

Conversation

@wkrozowski
Copy link
Copy Markdown
Contributor

@wkrozowski wkrozowski commented Mar 31, 2026

This PR adds a warning preventing a user from applying global attribute using ... in ..., e.g.

theorem a : True := trivial
attribute [simp] a in
def b : True := a

@wkrozowski wkrozowski added the changelog-language Language features and metaprograms label Mar 31, 2026
@wkrozowski
Copy link
Copy Markdown
Contributor Author

wkrozowski commented Mar 31, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 31, 2026 •
edited
Loading

Benchmark results for f92b7f3 against 48800e4 are in. There are no significant changes. @wkrozowski

  • 🟥 build//instructions: +1.7G (+0.01%)

Small changes (2🟥)

  • 🟥 build/module/Init.Data.Subtype//instructions: +3.1M (+0.90%)
  • 🟥 build/module/Lean.Elab.BuiltinCommand//instructions: +325.0M (+2.03%) (reduced significance based on *//lines)

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 1, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 1, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-31 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-04-01 00:27:11)
  • ✅ Reference manual branch lean-pr-testing-13223 has successfully built against this PR. (2026-04-01 23:26:06) View Log
  • 🟡 Reference manual branch lean-pr-testing-13223 build against this PR didn't complete normally. (2026-04-01 23:27:27) View Log
  • ✅ Reference manual branch lean-pr-testing-13223 has successfully built against this PR. (2026-04-02 12:36:05) View Log
  • 🟡 Reference manual branch lean-pr-testing-13223 build against this PR didn't complete normally. (2026-04-02 12:36:49) View Log

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2026
Update lean-toolchain for testing leanprover/lean4#13223
3d5a3aa
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Apr 1, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 1, 2026
Update lean-toolchain for testing leanprover/lean4#13223
deb87e3
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Apr 1, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 1, 2026

Mathlib CI status (docs):

@wkrozowski wkrozowski closed this Apr 1, 2026
@wkrozowski wkrozowski force-pushed the wojciech/global_attribute_in branch from f92b7f3 to 48800e4 Compare April 1, 2026 16:39
@wkrozowski wkrozowski reopened this Apr 1, 2026
@wkrozowski wkrozowski added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Apr 1, 2026
@wkrozowski wkrozowski marked this pull request as ready for review April 1, 2026 19:00
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2026
Update lean-toolchain for leanprover/lean4#13223
a2574fe
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 1, 2026
Update lean-toolchain for leanprover/lean4#13223
7eff816
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 1, 2026

Mathlib CI status (docs):

@wkrozowski wkrozowski force-pushed the wojciech/global_attribute_in branch from 4d67b4b to 59d9492 Compare April 1, 2026 21:53
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 1, 2026
Update lean-toolchain for leanprover/lean4#13223
9e1475e
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 1, 2026
Update lean-toolchain for leanprover/lean4#13223
dd773b3
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 1, 2026
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#13223
fedbb46
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Apr 1, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 2, 2026

Mathlib CI status (docs):

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Apr 2, 2026
Update lean-toolchain for leanprover/lean4#13223
4b683d8
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Apr 2, 2026
Update lean-toolchain for leanprover/lean4#13223
ce608e7
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Apr 2, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#13223
c2edd54
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 2, 2026

Mathlib CI status (docs):

@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Apr 2, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Apr 2, 2026

Mathlib CI status (docs):

@wkrozowski wkrozowski added this pull request to the merge queue Apr 8, 2026
Merged via the queue into leanprover:master with commit 91dd991 Apr 8, 2026
30 checks passed
wkrozowski added a commit to wkrozowski/lean4 that referenced this pull request Apr 10, 2026
@wkrozowski
feat: add warning when applying global attribute using in (leanpr…
8f2876c 
…over#13223)

This PR adds a warning preventing a user from applying global attribute
using `... in ...`, e.g.
```lean4
theorem a : True := trivial
attribute [simp] a in
def b : True := a
```
wkrozowski added a commit to wkrozowski/lean4 that referenced this pull request Apr 12, 2026
@wkrozowski
feat: add warning when applying global attribute using in (leanpr…
0cbf633 
…over#13223)

This PR adds a warning preventing a user from applying global attribute
using `... in ...`, e.g.
```lean4
theorem a : True := trivial
attribute [simp] a in
def b : True := a
```
volodeyka pushed a commit that referenced this pull request Apr 16, 2026
@wkrozowski @volodeyka
feat: add warning when applying global attribute using in (#13223)
ba2fc20 
This PR adds a warning preventing a user from applying global attribute
using `... in ...`, e.g.
```lean4
theorem a : True := trivial
attribute [simp] a in
def b : True := a
```
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@wkrozowski @leanprover-radar @leanprover-bot