chore: expand warning for the verso.code.warnLineLength linter

[b-mehta]

This PR expands the warning message for the verso.code.warnLineLength linter.

The motivation here came from the MI meeting on verso documentation, in which a new Verso user was confused by this message, in two aspects:

• It is unclear why the line length limit is different in Verso vs in mathlib
• It is unclear how to turn off this linter or adjust its limit (most linters provide this information)

I attempted to fix both of these issues, and keeping the message consistent with the existing core style. (But I could have gotten this wrong).

[github-actions]

Preview for this PR is ready! 🎉

[david-christiansen]

Thanks!

I want to refactor this a bit before merging, but I can take care of that bit.

In particular, the issue is really that wide lines don't render well on narrow viewports (e.g. mobile phones). I'd also like to use our explicit internal API for notes and hints.

I'm getting on a plane soon, so I can't do this immediately, but I'll do it soon.

Thanks again!

[b-mehta]

Thanks for the quick response! If you have a pointer to the explicit internal API you mention, I'm happy to make that aspect of the change myself (I tried figuring out the internal style but clearly wasn't successful!).

For mobile phones, I agree that's an issue, but does that suggest we should have a similar linter for the blog genre too?

[david-christiansen]

I'm in the boarding queue so sorry for bad formatting. It's MessageData.note and Message data.hint': https://leanprover-community.github.io/mathlib4_docs/Lean/Message.html#Lean.MessageData.note https://leanprover-community.github.io/mathlib4_docs/Lean/Message.html#Lean.MessageData.hint ' I agree, generalizing this lint would be useful. It's a bit more fraught in blog because font sizes will vary much more, but that's mostly an argument for this suggested improvement of the message. I'm hoping that once the formatter lands we can compile it to JS and reformat on the fly for different viewport widths. Thanks again! fre. 22. maj 2026, 17.58 skrev Bhavik Mehta ***@***.***>:

…

*b-mehta* left a comment (leanprover/verso#858) <#858 (comment)> Thanks for the quick response! If you have a pointer to the explicit internal API you mention, I'm happy to make that aspect of the change myself (I tried figuring out the internal style but clearly wasn't successful!). For mobile phones, I agree that's an issue, but does that suggest we should have a similar linter for the blog genre too? — Reply to this email directly, view it on GitHub <#858 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAA4FAWPOLQ3TLZSZU2DDI344CBMLAVCNFSM6AAAAACZJJCW5GVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHM2DKMRQHA4DQMJZGY> . You are receiving this because you commented.Message ID: ***@***.***>