leanprover-community/mathlib4

Make `scripts/add_deprecations.sh` support additivised declarations

Offen

#38.550 geöffnet am 26.04.2026

Auf GitHub ansehenContributor Guide
 (3 Kommentare) (1 Reaktion) (0 zugewiesene Personen)Lean (1.592 Forks)github user discovery
enhancementgood first issue

Repository-Metriken

Stars
 (3.869 Sterne)
PR-Merge-Metriken
 (Keine gemergten PRs in 30 T)

Beschreibung

Currently, changing

@[to_additive]
lemma foo_mul ...

to

@[to_additive]
lemma bar_mul ...

then running scripts/add_deprecations.sh creates

@[to_additive]
lemma bar_mul ...

@[deprecated ...] alias foo_mul := bar_mul

It should instead create

@[to_additive]
lemma bar_mul ...

@[deprecated ...] alias foo_mul := bar_mul
@[deprecated ...] alias foo_add := bar_add

Note that

@[to_additive (attr := deprecated ...)] alias foo_mul := bar_mul

doesn't work because deprecated loses track of what the deprecated declaration is an alias of (see #19424).

Contributor Guide

Research-Richtung
Untersuche das `to additive` Attribut und verstehe, wie das Skript derzeit Deklarationen verarbeitet. Verfolge die Logik in `scripts/add deprecations.sh`, um es so zu ändern, dass es auch Deprecation Aliase für additive Versionen generiert.
Tech Stack
shell
Domain
build systemdevops
Issue Type
Funktion
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
3
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
Halber Tag
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Aktiv
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Meist klar
Voraussetzungen
GitShell
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
40