search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 46 forks source link

Font changes #96

Closed dharmatech closed 4 years ago

dharmatech commented 4 years ago

Not sure if this is considered a huge deal or not but it looks like the font changed since the August 3rd edition.

Left: 2019-08-03 edition Right: 2019-12-12 edition

image

Note that the text highlighted on the left does not extend to the full line on the right. So it seems like the new font there is smaller or more condensed.

Here's some text from a chapter header. The text in red-outline is from the 2019-12-12 edition. The other text is from 2019-08-03.

image

The differences are subtle, but it seems a different font was used here as well.

Again, not sure if it's considered an issue, but just wanted to report it in case the changes were not intentional.

avigad commented 4 years ago

Thanks for the information. We use Sphinx with Xelatex to handle the unicode characters. According to the documentation, Sphinx with Xelatex uses the FreeFont Open Type family: https://www.sphinx-doc.org/en/master/latex.html. I don't know what caused the change, but it doesn't seem to be a problem.