Zulip Chat Archive

Stream: general

Topic: Lean in Beamer

Patrick Massot (Jan 03 2019 at 15:13):

How do people put Lean snippets inside LaTeX Beamer slides? Is there a listings syntax highlighting somewhere?

Patrick Massot (Jan 03 2019 at 15:15):

Hum, google answered https://github.com/leanprover/lean/blob/master/extras/latex/lstlean.md

Patrick Massot (Jan 03 2019 at 15:15):

I'd still be happy to read any comment of advice on this topic

Sebastian Ullrich (Jan 03 2019 at 15:21):

I've switched to minted + luatex + https://bitbucket.org/leanprover/pygments-main for better Unicode support (and better highlighting, I think?). But setting it up isn't trivial, I wouldn't bother if you're happy with listings.

Patrick Massot (Jan 03 2019 at 15:22):

I just discovered listings doesn't seem to like XeLaTeX so I'm not happy at all

Patrick Massot (Jan 03 2019 at 15:23):

Sebastian, do you have setup instruction somewhere?

Sebastian Ullrich (Jan 03 2019 at 15:23):

Not directly, no

Patrick Massot (Jan 03 2019 at 15:24):

if there any Lean-specific issue, or should general documentation apply?

Patrick Massot (Jan 03 2019 at 15:25):

appart from using the above fork of pygment I mean

Sebastian Ullrich (Jan 03 2019 at 15:25):

No, the minted documentation should work fine

Patrick Massot (Jan 03 2019 at 15:26):

Thanks!

Sebastian Ullrich (Jan 03 2019 at 15:26):

Just make sure you don't have the standard pygments installed, I think. It's been a while.

Patrick Massot (Jan 03 2019 at 16:08):

I can't get any unicode character to work :sad:

Sebastian Ullrich (Jan 03 2019 at 16:11):

I don't know anything about Xelatex. Does your monospace font support them?

Patrick Massot (Jan 03 2019 at 16:11):

It's the same with LuaLaTeX, inside or outside Beamer

Patrick Massot (Jan 03 2019 at 16:12):

Do you have any example of a working TeX file?

Sebastian Ullrich (Jan 03 2019 at 16:12):

I.e. does it work in \verb?

Sebastian Ullrich (Jan 03 2019 at 16:13):

This is what I do for unsupported characters:

\usepackage{newunicodechar}
\newfontfamily{\freeserif}{DejaVu Sans}
\newunicodechar{ℕ}{\freeserif{ℕ}}
\newunicodechar{ℝ}{\freeserif{ℝ}}
...

Patrick Massot (Jan 03 2019 at 16:13):

It doesn't work with \verb

Patrick Massot (Jan 03 2019 at 16:14):

But it works with your extra input

Sebastian Ullrich (Jan 03 2019 at 16:14):

Great

Johannes Hölzl (Jan 03 2019 at 16:19):

@Patrick Massot how important is it to use xelatex or lualatex? I use something similar to the following setup with just pdflatex, and it works for me including unicode: https://gist.github.com/johoelzl/cf74935acdcc9f3133fe1aabaace68f0

Patrick Massot (Jan 03 2019 at 16:21):

I use them to be able to use unicode-math

Patrick Massot (Jan 03 2019 at 16:21):

I didn't know you could specify an aspect ratio to Beamer! Now I expect the organizers to tell me what is the aspect ratio of your video beamer!

Johannes Hölzl (Jan 03 2019 at 16:26):

Monday to Wednesday we are in a room called "Agora 1", I never was in this room, but "Agora 3" has 4:3. I can check tomorrow. @Rob Lewis do you know what kind of projection we will have?

Rob Lewis (Jan 03 2019 at 16:34):

Uh, I assume the same as Agora 3. I was also going to check on the whiteboard and projector inputs tomorrow.

Patrick Massot (Jan 03 2019 at 16:35):

Hum, I tried to sed-convert my unicode mapping list to Sebastian's trick, but the 80's fought back: ! TeX capacity exceeded, sorry [input stack size=5000].

Patrick Massot (Jan 03 2019 at 16:37):

Thanks Johannes and Rob! Don't worry too much about that aspect ratio thing, it's almost certainly traditional

Patrick Massot (Jan 03 2019 at 16:37):

@Sebastian Ullrich do you have such a trick for calligraphic letters?

Sebastian Ullrich (Jan 03 2019 at 16:38):

Something like this?

\newunicodechar{𝓞}{\ensuremath{\mathcal{O}}}

Patrick Massot (Jan 03 2019 at 16:40):

I tried that, but then I get a red rectangle around the letter, as we somtimes see on Zulip. I guess this comes from Pygment though.

Patrick Massot (Jan 03 2019 at 16:41):

Oh, I also have it on the left pointing arrow from backward rewrite. Could it mean I don't use the right version of pygment? Is there an easy test here?

Patrick Massot (Jan 03 2019 at 16:49):

Maybe https://bitbucket.org/leanprover/pygments-main/src/50aee5370b53b5d05a2329d5e50ffdce83660d87/pygments/lexers/theorem.py?at=default&fileviewer=file-view-default#theorem.py-448 needs updating?

Sebastian Ullrich (Jan 03 2019 at 16:50):

Riight. You'll want this repo instead... I think https://bitbucket.org/derkha/pygments-main

Gabriel Ebner (Jan 03 2019 at 16:50):

Or this: https://bitbucket.org/gebner/pygments-main/

Gabriel Ebner (Jan 03 2019 at 16:51):

@Sebastian Ullrich You might want to merge my last commit.

Sebastian Ullrich (Jan 03 2019 at 16:52):

But then I'd have to figure out how to do that in hg again

Patrick Massot (Jan 03 2019 at 16:53):

It looks like Gabriel could create a PR, as he would do on GitHub

Gabriel Ebner (Jan 03 2019 at 16:55):

Access denied
Return to the previous page or go back to your dashboard.

:shrug:

Patrick Massot (Jan 03 2019 at 16:57):

or not

Sebastian Ullrich (Jan 03 2019 at 16:59):

Let's just set hg on fire instead

Sebastian Ullrich (Jan 03 2019 at 16:59):

I see pygments development has actually resumed, I'm surprised. So maybe we can even upstream the changes.

Patrick Massot (Jan 03 2019 at 17:00):

That would be soooo nice, especially for Zulip

Patrick Massot (Jan 03 2019 at 17:02):

@Gabriel Ebner are you sure you fixed the caligraphic letter issue?

Patrick Massot (Jan 03 2019 at 17:06):

Indeed it looks like activity resumed two weeks ago. They have only 83 PR to merge know, it's not even twice as many as mathlib!

Gabriel Ebner (Jan 03 2019 at 17:25):

@Patrick Massot No, I just fixed some highlighting issues (keywords, etc.). And this was mainly for sphinx (which uses the html backend). The calligraphic letters are only a problem with the latex backend (they work fine with html).

Patrick Massot (Jan 03 2019 at 17:28):

Would it be easy to fix?

Gabriel Ebner (Jan 03 2019 at 17:43):

I think you just need to add enough \DeclareUnicodeCharacter:

\DeclareUnicodeCharacter{1D49E}{\ensuremath{\mathcal{C}}} \DeclareUnicodeCharacter{1D4A5}{\ensuremath{\mathcal{J}}} \DeclareUnicodeCharacter{1D49F}{\ensuremath{\mathcal{D}}} \DeclareUnicodeCharacter{2964}{\ensuremath{\Rightarrow}} %FIXME \DeclareUnicodeCharacter{3A0}{\ensuremath{\Pi}} \DeclareUnicodeCharacter{2200}{\ensuremath{\forall}} \DeclareUnicodeCharacter{3C0}{\ensuremath{\pi}} \DeclareUnicodeCharacter{226B}{>>} % FIXME \DeclareUnicodeCharacter{22D9}{>>>} % FIXME \DeclareUnicodeCharacter{226A}{<<} % FIXME \DeclareUnicodeCharacter{27F6}{\ensuremath{\to}} \DeclareUnicodeCharacter{27E8}{\ensuremath{\langle}} \DeclareUnicodeCharacter{27E9}{\ensuremath{\rangle}} \DeclareUnicodeCharacter{3BB}{\ensuremath{\lambda}} \DeclareUnicodeCharacter{2245}{\ensuremath{\cong}} \DeclareUnicodeCharacter{2190}{\ensuremath{\leftarrow}} \DeclareUnicodeCharacter{27F9}{\ensuremath{\Rightarrow}} \DeclareUnicodeCharacter{2192}{\ensuremath{\longrightarrow}} % FIXME \DeclareUnicodeCharacter{3B9}{\ensuremath{\iota}} \DeclareUnicodeCharacter{3B1}{\ensuremath{\alpha}} \DeclareUnicodeCharacter{3B2}{\ensuremath{\beta}} \DeclareUnicodeCharacter{2081}{\ensuremath{{}_1}} \DeclareUnicodeCharacter{2082}{\ensuremath{{}_2}}

See https://gist.github.com/gebner/5f0026666e8758d00e87a2eb352f7a43 (This uses the pygmentize -f latex output directly). The same trick probably works with minted as well.