gh-142927: Tachyon: Comma separate thousands and fix singular/plurals

[hugovk]

Thing	Before	After
Console	Captured 4497 samples in 0.45 seconds Sample rate: 10000.01 samples/sec Error rate: 13.74% Heatmap output written to heatmap_69830/ - Index: heatmap_69830/index.html - 93 source file(s) analyzed	Captured 4,411 samples in 0.44 seconds Sample rate: 10,000.01 samples/sec Error rate: 20.40% Heatmap output written to heatmap_70238/ - Index: heatmap_70238/index.html - 92 source files analyzed
Index header
Index file list
Single file header
Single file specialisation

I used the UX improvement issue (#142927) for this, but can change it to the main implementation one (#138122) or another.

• Issue: Improve Tachyon UX #142927

[picnixz]

I'd like to suggest using a locale translation for separating numbers instead of using english-based values. I am personally always confused when commas are used to separate thousands and I think it's better if it's using a localized output.

[StanFromIreland]

I disagree with the "Single file specialisation," IMO the plural sounds better and in general zero takes a plural noun form?

[hugovk]

I'd like to suggest using a locale translation for separating numbers instead of using english-based values. I am personally always confused when commas are used to separate thousands and I think it's better if it's using a localized output.

Right now, the numbers are formatted in the Python script, and then put into the HTML. I guess one way would be to put unformatted numbers in the HTML and use some JS to do locale conversion in the browser?

[hugovk]

I disagree with the "Single file specialisation," IMO the plural sounds better and in general zero takes a plural noun form?

"x/y" is like saying "x of y", and it's the "y" that matters for the plural:

• "0 of 0 instructions"
• "0 of 1 instruction"
• "1 of 1 instruction"
• "1 of 4 instructions"
• "3 of 4 instructions"

[picnixz]

Right now, the numbers are formatted in the Python script, and then put into the HTML. I guess one way would be to put unformatted numbers in the HTML and use some JS to do locale conversion in the browser?

Can't we use localized messages? or maybe pass through locale.(...) for formatting numbers?

[hugovk]

Yes, and that's much simpler :)

How does this 9cfd9ef look?

[picnixz]

It looks better (and simpler). For the "words" we can also use gettext.ngettext to get a possible localized plural form (I don't know if you want all messages to be localized actually, but I think it may makes sense. argparse has localized output and profiling is something that is also very user-facing)

[hugovk]

I'll let you open a followup if you'd like to localise the words :)