Commit 2024-09-25 13:34 c7dedd66

feat: the docPrime linter (#16694) This syntax linter emits a warning on declarations whose name ends with a ' and that have no doc-string. By default, the linter is

• on on mathlib and
• off on projects depending on mathlib. The file scripts/no_lints_prime_decls.txt contains the current exceptions. The exceptions need to be managed manually by design: the expectation is that, once the linter starts, the nolints file should only decrease and never increase. In particular, after the linter flags a declaration, simply adding manually an exception is not enough for CI to be successful. There needs to be a change in the file with the exception (or upstream from it), since otherwise lake will replay the oleans and keep emitting the initial warning. The expectation is that the change will be the addition of a doc-string.