KDE syntax highlighting definition for Lean?

Stream: general

[Ryan Lahfa]

Hello, I'm writing some Beamer presentation using pandoc and wondered if there was any KDE syntax highlighting file (https://github.com/KDE/syntax-highlighting/tree/master/data/syntax) for Lean, apparently, not ; but I'm pretty sure that Pygments support Lean as a target, because minted support Lean.
Does anyone how hard would it be to write one for Lean?

[Bhavik Mehta]

You could probably adapt one from https://github.com/leanprover/vscode-lean/blob/master/syntaxes/lean.json and/or https://github.com/leanprover/lean/blob/master/extras/latex/lstlean.tex

[Ryan Lahfa]

Makes sense, I think the JSON looks easier to port, but it would require my full concentration to do this kind of stuff w/o errors

[Bryan Gin-ge Chen]

The master branch of pygments has a decent lexer for Lean. I'm hoping they'll cut a release soon so that we can get Zulip's syntax highlighting fixed and also start adding syntax highlighting to the docs and website.

[Hagb (Junyu Guo)]

I just wrote a KDE syntax highlighting file for Lean(4), which was ported from the existing pygments highlighting file for Lean4 and VSCode highlighting file for Lean4.
https://gist.github.com/Hagb/df9044a81525aff0f6b44f4fae3270c0
highlight.png, and hardcoded some frequently used tactics to highlight them without semantic highlighting.
It can be used by Kate, pandoc and so on to highlight the Lean code. The following picture is captured from the html file generated with Breeze Light theme.

[Bulhwi Cha]

Thanks! I'll try it with Kate.

[Miguel Marco]

Would it work for lean3 too?

[Hagb (Junyu Guo)]

Miguel Marco said:

Would it work for lean3 too?

Maybe not totally working. But I think that the availability for Lean3 is close to the availability for Lean4. (Maybe I should improve it after referring to the existing highlight file for Lean3.)
I just found that begin was not highlighted. And after trying to highlight the tutorials, I found that there were still some frequently-used tactics missing.
Now the highlighting file is updated with begin keyword and more tactics. (In fact, I don't know whether it is a good idea to hardcode the tactics. I am trying to make the highlight look like VSCode's, where the highlighting for tactics is semantic but not hardcoded.)

[Miguel Marco]

Thanks, it might be very helpful!

Related to this, I think another interesting thing to have is a way to run lean in jupyterlab.

[Malvin Gattinger]

Thanks for this! Just leaving as a note for others unsure how to use the .xml file with Lean, this page explains where to copy it: https://docs.kde.org/stable5/en/kate/katepart/highlight.html

[Julian Berman]

In case it's helpful, the Pygments definitions were slightly improved by @Eric Wieser while upstreaming them to Pygments. You can find that here now: https://github.com/pygments/pygments/blob/c094455b4aa518909b0a93fffd2b516421750923/pygments/lexers/lean.py#L135

[Eric Wieser]

In particular, the commit logs for that file show the changes applied on top of the old version in the Lean 4 repo

[Kevin Cheung]

Hagb (Junyu Guo) said:

I just wrote a KDE syntax highlighting file for Lean(4), which was ported from the existing pygments highlighting file for Lean4 and VSCode highlighting file for Lean4.
https://gist.github.com/Hagb/df9044a81525aff0f6b44f4fae3270c0
highlight.png, and hardcoded some frequently used tactics to highlight them without semantic highlighting.
It can be used by Kate, pandoc and so on to highlight the Lean code. The following picture is captured from the html file generated with Breeze Light theme.

Is there a repository hosting this KDE syntax highlighting file for Lean 4 that can be used in pandoc?

[Malvin Gattinger]

I just learned that a gist is also repository. Writing this into test.md:

~~~lean
def test := sorry
~~~

And then running this:

git clone https://gist.github.com/df9044a81525aff0f6b44f4fae3270c0.git
pandoc --standalone --syntax-definition df9044a81525aff0f6b44f4fae3270c0/lean.xml test.md -o test.html
firefox test.html

seems to work :-)

[Kevin Cheung]

Works great! Thank you!