leanprover-community/mathlib4

Make `scripts/add_deprecations.sh` support additivised declarations

Aberta

#38.550 aberto em 26 de abr. de 2026

Ver no GitHubGuia do colaborador
 (3 comentários) (1 reação) (0 responsável)Lean (1.592 forks)github user discovery
enhancementgood first issue

Métricas do repositório

Stars
 (3.869 estrelas)
Métricas de merge de PR
 (Nenhuma PRs mesclada em 30d)

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

Guia do colaborador

Direção de pesquisa
Investigue o atributo `to additive` e entenda como o script atualmente processa as declarações. Trace a lógica em `scripts/add deprecations.sh` para modificá lo para também gerar aliases de depreciação para versões aditivas.
Pilha de tecnologia
shell
Domain
build systemdevops
Tipo Issue
Funcionalidade
DifficultyDificuldade de implementação estimada para um novo contribuidor, de 1 para alterações muito pequenas a 5 para trabalho de nível especializado.
3
Tempo estimadoUm intervalo de tempo aproximado para um colaborador experiente investigar, implementar, testar e preparar um pull request.
Meio dia
Status da atividadeQuão disponível o issue aparece agora: novo, ativo, obsoleto, bloqueado ou aguardando entrada do mantenedor.
Ativo
ClarityCom que clareza o issue explica a mudança esperada, os critérios de aceitação e a próxima etapa.
Principalmente claro
Prerequisites
GitShell
Simpatia para novatosUma pontuação de 1 a 100 que estima o quão acessível este issue é para colaboradores iniciantes.
40