leanprover-community/physlib

Multigoal linter

Offen

#353 geöffnet am 27.02.2025

Auf GitHub ansehenContributor Guide
 (0 Kommentare) (0 Reaktionen) (0 zugewiesene Personen)Lean (139 Forks)auto 404
good first issuehelp-wanted

Repository-Metriken

Stars
 (642 Sterne)
PR-Merge-Metriken
 (PR-Metriken ausstehend)

Beschreibung

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

Contributor Guide

Research-Richtung
Fügen Sie die Linter Konfiguration zur lakefile.toml hinzu, führen Sie `lake build` aus und beheben Sie die generierten Warnungen in den PhysLean Quelldateien, indem Sie die Multi Goal Syntax durch Aufzählungsbeweise ersetzen.
Tech Stack
Keine
Domain
developer experience
Issue Type
Wartung
SchwierigkeitGeschätzte Implementierungsschwierigkeit für neue Contributors, von 1 für sehr kleine Änderungen bis 5 für Expertenarbeit.
2
Geschätzte ZeitEin grober Zeitrahmen, um zu recherchieren, zu implementieren, zu testen und einen Pull Request vorzubereiten.
1-3 Stunden
AktivitätsstatusWie verfügbar das Issue gerade wirkt: frisch, aktiv, stale, blockiert oder wartet auf Maintainer-Input.
Aktiv
KlarheitWie klar das Issue die erwartete Änderung, Akzeptanzkriterien und den nächsten Schritt erklärt.
Klar
Voraussetzungen
LeanGit
EinsteigerfreundlichkeitEin Score von 1 bis 100, der schätzt, wie zugänglich dieses Issue für First-Time Contributors ist.
75