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.