search

leanprover / theorem_proving_in_lean

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

Typography issues in 2019-11-13 edition #94

Closed dharmatech closed 4 years ago

dharmatech commented 4 years ago

On the left is the 2019-11-13 edition. On the right is the 2019-08-03 edition. Note that the highlighted character is not displayed correctly in the 2019-11-13 edition:

image

jamesba commented 4 years ago

Came here to report the same.

avigad commented 4 years ago

Thanks for bringing this to my attention. I am not sure what went wrong, but, for the record, here is the fix. We use xelatex for the documentation to handle the unicode characters, together with a file unixode.sty. It has the following line:

  \newunicodechar{Π}{\ensuremath{\mathrm{\Pi}}}

Eliminating unixode.sty almost worked, but some subscripted letters in Section 8.3 broke. Commenting out the line above worked and a Pi in a courier-like font. Deleting \mathrm also worked, and produced a Pi in a better font. I took the latter route, since the resulting symbol matches e.g. the forall symbol best.

We had the same issue with Sigma. Lower case greek letters were working fine though (with mathrm), so I didn't touch anything other than Pi and Sigma.