Linting in VS code

Stream: mathlib4

[Thomas Murrills]

Is VS code with the lean extension supposed to word-wrap for you? Currently word wrapping in VS code (alt Z) refers only to visual word-wrapping, as opposed to actually chopping up lines with newlines when they get too long. (I tried running scripts/lint-style.sh on advice, but got the error (touch: scripts/style-exceptions.txt: No such file or directory)

[Yaël Dillies]

No, sorry for the confusion, it's only a visual aid.

[Thomas Murrills]

Gotcha! Others seemed to suggest that somehow the lean extension was capable of wrapping via newlines at 100 characters, though. Did I interpret what was said correctly?

[Yaël Dillies]

Pretty sure they meant the vertical bar here

[Thomas Murrills]

Hmm, ok. So is it standard practice to go through and insert newlines at 100 characters by hand?

[Mario Carneiro]

yes. Automatic line wrapping would play havoc with lean's whitespace sensitivity unless lean is doing the reformatting

[Jireh Loreaux]

Generally you're writing new code instead of copying, so hitting Enter isn't a big deal. It's just a bit weird because mathport is outputting long lines in comments right now.

[Mario Carneiro]

in comments? If they are lean 3 comments then they should already be line-wrapped

[Mario Carneiro]

do you mean mathport's own notes (e.g. error messages)?

[Jireh Loreaux]

Yeah, for example, the output of dubious translations.

[Jireh Loreaux]

I'm not saying it's a big deal, only that it's not something that would be an issue under normal circumstances.

[Mario Carneiro]

those lines should generally be deleted from the file

[Mario Carneiro]

I think mathport's output can also be > 100 characters in regular code, it's using the default formatter settings which I think might be a bit more than 100 chars

[Jireh Loreaux]

I've seen that in a few places too.