doc-gen4 suggestions

Stream: general

[Winston Yin (尹維晨)]

Anybody here maintains doc-gen4? Small suggestions:

1. CSS for h1, h2, etc. should not be fixed to 17px. This erases the visual hierarchy we're used to in docs3.
2. CSS for code, etc. should not be fixed to 16px. Instead, change it to 90%.

I'm open to more fine tuning, but just removing lines 24 and 680 in style.css will be an instant improvement.

[Henrik Böving]

Im the maintainer, feel free to shoot a PR with however many CSS improvements you'd like, I barely survive in the frontend with my skills :D.

[Winston Yin (尹維晨)]

Will do!

[Winston Yin (尹維晨)]

I opened this PR. I ended up making a number of stylistic changes and fixing a couple typos in the CSS.

How do I build and test it on my machine quickly without having to generate the entire mathlib4 docs?

[Winston Yin (尹維晨)]

Before/after
Screenshot-2024-01-05-at-18.44.57.png
Screenshot-2024-01-05-at-18.42.13.png

[Henrik Böving]

Winston Yin (尹維晨) said:

I opened this PR. I ended up making a number of stylistic changes and fixing a couple typos in the CSS.

How do I build and test it on my machine quickly without having to generate the entire mathlib4 docs?

I usually checkout std4 and point it at my local doc-gen

[Michael Stoll]

Winston Yin (尹維晨) said:

Before/after
Screenshot-2024-01-05-at-18.44.57.png
Screenshot-2024-01-05-at-18.42.13.png

BTW, this shows a LaTeX problem of doc-gen4: the spurious commas at the ends of the displayed equations are really tiny spaces "\,". This is a regression vs. what we had with mathlib3, compare the old version of the page.

[Yaël Dillies]

Do people really intentionally add punctuation to centered equations? I always treated that as typos.

[Michael Stoll]

I do, and it is the recommended style of some journals (but others recommend the opposite...).
EDIT: I misread what Yaël wrote. I was talking about the tiny space before the punctuation, not the punctuation as such. I very much agree with what Kevin says below.

[Kevin Buzzard]

I also much prefer a comma in a displayed equation to a comma beginning the next line of text, which I think looks awful.

[Eric Wieser]

Michael Stoll said:

BTW, this shows a LaTeX problem of doc-gen4: the spurious commas at the ends of the displayed equations are really tiny spaces "\,". This is a regression vs. what we had with mathlib3, compare the old version of the page.

My guess is that this is caused by our markdown parser consuming \s inside $ (as it doesn't know about $ at all), meaning by the time Latex sees it, the , is gone.

[Eric Wieser]

We switched parser because the old one was python and that was hard to call from Lean

[Yaël Dillies]

Oh I don't flush the comma to the next line of text. I just omit it'

[Eric Wieser]

Kevin Buzzard said:

I also much prefer a comma in a displayed equation to a comma beginning the next line of text, which I think looks awful.

Where does the comma go if you replace an equation with a lean code sample?
Should it be

example : 1 + 1 = 2 -- ,

which looks silly?

[Eric Wieser]

Or

example : 1 + 1 = 2

, which has an orphaned comma?

[Pedro Sánchez Terraf]

Eric Wieser said:

Kevin Buzzard said:

I also much prefer a comma in a displayed equation to a comma beginning the next line of text, which I think looks awful.

Where does the comma go if you replace an equation with a lean code sample?
Should it be

example : 1 + 1 = 2 -- ,

which looks silly?

Perhaps it is convenient here to regard this as LaTeX example environment, so it should be a standalone paragraph---a new sentence after that :shrug:.

[Michael Stoll]

A feature request: Would it be possible to render instances and defs in different colors?

[Eric Rodriguez]

Kevin Buzzard said:

I also much prefer a comma in a displayed equation to a comma beginning the next line of text, which I think looks awful.

I think neither is best though, imo

[Jireh Loreaux]

That violates readability. A sentence containing mathematics should just be a sentence, albeit with symbols to condense many words. If you remove punctuation then you lose meaning.

[Yaël Dillies]

Well, not if you rephrase the sentence for punctuation not to fall at the end of a formula.

[Mauricio Collares]

I remember when I first noticed punctuation at the end of an equation. I went to excitedly tell a friend, and he just replied with "now open any book you have", and indeed they were there all along.

[Joachim Breitner]

I recommend this book for everyone who cares about these fine issues of math presentation:
https://link.springer.com/book/10.1007/978-3-8348-9599-8

[Yaël Dillies]

Klar! Das werde ich lesen.

[Eric Wieser]

I assume no english translation exists?