Tracking Issue: Refactoring Ideas

[BoltonBailey]

This issue is based on the list from this discussion on Zulip. It contains a number of items of technical debt or refactoring possibilities. Contributors should feel free to:

• Add to this list by editing this comment
• Implement counters for items not tracked by the Tech Debt Bot, and add them to the bot's report.
• Submit PRs to reduce or resolve these issues.

Things tracked by the Tech Debt bot

• Porting notes from the Lean 3 to Lean 4 port.
• backwards compatibility flags
• skipAssignedInstances flags
• adaptation notes
• disabled simpNF lints
• erw
• maxHeartBeats modifications
• disabled deprecation lints
• documentation nolint entries
• Files >1500 lines long
• exceptions for the docPrime linter
• Deprecated files
  • The tech debt counter also tracks the number of lines of code in Deprecated files

Things tracked by other tracking issues

• Linters
• Naming consistency

Other Items

• Triage old issues: updating the state of a tracking issue is useful information. If you think a PR resolved an issue, pinging the author with a friendly message can be useful.
• Help out with PRs: the review dashboard has a section with PRs needing help. For PRs with just a merge conflict, please be tactful and keep in mind that most contributors are volunteers working in their free time - e.g., don't expect faster reactions than a week.
• organisational debt: documenting existing mathlib policies, that are not formally written down. The deprecation policy comes to mind (and has an open PR). If you see something else, feel free to propose a PR (and leave a comment here, as zulip is read more often than the webpage repository). This thread aims to collect some examples.
  • document the current policy about using "open (scoped) classical". Much of it is enforced by a linter; some aspects are still being discussed
  • Document the current spelling policy (British/American/other variants of English). See e.g. here; might need further waiting (or work to build consensus)
  • Another informal policy incoming (still under discussion): "file names should be UpperCamelCase" (except for specific exceptional cases). If the discussion converges, a PR documenting this is very welcome.
    Michael Rothgang:
    Adding to 19: a linter implementing this is also very welcome; I'm happy to mentor that.
• Document top folder directories and their main subdirectories with a README.md file
• Sort/split basic algebra files into the folders Algebra.Group, Algebra.GroupWithZero, Algebra.Ring, Algebra.Field, and their Algebra.Order counterparts.
• Tooling consolidation: rewrite the lint-style.py linters in Lean or as syntax linters. Requires some knowledge of syntax linting, but can be fun. Michael Rothgang can answer questions.
• fixing TODOs in the source code: often, a number of these are doable. Sometimes, TODOS can be very hard. Usually a PR is welcome. (If a TODO is hard, talking to the author of the TODO helps.)
• Improve David Renshaw's excellent tryAtEachStep tool, so it can be used to drive automatic tactic replacements. In particular see Kim's issue request: filter by reducing number of heartbeats dwrensha/tryAtEachStep#12 allowing filtering by the change in heartbeats.
• Replace terminal simp only with simp or simp [X], when there is minimal build time cost.
• Programming/linter-related; doesn't require deep knowledge: Rewrite the directory Dependency linter to take an allowlist of directories, instead of blocklisting them. (Or perhaps use a hybrid approach.)
• Help with reorganising top-level folders --- some of these are not logical. See here for more details. Typically, this may need some discussion on zulip.
• (Due to Eric Wieser) #24099 is also looking for crowd help: it does not require expert knowledge, but some familiary with the respective part of the library.
• Help categorising the list of all tactics in the mathlib manual: this comment has more details.
• Create PRs to mathlib (and dependencies) marking alternative forms of tactics with @[tactic_alt original_tactic], cleaning-up docstrings as you do so, i.e. describing all tactic alternatives in the main tactic's docstring. This comment links to an example. This would also help the mathlib manual.