LaTeX Syntax rendering

Stream: new members

[Simon Daniel]

Hello,
i try to render Lean code in LaTex.
i followed the instructions from the Manual but both options did not work for me.
When using listings some none ASCII Characters are rendered displaced for some reason.

And my Minted version is 2.7, i copied the first answer from this issue but lualatex fails to build it.

[Simon Daniel]

lean_syntax.png
this how a listings render the follwing code for me

\begin{lstlisting}[language=lean]
variable {μ: Type}
\end{lstlisting}

[Eric Wieser]

Based on https://github.com/pygments/pygments/milestones, I think if you wait a few days then lean4 support might be native to pygments

[Eric Wieser]

Of course, I thought this in january which is when their previous release was scheduled for, which never happened...

[Eric Wieser]

i copied the first answer from this issue but lualatex fails to build it.

I was able to get @Tobias Grosser's approach here to work with LuaLatex for my thesis

[Eric Wieser]

What I had there is

% from https://github.com/opencompl/paper-template/commit/b71adc99c0784ba69d8f73ec3338c3d410dc0e6b
\makeatletter
    \ifcsdef{minted@optlistcl@quote}
    {
    \ifwindows
    \renewcommand{\minted@optlistcl@quote}[2]{%
        \ifstrempty{#2}{\detokenize{#1}}{\detokenize{#1="#2"}}}
    \else
    \renewcommand{\minted@optlistcl@quote}[2]{%
        \ifstrempty{#2}{\detokenize{#1}}{\detokenize{#1='#2'}}}
    \fi

    % similar to \minted@def@optcl@switch
    \newcommand{\minted@def@optcl@novalue}[2]{%
    \define@booleankey{minted@opt@g}{#1}%
        {\minted@addto@optlistcl{\minted@optlistcl@g}{#2}{}%
        \@namedef{minted@opt@g:#1}{true}}
        {\@namedef{minted@opt@g:#1}{false}}
    \define@booleankey{minted@opt@g@i}{#1}%
        {\minted@addto@optlistcl{\minted@optlistcl@g@i}{#2}{}%
        \@namedef{minted@opt@g@i:#1}{true}}
        {\@namedef{minted@opt@g@i:#1}{false}}
    \define@booleankey{minted@opt@lang}{#1}%
        {\minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang}{#2}{}%
        \@namedef{minted@opt@lang\minted@lang:#1}{true}}
        {\@namedef{minted@opt@lang\minted@lang:#1}{false}}
    \define@booleankey{minted@opt@lang@i}{#1}%
        {\minted@addto@optlistcl@lang{minted@optlistcl@lang\minted@lang @i}{#2}{}%
        \@namedef{minted@opt@lang\minted@lang @i:#1}{true}}
        {\@namedef{minted@opt@lang\minted@lang @i:#1}{false}}
    \define@booleankey{minted@opt@cmd}{#1}%
        {\minted@addto@optlistcl{\minted@optlistcl@cmd}{#2}{}%
            \@namedef{minted@opt@cmd:#1}{true}}
        {\@namedef{minted@opt@cmd:#1}{false}}
    }
    \minted@def@optcl@novalue{customlexer}{-x}
    }
    {
    }
\makeatother

[Simon Daniel]

im confused to how even use this code. should i add it to my preamble after the minted import?
My thesis is due to this month so i probably cant wait for the native Lean support.

[Eric Wieser]

Sorry, I'm afraid I missed your message @Simon Daniel. If it's not too late, pygments just released a version with native lean4 support.

[Simon Daniel]

no worries, i worked out a half decent looking solution. Ill have a look into the pygments release if I need latex support in the future

[Utensil Song]

I have just given minted and pygments another try.

My preamble:

% I have the following to adjust outputdir and cachedir but in general they are not needed
% \usepackage[outputdir=../print,cachedir=_minted-cache]{minted}
\usepackage{minted}

\setminted{
  fontsize=\footnotesize,
  frame=single,
  breaklines
}

Code block:

    \begin{minted}[autogobble,mathescape]{lean4}
        /--
            Let $K$ be a division ring, a module $V$ over $K$ is a vector space
            where being a module requires $V$ to be a commutative group over $+$.
        -/
        variable [DivisionRing K] [AddCommGroup V] [Module K V]
    \end{minted}

Inline code:

\mintinline{lean4}{Algebra.toRingHom r}

It seems ok, except that mathescape is not working like lstlisting as claimed in minted documentation.

Here is lstlisting output:

image.png

While minted gives:

image.png

but mathescape actually works for Python:

image.png

[Utensil Song]

Another side note is that usually when publishing, one has no control over the Python environment or the pygments version of the publisher, released or not. One could just use the master version of pygments locally, then submit using \usepackage[frozencache,cachedir=_minted-cache]{minted}.

[Jireh Loreaux]

@Utensil Song , I haven't tested it, but I think you want the option texcomments instead of mathescape. The former is for escaping to LaTeX within the code itself, the latter is for escaping to LaTeX in comments.

[Utensil Song]

Thanks, they are for different purposes, mathescape has less side-effect IIUC.

I've pushed a fix following the C/C++ lexer. When using pygments @ git+https://github.com/utensil/pygments.git@lean4_mathescape, mathescape works as expected.

[Eric Wieser]

I thought mathescape was the more aggressive option, and will mess up $ symbols in syntax antiquotations?

[Eric Wieser]

(https://github.com/utensil/pygments/tree/lean4_mathescape for reference)

[Eric Wieser]

That patch looks strange to me; and it breaks nested comments

[Utensil Song]

Actually, the patch is mostly unnecessary, no need to change the lexer nor add __init__ it seems, they are byproducts of figuring out the problem.

The only actual effect is to treat doc strings as comments so that these options about comments will work. Alternatively, I can just use /- comments instead of /--.

And thanks for the heads-up and explanation, it seems that I should change to texcomments after all.