lint failed to spot problem

Stream: new members

[Stuart Presnell]

I ran #lint on this code just before PRing it and got the all clear, but it then failed the CI lint check because of the curly braces at lines 141 and 146. Why didn't the local check pick this up?
https://github.com/leanprover-community/mathlib/pull/11440/commits/9e09cf639992e813675898ad3a83d472b1bfd429

[Alex J. Best]

the #lint command only runs the semantic linters (unused arguments etc), syntax linters are a separate thing written in python that you can run locally with scripts/lint-style.py my_file.lean

[Yaël Dillies]

Yeah, I wish we had a #lintstyle command.

[Johan Commelin]

In Lean 4 we'll be able to write the style linters in Lean as well.

[Alex J. Best]

You could try and find a way to call the style linters from lean to implement such a command, but it would necessarily be a hack, Lean doesn't have a good way of getting the current file name (in fact the current file may not even exist). The best thing to do is likely to configure your editor to run the style linters for you. @Julian Berman did this for the neovim plugin if I remember correctly, and it nicely shows the style errors inline as you type

[Stuart Presnell]

That would be nice to have for VS Code

[Julian Berman]

Yeah, it's here: https://github.com/Julian/lean.nvim/wiki/Configuring-&-Extending#mathlib-style-linting -- undoubtedly it should be possible to do this with VSCode I just don't know how to do it offhand, but googling around for showing external linter diagnostics should turn up something. E.g. if you Google for how VSCode python people run flake8 it should be the same