Lint style

Stream: general

[Paul van Wamelen]

If CI complains with ERR_LIN: Line has more than 100 characters, how do I find the file it is complaining about? Is there something I can run locally?

[Mario Carneiro]

It should say the line in question

[Mario Carneiro]

link?

[Paul van Wamelen]

https://github.com/leanprover-community/mathlib/runs/1833692562?check_suite_focus=true

[Bryan Gin-ge Chen]

You can run the style linter locally by going to your mathlib directory and running ./scripts/lint-style.sh, though I think it may fail before it finishes on macOS since mac find doesn't have the command flags needed.

[Mario Carneiro]

but FYI it's the line

def upper_block_triangular_matrix {o : Type*} [fintype o] (M : matrix o o R) (n : ℕ) (b : o → ℕ) :=

[Bryan Gin-ge Chen]

Ah, looks like the change in #5952 caused GitHub to suppress the line info. It should show up eventually on your commit, but we should really have it show up in the log as well. cc: @Eric Wieser

[Eric Wieser]

This page shows the line number: https://github.com/leanprover-community/mathlib/actions/runs/538250041

[Bryan Gin-ge Chen]

Something seems wrong there: it says Lint style: src/data/equiv/basic.lean#L1164, but clicking that link goes to a commit that didn't change that line.

[Mario Carneiro]

Oh, it shows up here too https://github.com/leanprover-community/mathlib/commit/c1960e1c286fc7c86209c074a23df0837637834d

[Mario Carneiro]

it's in the parent commit

[Julian Berman]

If this still isn't runnable locally on macos I am happy to PR fixing it, I should have tried that before my last PR

[Julian Berman]

(so feel free to @ me if that's not the case)

[Bryan Gin-ge Chen]

@Julian Berman Yeah, it's still failing for me:

$ ./scripts/lint-style.sh
+ touch scripts/style-exceptions.txt
+ find src archive -name '*.lean'
+ xargs ./scripts/lint-style.py
++ find . -name '*.lean' -type f -executable
find: -executable: unknown primary or operator
+ executable_files=

Thanks for all your work on this!

[Julian Berman]

OK I'll look at that later.

[Paul van Wamelen]

Thanks all!
Running lint-style.sh on windows gives me

$ ./scripts/lint-style.sh
+ touch scripts/style-exceptions.txt
+ find src archive -name '*.lean'
+ xargs ./scripts/lint-style.py
Traceback (most recent call last):
  File "./scripts/lint-style.py", line 248, in <module>
    lint(Path(filename))
  File "./scripts/lint-style.py", line 231, in lint
    lines = f.readlines()
  File "C:\Anaconda3\lib\encodings\cp1252.py", line 23, in decode
    return codecs.charmap_decode(input,self.errors,decoding_table)[0]
UnicodeDecodeError: 'charmap' codec can't decode byte 0x81 in position 1093: character maps to <undefined>
Traceback (most recent call last):
  File "./scripts/lint-style.py", line 248, in <module>
    lint(Path(filename))
  File "./scripts/lint-style.py", line 231, in lint
    lines = f.readlines()
  File "C:\Anaconda3\lib\encodings\cp1252.py", line 23, in decode
    return codecs.charmap_decode(input,self.errors,decoding_table)[0]
UnicodeDecodeError: 'charmap' codec can't decode byte 0x90 in position 4169: character maps to <undefined>

Is that just my python install that is bad?

[Eric Wieser]

That's likely a bug in the script - it should be opening files with the utf8 encoding

[Eric Wieser]

This line:
https://github.com/leanprover-community/mathlib/blob/4d26028ea2dc978ef4f713d33b2886e61d0a9a40/scripts/lint-style.py#L230

Should pass encoding="utf8"

[Julian Berman]

Fixes (and test): https://github.com/leanprover-community/mathlib/pull/6047