leanprover-community/mathlib4

Make `scripts/add_deprecations.sh` support additivised declarations

Aperta

#38.550 aperta il 26 apr 2026

Vedi su GitHubGuida contributor
 (3 commenti) (1 reazione) (0 assegnatari)Lean (1592 fork)github user discovery
enhancementgood first issue

Metriche repository

Star
 (3869 stelle)
Metriche merge PR
 (Nessuna PR mergiata in 30 g)

Descrizione

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

Guida contributor

Direzione di ricerca
Investiga l'attributo `to additive` e comprendi come lo script elabora attualmente le dichiarazioni. Traccia la logica in `scripts/add deprecations.sh` per modificarlo in modo da generare anche alias di deprecazione per le versioni additive.
Tech stack
shell
Dominio
build systemdevops
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
Mezza giornata
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Abbastanza chiara
Prerequisiti
GitShell
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
40