Zulip Chat Archive

Stream: general

Topic: Lint style


view this post on Zulip Paul van Wamelen (Feb 04 2021 at 19:48):

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?

view this post on Zulip Mario Carneiro (Feb 04 2021 at 19:49):

It should say the line in question

view this post on Zulip Mario Carneiro (Feb 04 2021 at 19:50):

link?

view this post on Zulip Paul van Wamelen (Feb 04 2021 at 19:51):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 04 2021 at 19:51):

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.

view this post on Zulip Mario Carneiro (Feb 04 2021 at 19:53):

but FYI it's the line

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

view this post on Zulip Bryan Gin-ge Chen (Feb 04 2021 at 19:54):

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

view this post on Zulip Eric Wieser (Feb 04 2021 at 19:56):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 04 2021 at 19:57):

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.

view this post on Zulip Mario Carneiro (Feb 04 2021 at 19:58):

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

view this post on Zulip Mario Carneiro (Feb 04 2021 at 19:58):

it's in the parent commit

view this post on Zulip Julian Berman (Feb 04 2021 at 19:59):

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

view this post on Zulip Julian Berman (Feb 04 2021 at 19:59):

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

view this post on Zulip Bryan Gin-ge Chen (Feb 04 2021 at 20:00):

@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!

view this post on Zulip Julian Berman (Feb 04 2021 at 20:00):

OK I'll look at that later.

view this post on Zulip Paul van Wamelen (Feb 04 2021 at 20:12):

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?

view this post on Zulip Eric Wieser (Feb 04 2021 at 20:17):

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

view this post on Zulip Eric Wieser (Feb 04 2021 at 20:18):

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

Should pass encoding="utf8"

view this post on Zulip Julian Berman (Feb 04 2021 at 23:14):

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


Last updated: May 14 2021 at 00:42 UTC