search

leanprover-community / lean

Lean 3 Theorem Prover (community fork)
http://leanprover-community.github.io/
Apache License 2.0
435 stars 80 forks source link

Core library linting #200

Open PatrickMassot opened 4 years ago

PatrickMassot commented 4 years ago

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

gebner commented 4 years ago

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

bryangingechen commented 4 years ago

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?

bryangingechen commented 4 years ago

Zulip thread.

gebner commented 4 years ago

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.