## Stream: general

### Topic: Lean in LaTeX

#### Kevin Buzzard (Apr 02 2020 at 14:58):

I get an error when copy-pasting the definition of a perfectoid ring into a \begin{lstlisting} \end{lstlisting} block. The error is at the unicode \varpi character and says

ERROR: Package ucs Error: Unknown Unicode character 982 = U+03D6,

--- TeX said ---

(ucs)                possibly declared in uni-3.def.
(ucs)                Type H to see if it is available with options.

See the ucs package documentation for explanation.
Type  H <return>  for immediate help.
...

l.204 (ramified  : ∃ ϖ
: pseudo_uniformizer R, ϖ^p ∣ p in Rᵒ)
--- HELP ---
From the .log file...

Unicode character 982 = U+03D6:
GREEK PI SYMBOL
GREEK SMALL LETTER OMEGA PI
Character available with following options:
mathletters, postscript.
Enter I!<RET> to define the glyph.


Rather than just launching in and trying to fix it myself I thought I'd ask here first. I have the package working fine and displaying other Lean code.

#### Johan Commelin (Apr 02 2020 at 15:08):

What did we do in the paper?

#### Johan Commelin (Apr 02 2020 at 15:09):

That also had this symbol, right?

#### Kevin Buzzard (Apr 02 2020 at 15:10):

Good question. I guess Patrick did some magic or something?

#### Johan Commelin (Apr 02 2020 at 15:10):

Maybe you need to hack your lstlean.tex file: https://github.com/leanprover-community/lean/blob/4b40cea334bfba36e204e65475c1f21db7367b5f/extras/latex/lstlean.tex#L81

#### Kevin Buzzard (Apr 02 2020 at 15:11):

Right -- but I'm not a hacker and I don't know what else I have to do afterwards. I don't really understand TeX packages.

#### Andrew Ashworth (Apr 02 2020 at 16:41):

I think your solution is here: https://en.wikibooks.org/wiki/LaTeX/Source_Code_Listings, at heading "Encoding Issues"

#### Andrew Ashworth (Apr 02 2020 at 16:43):

Another person moaning about LaTeX having issues with UTF-8 here: https://analyzethedatanotthedrivel.org/2011/08/15/typesetting-utf8-apl-code-with-the-latex-lstlisting-package/

#### Andrew Ashworth (Apr 02 2020 at 16:46):

StackOverflow claims that the minted package with XeLaTeX would work seamlessly because it uses Pygments under the hood... although, I have no idea about the current status of Pygments syntax highlighting as seen by the number of red squares in this chat...

#### Bryan Gin-ge Chen (Apr 02 2020 at 16:51):

A fix has been merged into pygments master, no idea when a new version will be released though.

#### Sebastian Ullrich (Apr 02 2020 at 17:04):

Also see https://tex.stackexchange.com/questions/343494/minted-red-box-around-greek-characters for disabling the boxes in minted in general

#### Kevin Buzzard (Apr 02 2020 at 19:28):

We used an old lstlean.tex in the perfectoid project, but someone added a couple of extra lines. I've stared at the diff and added

{ϖ}{{\ensuremath{\mathrm{\mathnormal{\varpi}}}}}1


and

{ᵒ}{{\color{symbolcolor}\ensuremath{^\circ}}}1


but I've basically come up with these lines by some kind of pattern matching algorithm and don't really know if they're right. The color stuff on the little circle is not in our project, it's just guesswork.

Last updated: May 14 2021 at 13:24 UTC