leanprover-community/physlib

Multigoal linter

Ouverte

#353 ouverte le 27 févr. 2025

Voir sur GitHubGuide contributeur
 (0 commentaire) (0 réaction) (0 personne assignée)Lean (139 forks)auto 404
good first issuehelp-wanted

Métriques du dépôt

Stars
 (642 étoiles)
Métriques de merge PR
 (Métriques PR en attente)

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

Guide contributeur

Direction de recherche
Ajoutez la configuration du linter à lakefile.toml, exécutez `lake build` et corrigez les avertissements générés dans les fichiers source de PhysLean, en remplaçant la syntaxe multi objectif par des preuves à puces.
Stack technique
Aucun
Domaine
developer experience
Type d'issue
Maintenance
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
2
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
1-3 heures
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.
Claire
Prérequis
LeanGit
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
75