Zulip Chat Archive

Stream: Zulip meta

Topic: code too wide


Kevin Buzzard (May 01 2023 at 08:45):

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 (May 01 2023 at 09:00):

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 (May 01 2023 at 09:02):

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 (May 01 2023 at 09:12):

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 (May 01 2023 at 09:14):

On windows + chrome I only get 97

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

Mario Carneiro (May 01 2023 at 09:16):

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

Mario Carneiro (May 01 2023 at 09:23):

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

----------------------------- 60 chars ---------------------1234567890123
----------------------------- 60 chars ---------------------12345678901234
----------------------------- 60 chars ---------------------123456789012345

Kevin Buzzard (May 01 2023 at 09:26):

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 (May 01 2023 at 09:26):

on FF or chrome?

Kevin Buzzard (May 01 2023 at 09:26):

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

Kevin Buzzard (May 01 2023 at 09:26):

Is that not "Zulip desktop"?

Mario Carneiro (May 01 2023 at 09:26):

oh whoops I meant the web app

Kevin Buzzard (May 01 2023 at 09:27):

got it

Mario Carneiro (May 01 2023 at 09:27):

I haven't tested the native app

Kevin Buzzard (May 01 2023 at 09:29):

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 (May 01 2023 at 09:29):

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

Mario Carneiro (May 01 2023 at 09:32):

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

Eric Wieser (May 01 2023 at 09:39):

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

Mario Carneiro (May 01 2023 at 09:39):

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 (May 01 2023 at 10:12):

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 (May 10 2023 at 18:49):

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.


Last updated: Dec 20 2023 at 11:08 UTC