support for lean4 in latex listings package

Stream: new members

[rzeta0]

The listings package for latex enables the listing of code/programs in latex documents, and language specific support enables syntax highlighting.

https://ctan.org/pkg/listings?lang=en

Currently the upstream package doesn't have support for lean4.

Sometimes people will create the "style" file themselves.

So my question is - is anyone aware of a "listings package" style file for lean4 that I can manually place in the correct folder for it to be supported by my latex setup?

(I myself actually use lyx, not latex directly, but I don't think that makes a difference as lyx imports the standards latex package.)

[Patrick Massot]

See https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex

[Patrick Massot]

Note that there are many versions of this file floating around, where each user add a couple of tweaks. But there is no great solution, especially if you are used to relying on semantic syntax highlighting.

[Mario Carneiro]

Can we upstream this to listings itself somehow? I have 100 versions of that file in all my latex projects

[Patrick Massot]

I agree this is a real issue. But I don’t know whether there is a maximal version that would be useful for everybody.

[Mario Carneiro]

There is obviously a prototype file which is distributed and modified by users

[Mario Carneiro]

I don't think it needs to be maximal, but you can certainly approximate the basic standard language of lean4

[rzeta0]

in case it helps others...

after some hacking with Lyx on macOS and maxTex ... the following recipe seems to be working..

install lean listings style from

https://github.com/leanprover/lean4/blob/master/doc/latex/lstlean.tex

rename it to .sty and put it in

/usr/local/texlive/2024/texmf-dist/tex/latex/listings

update listings.cfg with {lstlang0.sty,lstlang1.sty,lstlang2.sty,lstlang3.sty,lstlean.sty}

then run texhash as root

then as preamble

\usepackage{color}
\definecolor{keywordcolor}{rgb}{0.7, 0.1, 0.1}   % red
\definecolor{tacticcolor}{rgb}{0.0, 0.1, 0.6}    % blue
\definecolor{commentcolor}{rgb}{0.4, 0.4, 0.4}   % grey
\definecolor{symbolcolor}{rgb}{0.0, 0.1, 0.6}    % blue
\definecolor{sortcolor}{rgb}{0.1, 0.5, 0.1}      % green
\definecolor{attributecolor}{rgb}{0.7, 0.1, 0.1} % red

[Patrick Massot]

You don’t need to do anything as root, you can simply put lstlean.tex in the same folder as your main tex file.

[rzeta0]

hi Patrick - you're right. The reason I was messing with system folders is that I was hoping to get Lyx to pick up the new language option and show it in the UI. (I use lyx files, not tex files directly).

Sadly it seems Lyx's list of languages is hardcoded and not read dynamically from the listing package style files.

[Eric Wieser]

Does Lyx have support for minted?

[rzeta0]

Eric - I don't think it does within the UI, but some people do use custom code. For me that would be too manual as I'm hoping to have lots of lean4 code examples.

For now I have a solution - the lstlean.sty file is found by Latex and my Lyx code sections have a config to override the language, so I can copy/paste those sections.

[Patrick Massot]

It may be a good opportunity to get rid of Lyx and switch to an efficient way of editing TeX files.