syntax highlight of Lean4 in Zola

Stream: new members

[Asei Inoue]

I want to enable syntax highlighting of lean4 in zola (static site generator written by rust).
so I create a .sublime-syntax file (copied from https://gist.github.com/Julian/062e5ae6a6a5edfea23f8c89a7ff5d41. Thank you, Julian)

https://github.com/lean-ja/lean-sublime-syntax

[Asei Inoue]

But this file is outdated, so I will update this file for lean4.

[Asei Inoue]

Does the lean prover community not need a sublime-syntax file for lean? Has anyone already created a sublime-syntax file for latest lean4?

[Eric Wieser]

Isn't sublime-syntax pretty much the same as tmLanguage? In which case, it's only a small transformation away from the standard highlighter

[Asei Inoue]

what is tmLanguage? Is it possible to generate sublime-syntax file from tmLanguage?
If so, that sounds nice.

[Eric Wieser]

tmLanguage is the ancestor of both vscode and sublime text's syntax format. The standard highlighter I'm referring to is this one.

[Asei Inoue]

ok i will edit my sublime-syntax file based on https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/syntaxes/lean4.json

[Asei Inoue]

@Eric Wieser Thank you!

[Eric Wieser]

I think you can just rename it to tmLanguage.json, and there is a sublimtext extension to convert it to a .tmLanguage (edit: https://stackoverflow.com/a/61286113/102441 edit edit: https://github.com/SublimeText/PackageDev)

[Eric Wieser]

(and sublime text knows how to use .tmLanguage natively)

[Asei Inoue]

I want to enable syntax highlight of lean4 in website built by Zola, not sublime text.
Zola recognizes tmLanguage...?

[Eric Wieser]

I would guess that PackageDev also knows how to convert tmLanguage to sublime-syntax

[Eric Wieser]

From the Zola documentation:

Zola only works with syntaxes in the .sublime-syntax format. If your syntax
is in .tmLanguage format, open it in Sublime Text and convert it to sublime-syntax by clicking on
Tools > Developer > New Syntax from ... and put it in the sublime/syntaxes directory.