XeLaTeX with minted error

Stream: new members

[Moti Ben-Ari]

After installing Pygments and minted, and setting up the files as required, I ran the example code from https://lean-lang.org/lean4/doc/syntax_highlight_in_latex.html.
I got the following error

(C:\Users\admin\AppData\Local\Programs\MiKTeX\tex/latex/base\ts1cmr.fd)
(_minted-test/default.pygstyle)Error: no lexer for alias 'lean4.py:Lean4Lexer -x' found
! Package minted Error: Missing Pygments output; \inputminted was
probably given a file that does not exist--otherwise, you may need
the outputdir package option, or may be using an incompatible build tool,
or may be using frozencache with a missing file.

[Eric Wieser]

It looks like you forgot to save the lean4.py file next to your tex file

[Moti Ben-Ari]

Eric Wieser said:

It looks like you forgot to save the lean4.py file next to your tex file

No ....
files.jpg

[Utensil Song]

This is a static error message, it could actually be caused by quite a few different reasons: https://tex.stackexchange.com/questions/440511/package-minted-error-missing-pygments-output

[Eric Wieser]

It would be worth checking if things work with lean (aka lean3) instead of lean4.py:Lean4Lexer -x first (which is built in to pygments)

[Moti Ben-Ari]

@Utensil Song : I tried the suggestions from stackexchange. Adding cache=false to \userpackage{minted} removed the errors concerning the cache, but I still get

(C:\Users\admin\AppData\Local\Programs\MiKTeX\tex/latex/base\ts1cmr.fd)
(test.out.pyg)Error: no lexer for alias 'lean4.py:Lean4Lexer -x' found

The permissions were OK.

@Eric Wieser : Is this what you mean?

\newmintinline[lean]{lean.py:LeanLexer -x}{bgcolor=white}
\newminted[leancode]{lean.py:LeanLexer -x}{fontsize=\footnotesize}

No change.

[Eric Wieser]

I mean replace lean4.py:Lean4Lexer -x with lean, not with lean.py:LeanLexer -x

[Eric Wieser]

This will use the lean3 highlighting, but it will tell you whether the problem is to do with lean4.py or minted

[Utensil Song]

OK, I've reproduced the error and solved it.

[Utensil Song]

2 key issues for me:

1. My LaTeX compile command is xelatex --shell-escape -output-directory=../print print.tex which changed output directory, so I need to use option outputdir=../print for minted
2. For some reasons, cache also doesn't work properly in this case, so I also need cache=false.

Result:

\usepackage[cache=false,outputdir=../print]{minted}

[Utensil Song]

The above only caused a delusion, LaTeX no longer error, but there is also no code highlight output. The true issue is the quoting. Looking into the LaTeX log (../print/print.log for me), there is a command:

pygmentize -l 'lean4.py:Lean4Lexer -x' -f latex -P commandprefix=PYG
-F tokenmerge -P stripnl='False' -o ../print/_minted-print/0E5380BA5684F7C1B2CE
81B5A73A997A0298A94EFC840CC8AEFBE5423A43D7A4.pygtex ../print/print.pyg

merge it into one line and execute in the same directory of your LaTeX main source file and the lean4.py, this will also error. But if you remove the single quotes, it works fine, and you can see pygtex files generated in _minted-print. This is caused by gpoore/minted#360 .

[Utensil Song]

A complicated workaround that requires adaptation is also provided in the issue, by overriding some macros in the LaTeX preamble. This issue is a "won't fix" for minted, instead minted will release a new way to support custom lexers which will release by early 2024. :joy:

[Utensil Song]

I have my adapted fix here for your reference (you only need to check preamble.tex and fix_minted.tex), the issue itself is solved, but another minted issue involving "missing $ is inserted" surfaced, and I don't have any more time for minted.

[Moti Ben-Ari]

@Utensil Song What do I do with preamble.tex and fix_minted.tex? MiKTeX just installed a style file for minted. Should I also use the new lean4.tex and lean4.py?

[Utensil Song]

Moti Ben-Ari said:

Utensil Song What do I do with preamble.tex and fix_minted.tex? MiKTeX just installed a style file for minted. Should I also use the new lean4.tex and lean4.py?

You only need to add fix_minted.tex, and use \input to include it in the location you observed in preamble.tex (that is somewhere afer your \usepackage{minted}) in your own preamble file which might be named differently. Everything else are irrelevant.

[Moti Ben-Ari]

My native language is LaTeX :smile: but I'm way out of my depth with minted and pygments. The following

\documentclass{article}
\usepackage{fontspec}
% switch to a monospace font supporting more Unicode characters
\setmonofont{FreeMono}
\usepackage[cache=false]{minted}
% instruct minted to use our local theorem.py
\newmintinline[lean]{lean4.py:Lean4Lexer -x}{bgcolor=white}
\newminted[leancode]{lean4.py:Lean4Lexer -x}{fontsize=\footnotesize}
\usemintedstyle{tango}  % a nice, colorful theme
\begin{document}
\input{fix_minted}   %%%%%%%%% <- ???
\begin{leancode}
theorem funext {f₁ f₂ : ∀ (x : α), β x} (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by
  show extfunApp (Quotient.mk' f₁) = extfunApp (Quotient.mk' f₂)
  apply congrArg
  apply Quotient.sound
  exact h
\end{leancode}
\end{document}

gives a missing $ inserted error. In preamble.texthe path is blueprint/src/ which I can't find.

Sorry if I'm taking up too much of your time! It's not urgent and I can wait for the official fix.

[Utensil Song]

\input{fix_minted} needs to be before \newmintinline etc., immediately after \usepackage[cache=false]{minted}.

[Moti Ben-Ari]

Since I don't need syntax highlighting for now, I found a simple way to get monospaced text with the unicode symbols

\documentclass{article}
\usepackage{times}
\usepackage{fontspec}
\setmonofont{FreeMono}
\parindent=0pt
\newcommand*{\ind}{\hspace*{2em}}
\begin{document}
How to format $\forall x ( f_1\neq f_2)=f_1$:

\begin{ttfamily}
∀ (x : α), β x (h : ∀ x, f₁ x = f₂ x) : f₁ ≠ f₂ := by\\
\ind{}show extfunApp (Quotient.mk' f₁) = \\
\ind{}\ind{}extfunApp (Quotient.mk' f₂)
\end{ttfamily}
\end{document}

image.png

When the minted stuff gets fixed it will be easy to change by a global replace.

[Utensil Song]

If that's all you need, any variant of verbatim would suffice.

[Utensil Song]

Or you could just use the listings choice, which works fine for me.

[Utensil Song]

Previously I got minted working for the old Lean lexer (presumably Lean 3 only but works most of the time for Lean 4 too) but didn't like how it floods the LaTeX output and the need of shell escape so I stopped using it.

[Moti Ben-Ari]

At some point verbatim didn't work but now it does!

[Utensil Song]

But minted has a nice feature of mathescape which I think is particularly useful for Lean code/proof (so does lstlisting).

image.png

[Utensil Song]

Utensil Song said:

If that's all you need, any variant of verbatim would suffice.

Have you tried moreverb or fancyvrb?

[Eric Wieser]

You can also just use minted with the built-in lean 3 highlighter, which is better than nothing but less work than the hack to use the custom lean 4 highlighter

[Eric Wieser]

Ideally we'd just upstream the lean 4 highlighter into pygments, though I think it's based off an old version of the lean 3 one and should probably integrate the subsequent changes first

[Utensil Song]

Eric Wieser said:

You can also just use minted with the built-in lean 3 highlighter, which is better than nothing but less work than the hack to use the custom lean 4 highlighter

Which could take this commit for reference. It worked.

[Eric Wieser]

That still looks like it uses a custom lexer?

[Utensil Song]

Eric Wieser said:

That still looks like it uses a custom lexer?

Yep, do you have some pre-custom lexer code for this? I haven't tested that lately.

[Eric Wieser]

Lean3 is built-in to minted

[Eric Wieser]

No custom lexer needed

[Eric Wieser]

Just ask minted for lean like you would python

[Eric Wieser]

(As of the latest pygments release you can also use lean3, though I don't know how pygments releases interact with TeX live releases)

[Utensil Song]

Oh, just checked, yes, previously it was just

\usepackage{minted}
\setminted{
  fontsize=\scriptsize,
  frame=single,
  breaklines,
  samepage
}

\mintinline{lean}{some_lean_code}

\begin{minted}[autogobble]{lean}
some_longer_lean_code
\end{minted}

[Eric Wieser]

I created lean4#3047

[Utensil Song]

Eric Wieser said:

I created lean4#3047

Probably guiding users to that issue is not gonna help, the workaround has not been confirmed to work.

[Utensil Song]

gpoore/minted#350 looks more promising.

[Eric Wieser]

Maybe the compromise is to reference that issue from the one I link to, since mine feels more canonical.

[Utensil Song]

Hopefully the PR would be recovering the old instruction that's guaranteed to work, or the new working solution (that still requires some further debugging to work).

[Utensil Song]

Eric Wieser said:

Maybe the compromise is to reference that issue from the one I link to, since mine feels more canonical.

Users can discover gpoore/minted#350 from gpoore/minted#360 (350 referenced 372, 372 is referenced by 360), so it's fine to use 360.

[Moti Ben-Ari]

Utensil Song said:

Have you tried moreverb or fancyvrb?

I learned LaTeX at least 35 years ago and haven't always kept up with new stuff (except TikZ which I love)! But I'll check out your suggestions.

[Utensil Song]

Moti Ben-Ari said:

Utensil Song said:

Have you tried moreverb or fancyvrb?

I learned LaTeX at least 35 years ago and haven't always kept up with new stuff (except TikZ which I love)! But I'll check out your suggestions.

Maybe it better for you to go with this for now. Certainly better than no highlight.