including listings in LaTeX

Stream: general

[Kenny Lau]

@people who have successfully included LaTeX code (with unicode) in your LaTeX files, how did you do it?

[Kenny Lau]

I'm currently 37 layers deep in errors

[Kenny Lau]

Edit: it seems like all problems have been solved upon switching from pdflatex to lualatex

[Eric Wieser]

Unfortunately some paper submission systems only accept pdflatex

[Eric Rodriguez]

lualatex & minted, with this line:

[Eric Rodriguez]

\AtBeginEnvironment{minted}{%
  \renewcommand{\fcolorbox}[4][]{#4}}

[Eric Wieser]

If you update pygments you shouldn't need that line

[Kenny Lau]

edit: I don't know why, but suddenly minted is complaining that I do not have -shell-escape flag

[Kenny Lau]

but earlier it didn't

[Kenny Lau]

because I typed the flag into the VSCode extension settings

[Eric Rodriguez]

Eric Wieser said:

If you update pygments you shouldn't need that line

ooh that's nice, thanks for fixing that

[Kenny Lau]

    "latex-workshop.latex.tools": [
        {
            "name": "latexmk",
            "command": "latexmk",
            "args": [
                //"-xelatex",
                "-lualatex",
                "-shell-escape",              // <---- added this line
                "-synctex=1",
                "-interaction=nonstopmode",
                "-file-line-error",
                "-shell-escape",              // <---- added this line
                "-lualatex",
                "-shell-escape",              // <---- added this line
                "-outdir=%OUTDIR%",
                "%DOC%"
            ],
            "env": {}
        }
    ]

[Kenny Lau]

I told it three times already

[Kenny Lau]

surely it should enable -shell-escape right

[Eric Rodriguez]

        {
            "name": "shellualatexmk",
            "command": "latexmk",
            "args": [
                "-synctex=1",
                "-shell-escape",
                "-interaction=nonstopmode",
                "-file-line-error",
                "-outdir=%OUTDIR%",
                "%DOC%"
            ],
            "env": {}
        },

works for me

[Eric Rodriguez]

try maybe remove the -xelatex line instead of commenting it out?

[Kenny Lau]

but where do you specify to use lualatex

[Eric Wieser]

There's another pygments bug that I have a PR out for here: https://github.com/pygments/pygments/pull/1817

[Eric Rodriguez]

that's... actually a good question

[Eric Rodriguez]

i think latexmk is lualatex by default maybe?

[Eric Wieser]

Bryan is the one to thank for fixing the red boxes I think

[Eric Rodriguez]

yeah, I just checked and it definitely runs LuaHBTeX, even though I didn't tell it to

[Eric Rodriguez]

that's interesting

[Kenny Lau]

ok I think my -shell-escape error is caused by me using magic command to override

[Kenny Lau]

% !TEX program = lualatex -shell-escape

[Eric Rodriguez]

ahh, and the reason i get luatex by default is because i have a latexmk config file:

[Eric Rodriguez]

$pdflatex = 'lualatex %O %S';
$pdf_mode = 1;
$postscript_mode = $dvi_mode = 0;
$MSWin_back_slash = 0;

[Kenny Lau]


[Kenny Lau]

30b1gx.jpg

[Kenny Lau]

ok so I switched to lualatex and then somehow \C is used to I can't use it to mean $\Bbb C$ so I had to change that command

[Kenny Lau]

but then it's fine

[Kenny Lau]

never mind, it isn't fine, the symbols are missing

[Eric Rodriguez]

the symbols? lualatex supports unicode

[Kenny Lau]

I've been told that

[Eric Wieser]

It could be a font issue now

[Kenny Lau]

what is luahbtex?

[Eric Rodriguez]

got a different font renderer

[Eric Rodriguez]

basically allows colourful emoji

[Kenny Lau]

I swear it worked at one point

[Kenny Lau]

but I have no idea what the settings were

[Kenny Lau]

which is very frustrating

[Kenny Lau]

[73
Missing character: There is no ₁ (U+2081) in font [lmmono10-regular]:!
Missing character: There is no ℕ (U+2115) in font [lmmono10-regular]:!
Missing character: There is no ℕ (U+2115) in font [lmmono10-regular]:!
Missing character: There is no λ (U+03BB) in font [lmmono10-regular]:!
Missing character: There is no λ (U+03BB) in font [lmmono10-regular]:!
]

[Kenny Lau]

wow i found these in over 2000 lines of log

[Patrick Massot]

Kenny, are you using VScode to type LaTeX?! With Lean we are somewhat forced to use VSCode but for LaTeX you should definitely use some decent editor such as emacs or vim.

[Kenny Lau]

those are so difficult to learn

[Mario Carneiro]

I haven't had a major problem using vscode + latex workshop to write latex, although I haven't done anything using lualatex or shell aliases

[Kenny Lau]

@Chris Hughes pointed me to this file which contains a lot of unicode replacements: https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.tex

[Eric Wieser]

Has anyone had any luck making lean listings copy-pastable from pdflatex PDFs?

[Eric Wieser]

I was able to get this working with the accsupppackage in adobe (but not sumatra which has no support for ActualText) using lines like:

\newunicodechar{ℕ}{\BeginAccSupp{method=hex,unicode,ActualText=2115}\ensuremath{\mathbb{N}}\EndAccSupp{}}

where 2115 is the utf-16-be encoding of ℕ.