leanprover-community/mathlib4

Make `scripts/add_deprecations.sh` support additivised declarations

Ouverte

#38 550 ouverte le 26 avr. 2026

Voir sur GitHubGuide contributeur
 (3 commentaires) (1 réaction) (0 personne assignée)Lean (1 592 forks)github user discovery
enhancementgood first issue

Métriques du dépôt

Stars
 (3 869 étoiles)
Métriques de merge PR
 (Aucune PR mergée en 30 j)

Description

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).

Guide contributeur

Direction de recherche
Étudiez l'attribut `to additive` et comprenez comment le script traite actuellement les déclarations. Suivez la logique dans `scripts/add deprecations.sh` pour le modifier afin de générer également des alias de dépréciation pour les versions additives.
Stack technique
shell
Domaine
build systemdevops
Type d'issue
Fonctionnalité
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
3
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
Une demi journée
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Plutôt claire
Prérequis
GitShell
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
40