Lean in LaTeX

Stream: general

[Kevin Buzzard]

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]

What did we do in the paper?

[Johan Commelin]

That also had this symbol, right?

[Kevin Buzzard]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Andrew Ashworth]

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]

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]

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

[Sebastian Ullrich]

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

[Kevin Buzzard]

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.