code too wide

Stream: Zulip meta

[Kevin Buzzard]

I've just noticed that in my post here https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/change.20in.20behaviour.20with.20.60simps.60/near/354350606 I can't resize the (ubuntu) Zulip app window to enable me to see all of the code -- there is always a scrollbar at the bottom. Is there a recommended number-of-characters width for posting code to Zulip?

[Mario Carneiro]

yes, the view width is deliberately upper-bounded, I think this is considered a web dev best practice to avoid long lines when the user has a big monitor

[Mario Carneiro]

using the example as a meter stick, it looks like I would be able to view up to 114-115 characters without a scroll bar. (On zulip desktop, Ubuntu + FF)

------------------------------------- 100 chars ----------------------------------------------------12345678901234

------------------------------------- 100 chars ----------------------------------------------------123456789012345

------------------------------------- 100 chars ----------------------------------------------------1234567890123456

[Mario Carneiro]

Testing again on chromium, the fonts seem to be a bit different and I get much less, 97 chars:

------------------------------------- 90 chars -------------------------------------------1234567

------------------------------------- 90 chars -------------------------------------------12345678

------------------------------------- 90 chars -------------------------------------------123456789

[Eric Wieser]

On windows + chrome I only get 97

--------------------------------- 90 chars -----------------------------------------------1234567

--------------------------------- 90 chars -----------------------------------------------12345678

[Mario Carneiro]

On FF I get either 114 or 115 depending on zoom width, on chromium it seems to be 97 at all zooms

[Mario Carneiro]

On zulip mobile I'm getting what looks like 73 in landscape mode:

----------------------------- 60 chars ---------------------1234567890123

----------------------------- 60 chars ---------------------12345678901234

----------------------------- 60 chars ---------------------123456789012345

[Kevin Buzzard]

Huh so maybe some "best practice" involves sticking to <= 97? I hadn't realised this (obviously when writing code I know to stick to <= 100 but when posting stuff I hadn't realised there was also a constraint). On Zulip desktop with Ubuntu I'm seeing scrollbars in all of the 114+ things Mario is posting.

[Mario Carneiro]

on FF or chrome?

[Kevin Buzzard]

I don't know what that means. I'm using the app.

[Kevin Buzzard]

Is that not "Zulip desktop"?

[Mario Carneiro]

oh whoops I meant the web app

[Kevin Buzzard]

got it

[Mario Carneiro]

I haven't tested the native app

[Kevin Buzzard]

huh, on Ubuntu 22.04 and firefox I see scrolling after 97, so I can't get up to Mario's 114 (I have the browser window pulled across two monitors

[Kevin Buzzard]

I think the moral of the story is to stick to 100 even when posting code

[Mario Carneiro]

I actually see a wider font in really old zulip posts, so possibly something changed in their styling

[Eric Wieser]

Wow, very weird that the font is embedded in the old posts

[Mario Carneiro]

For example this post from 2019 doesn't hit the limit but it has a visibly wider font and if I add characters to it I can get a max of 98 characters before it overflows

[Mario Carneiro]

oh, interesting; it looks like the difference is that old posts use <pre>bla</pre> while new posts use <pre><code>bla</code></pre>, and the styling on <code> is a bit different

[Mac Malone]

Kevin Buzzard said:

Huh so maybe some "best practice" involves sticking to <= 97? I hadn't realised this (obviously when writing code I know to stick to <= 100 but when posting stuff I hadn't realised there was also a constraint).

I know that in code the general principle is to keep lines ~80 characters (i.e., ideally less, but going over is okay when necessary) with a usual max of 100 characters (with 120 being absolute upper maximum I recall hearing in standards). I also know that many editors and code display UIs are designed around this assumption (i.e., generally ensure code boxes can display between 80-100 characters). I imagine that is what Zulip did here.