Linting tools

[cipher1024]

The goal is to sanitize the mathlib code base but also, the code base of any project depending on it.

Here is a short list of code smells that can be detected automatically:

• unnecessary imports
• unused parameters or assumption
• unused lemmas
• overlapping type class instances
• simp rules that may cause simp loops

These could be implemented by a combination of @digama0's olean parser and some Lean meta programming.

[cipher1024]

@spl, @robertylewis, @rwbarton, @digama0, @johoelzl any thoughts?

[spl]

It all sounds good to me!

[jcommelin]

Another thing that can be detected: duplicate lemmas

[cipher1024]

Would you recommend detecting duplicata via syntactic equality modulo variable renaming?

[jcommelin]

I have no clue what is best... if the versions are next to each other, and one has explicit arguments and the other doesn't, maybe it is on purpose. But if they are in different files... it probably is a mistake. So we need some heuristics...

[cipher1024]

I just built a tool for detecting spurious imports using @digama0's parser: https://github.com/cipher1024/olean-rs

I used it to remove quite a few unneeded imports: #878

[PatrickMassot]

Is there any documentation?

[cipher1024]

not much for now except when you call olean-rs -h:

Usage: olean-rs path/to/file.olean [options]

Options:
    -D, --dump FILE     dump olean parse
    -L                  give location of lean library
    -d, --deps lean.name
                        view all dependents of the target file
    -p DIR              set current working directory
    -u, --unused lean.name
                        list unused imports
    -l lean.name        test lexer
    -t lean.name        testing
    -m, --makefile      generate a makefile to build project
    -h, --help          print this help menu

[cipher1024]

What I've been doing in mathlib/src is lean-rs -m and then make all -j 3. It builds every file in mathlib and, every time, it checks the imports. It has the benefit that, if you change the imports, you can pick up right where you left off after.

[cipher1024]

... now I'm realizing that that doc is wrong :/

[cipher1024]

It should be

Usage: olean-rs [options]

Options:
    -D, --dump FILE     dump olean parse
    -L                  give location of lean library
    -d, --deps FILE
                        view all dependents of the target file
    -p DIR              set current working directory
    -u, --unused FILE
                        list unused imports
    -l lean.name        test lexer
    -t lean.name        testing
    -m, --makefile      generate a makefile to build and check project
    -h, --help          print this help menu

[robertylewis]

I had forgotten about this issue. Some of this is now in the "internal" linter, and perhaps more could be added (#1924).