Zulip Chat Archive

Stream: new members

Topic: support for lean4 in latex listings package


rzeta0 (Jun 04 2024 at 15:12):

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 (Jun 04 2024 at 16:38):

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

Patrick Massot (Jun 04 2024 at 16:39):

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 (Jun 04 2024 at 22:50):

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

Patrick Massot (Jun 04 2024 at 22:51):

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 (Jun 04 2024 at 22:52):

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

Mario Carneiro (Jun 04 2024 at 22:52):

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

rzeta0 (Jun 05 2024 at 02:13):

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 (Jun 05 2024 at 02:15):

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 (Jun 05 2024 at 02:22):

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 (Jun 05 2024 at 09:18):

Does Lyx have support for minted?

rzeta0 (Jun 05 2024 at 10:21):

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 (Jun 05 2024 at 12:27):

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


Last updated: May 02 2025 at 03:31 UTC