leanprover-community/physlib

Multigoal linter

Aberta

#353 aberto em 27 de fev. de 2025

Ver no GitHubGuia do colaborador
 (0 comentário) (0 reação) (0 responsável)Lean (139 forks)auto 404
good first issuehelp-wanted

Métricas do repositório

Stars
 (642 estrelas)
Métricas de merge de PR
 (Métricas PR pendentes)

Description

The whole of PhysLean needs the MultiGoal linter run on it and all the warnings dealt with.

In particular

[leanOptions]
linter.style.multiGoal = true

should be added to lakefile.toml and the project built with lake build. This will generate warnings, some of which may be from Mathlib, but the ones from PhysLean should be dealt. For example:

   exact h 
   exact h2

should be replaced with:

  · exact h1 
  · exact h2

Guia do colaborador

Direção de pesquisa
Adicione a configuração do linter ao lakefile.toml, execute `lake build` e corrija os avisos gerados nos arquivos fonte do PhysLean, substituindo a sintaxe multi objetivo por provas com marcadores.
Pilha de tecnologia
None
Domain
developer experience
Tipo Issue
Manutenção
DifficultyDificuldade de implementação estimada para um novo contribuidor, de 1 para alterações muito pequenas a 5 para trabalho de nível especializado.
2
Tempo estimadoUm intervalo de tempo aproximado para um colaborador experiente investigar, implementar, testar e preparar um pull request.
1-3 horas
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.
Claro
Prerequisites
LeanGit
Simpatia para novatosUma pontuação de 1 a 100 que estima o quão acessível este issue é para colaboradores iniciantes.
75