best practice for Lean code blocks inside LaTeX?

Stream: general

[Scott Morrison]

I understand I'll have to use xelatex, in order to cope with unicode symbols. Does anyone have a nice solution for displaying code blocks?

[matt rice]

I have in the past had luck following: https://github.com/leanprover-community/lean/blob/master/doc/syntax_highlight_in_latex.md

using minted/the lean pygments fork, Also see here for something to try if having issues with unicode symbols
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lean.20in.20Beamer/near/154253727

I recently had a case where the (lean chat link) didn't work, and I had to resort to:

\usepackage{newunicodechar} \usepackage{fontspec} \AtBeginDocument{\setmainfont[ BoldFont={STIX2Text-Bold.otf}, ItalicFont={STIX2Text-Italic.otf}, BoldItalicFont={STIX2Text-BoldItalic.otf} ] {STIX2Text-Regular.otf}} \newfontfamily{\mathfont}{STIX2Math.otf} \AtBeginDocument{\newunicodechar{⋁} {\mathfont{⋁}}}

[matt rice]

that said, recently i've been hacking on using https://crates.io/crates/syntect/, and generating the syntax highlighting directly from the same highlighter as used by the vscode extension, so it looks the same, and syntect is a lot easier of a dependency to require (IMO), but it's not ready yet