lean icon indicating copy to clipboard operation
lean copied to clipboard

Core library linting

Open PatrickMassot opened this issue 4 years ago • 4 comments

Should we somehow run the mathlib linters on the core library. For instance it would catch mul_nonneg which uses forbidden inequalities.

PatrickMassot avatar Apr 24 '20 17:04 PatrickMassot

YES! YES! YES!

If you open src/tactic/lint/default.lean in mathlib and write #lint_all, then you can already see the linting errors for the core library. IMHO we should change mathlib CI so that it runs the linters for the core library as well. There are quite a few linters where declarations in mathlib can cause linting errors in core.

cc @leanprover-community/mathlib-maintainers for visibility

gebner avatar Apr 24 '20 17:04 gebner

If you open src/tactic/lint/default.lean in mathlib and write #lint_all, then you can already see the linting errors for the core library.

Here's a gist based on a recent mathlib with 3.14.0c.

To fix these, should we just start opening random linting PRs here or do we want to do something more systematic?

  • [x] duplicated namespaces (#267).

bryangingechen avatar Apr 27 '20 02:04 bryangingechen

Zulip thread.

bryangingechen avatar Apr 29 '20 16:04 bryangingechen

To fix these, should we just start opening random linting PRs here or do we want to do something more systematic?

If PRs are opened, they will be merged. I don't think I'm motivated to do something more organized at the moment, but it's welcome if somebody else does it.

gebner avatar May 01 '20 20:05 gebner