Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Porting note: unimplemented dangerous_instance linter #12094

Open
grunweg opened this issue Apr 12, 2024 · 0 comments
Open

Porting note: unimplemented dangerous_instance linter #12094

grunweg opened this issue Apr 12, 2024 · 0 comments
Labels
porting-notes Mathlib3 to Mathlib4 porting notes. t-meta Tactics, attributes or user commands tech debt tracking cross-cutting technical debt

Comments

@grunweg
Copy link
Collaborator

grunweg commented Apr 12, 2024

This issue is tracking all porting notes referring to the dangerous_instance linter from mathlib3: as this linter has not been ported to mathlib4 yet, the nolint entries from mathlib3 are commented. Porting notes look like

mathlib4/Mathlib/Algebra/Ring/CompTypeclasses.lean

Line 182 in b0aea61

-- @[nolint dangerous_instance] Porting note: this linter is not implemented yet

Steps to fix

  • port the linter
  • see which of the previous nolints are required: uncomment the necessary ones and delete the now-superfluous ones.
    Remove the porting note in either case.
  • deal with any new errors in mathlib4
  • land the linter and rejoice :-)
@grunweg grunweg added porting-notes Mathlib3 to Mathlib4 porting notes. tech debt tracking cross-cutting technical debt t-meta Tactics, attributes or user commands labels Apr 12, 2024
@jcommelin jcommelin mentioned this issue Apr 13, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue Apr 13, 2024
@grunweg
chore: classify porting notes referring to missing linters (#12098)
c5b5490 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
Louddy pushed a commit that referenced this issue Apr 15, 2024
@grunweg @Louddy
chore: classify porting notes referring to missing linters (#12098)
637d8aa 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
atarnoam pushed a commit that referenced this issue Apr 16, 2024
@grunweg @atarnoam
chore: classify porting notes referring to missing linters (#12098)
5a3545a 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
uniwuni pushed a commit that referenced this issue Apr 19, 2024
@grunweg @uniwuni
chore: classify porting notes referring to missing linters (#12098)
c8626c7 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
callesonne pushed a commit that referenced this issue Apr 22, 2024
@grunweg @callesonne
chore: classify porting notes referring to missing linters (#12098)
b6a07a2 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
Jun2M pushed a commit that referenced this issue Apr 24, 2024
@grunweg @Jun2M
chore: classify porting notes referring to missing linters (#12098)
136f64c 
Reference the newly created issues #12094 and #12096, as well as the pre-existing #5171.
Change all references to #10927 to #5171.
Some of these changes were not labelled as "porting note"; change this for good measure.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
porting-notes Mathlib3 to Mathlib4 porting notes. t-meta Tactics, attributes or user commands tech debt tracking cross-cutting technical debt
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@grunweg