lstlean with beamer

Stream: general

[Adam Topaz]

I'm trying to typeset a beamer presentation using lstlean, but I can't get it to work. Is there some known incompatibility between beamer and listings/lstlean? Everything works fine once I change beamer to article (or amsart). Has anyone successfully used lstlean with beamer?

[Adam Topaz]

Ah it looks like Floris answered my question a few months ago
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20LaTeX.20beamer/near/281319800

[Kevin Buzzard]

I just make everything fragile when I'm doing lean in beamer :-)

[Kevin Buzzard]

AFAIK making everything fragile doesn't break anything

[Jeremy Avigad]

In VS Code with the LaTeX Workshop extension, you can control click in the PDF viewer window and jump to the relevant place in the source. The [fragile] tag breaks that, but otherwise I have not noticed any bad effects.

[Adam Topaz]

Interesting. I'm using emacs, and it seems that reverse lookup works (in beamer) if I ctrl-click as long as it's outside of a verbatim block.
Clicking inside a verbatim block (same goes for listings), it jumps to the .vrb file instead of the .tex file.