Various website improvements

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

219 stars 70 forks source link

Various website improvements #1154

Closed VojtechStep closed 3 months ago

VojtechStep commented 3 months ago

Renames and moves the "Formalized results from the literature"
Fixes syntax highlighting of Agda flags in the OPTIONS pragma
Fixes #1053
Improves line height for #1141

fredrik-bakke commented 3 months ago

It can also be noted that this PR reduced the font size in code blocks from 15.68 px to 14.56px and increases the font size in text code blocks from 13.72 px to 14.56px.

fredrik-bakke commented 3 months ago

Oh, there seems to be a rendering issue actually. Compare this:

to the live website:

EDIT: The left-hand bar doesn't collapse properly, and git metadata is not present.

VojtechStep commented 3 months ago

Git metadata is not present because we only enable it for CI, not locally, see https://github.com/UniMath/agda-unimath/blob/master/.github%2Fworkflows%2Fpages.yaml#L96-L97

The sidebar issue reminds me of some breakage that happened when we tried to update mdbook. Could you check that you're running 0.4.34? This version is pinned in the Makefile for install-website-dev and the CI script.

Could you compare it with a local build from master, not the live version?

fredrik-bakke commented 3 months ago

ah shoot, I'm running mdbook v.0.4.40

fredrik-bakke commented 3 months ago

Yep, the same issue is present for me when building from master. I'll merge this PR now.