Zulip Chat Archive

Stream: general

Topic: Lean in LaTeX


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Apr 02 2020 at 15:08):

What did we do in the paper?

view this post on Zulip Johan Commelin (Apr 02 2020 at 15:09):

That also had this symbol, right?

view this post on Zulip Kevin Buzzard (Apr 02 2020 at 15:10):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip 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/

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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