leanprover-community/physlib

Multigoal linter

Aperta

#353 aperta il 27 feb 2025

Vedi su GitHubGuida contributor
 (0 commenti) (0 reazioni) (0 assegnatari)Lean (139 fork)auto 404
good first issuehelp-wanted

Metriche repository

Star
 (642 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

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

Guida contributor

Direzione di ricerca
Aggiungi la configurazione del linter a lakefile.toml, esegui `lake build` e correggi gli avvisi generati nei file sorgente di PhysLean, sostituendo la sintassi multi obiettivo con prove puntate.
Tech stack
Nessuno
Dominio
developer experience
Tipo issue
Manutenzione
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
2
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-3 ore
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
LeanGit
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
75