Tracking issue: configuration for linters and further CI checks

[grunweg]

Currently, the project does not set up any configuration for running linters etc. I think it should do so, depending what the goal of the project is. Let's go through the various checks in order:

• I think mk_all should always be enforced. (If a user opts out of that by using globs, they can delete this bit also.) #29 does that

• environment linters: it may depend on the linter; blocked on external PRs

  • some of them are almost surely useful (such as the defLemma linter)
  • the unusedHave linter is probably also useful, perhaps after leanprover/lean4#8117 is backported to the current lean version
  • running the docBlame linter depends on the project's goal: if everything should be upstreamed to mathlib (as for the FLT project), it should absolutely be enabled. If the project is not meant to touch mathlib at all, it need not be. For projects with a mixed structure, enabling it only for the ToMathlib directory would be the most convenient. Such a setting cannot be configured yet, though... Thus, I would suggest asking the user about this in customize_template.py

• mathlib's syntax linters: "everything" be a possible option; leanprover/lean4#8106 will help with that.

  • the header linter (which enforces copyright headers) could be up for discussion. Many downstream projects don't enable it (but add copyright whenever significant new material is upstreamed to mathlib). Adding a copyright header can be a barrier to entry for new contributors, so this may be a sensible choice.
  • I would advocate for the flexible linter to be enabled by default: non-terminal simps are a significant source of churn which new contributors often learn about the hard way. Mathlib has not enabled that linter mostly because there are ~200 errors which are harder to fix. Most new projects should be fine enabling it. (If they know and care about this, they can disable it again.)
  • the style linters are... well, questions of style (hence subjective)
  • the file length linter is a matter of taste: perhaps don't enable it by default

• running shake: I think doing so by default is sensible (A noshake.json file is sensible; a nolints.json file only if needed. For new projects, there is no code yet, hence no need for this.)

• mathlib's text-based linters: these used to be very useful; that that many checks have been (or are being) rewritten as syntax linters, this is less clear-cut. This depends on leanprover-community/mathlib4#21476, but otherwise I'd tend to enable it by default as it's quick and can be useful.

• You may also want to lint for "import Mathlib" statements, as these are often very broad.

[grunweg]

Some concrete proposals for moving forward

• #29 enables mk_all in the default .yml file
• one could similarly add shake
• text-based linters: blocked on the mathlib PR (which is currently awaiting review)
• environment linters:
  • create a PR to runLinter to allow further configuration about enabling (or disabling) linters individually. I have a plan for this and can mentor this.
  • in customize_template.py, ask the user if they want "all mathlib linters" or prefer more fine-grained settings. Detailed options could include "no doc-blame linter" or "only clear errors" (i.e., just the defLemma, checkUnivs and similar linters).
• mathlib's syntax linters:
  • perhaps wait until there is a "mathlib linter" set
  • ask the user if they want "all mathlib linters" or something more fine-grained. Fine-grained questions include asking for "enforcing copyright headers" (the header linter), line length, mathlib's tactic deprecations... this could be fleshed out more.

[pitmonticone]

Thank you very much @grunweg!

I agree linters should be incorporated in LeanProject.

[grunweg]

Brief status update:

• a shake step shouldn't be hard to add
• there is a mathlib linter set now - so I would suggest adding that to the lakefile by default
• I'm not sure if there are any updates regarding the text-based linters