Zulip Chat Archive

Stream: general

Topic: best practice for Lean code blocks inside LaTeX?

Scott Morrison (May 16 2019 at 04:03):

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 (May 16 2019 at 06:09):

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

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 (May 16 2019 at 06:18):

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

Last updated: Dec 20 2023 at 11:08 UTC