browser-only syntax highlighting

Stream: general

[Utensil Song]

I needed a browser-only syntax highlighting solution for Lean 4 a few days ago. I've chosen shiki because it can reuse themes and language syntaxes from VSCode. I want to reuse my favorite theme from VSCode (Railscasts Renewed), and most highlighting js libraries don't support highlighting Lean 4, e.g. highlight.js, prism.js, code mirror (these are links to add a new language to them).

So I would like to share my (quite simple) solution in case anyone needs it too, besides the syntax highligting solution for LaTeX based on minted and pygments.

The script is here, it could be simplified if one only wishes to use bundled themes, or one deploys the VSCode Lean syntax json like it's bundled. There's also a bit of light/dark theme switch code that needs adaption for the switch mechanism in use.

To use the sciprt, add the following to your html:

<script type="module" src="shiki.js"></script>

It looks like this in dark theme (test page):

image.png

[Utensil Song]

There are a few potential improvements though:

1. single line comments that doesn't start at the beginning of a line are not highlighted:

image.png

2. some tricky syntax is not handled:

image.png

These issue don't show up in VS Code probably due to semantic highlighting.

[Utensil Song]

@Marc Huisinga Can you help evaluating if these syntax json files will accept PRs to fix these issues, or are they non-issue because LSP will fix them with semantic highlighting? Thanks, no hurry, I can see that you are in vocation. :palm_tree:

[Marc Huisinga]

Issue 1. is not an issue in VS Code when you disable semantic highlighting using the 'Editor > Semantic Highlighting: Enabled' setting. In fact, we do not use the comment semantic token kind at all, so all comment highlighting you see is provided by the editor.

I can confirm that issue 2. is reproducible in VS Code. I'm happy to accept PRs to the TextMate Lean 4 syntax highlighting as long as it's not excessively tricky to make the adjustment; the regexes in the grammar shouldn't get too messy and there shouldn't be lots of additional edge cases introduced by a change. Searching Mathlib with the regexes that you are trying to implement can be helpful in this regard.

[Utensil Song]

Thanks, then I suspect issue 1 could be caused by shiki instead. I'll take a look into them. As for regex, hopefully it's not going to be messy as @Eric Wieser 's pygments lexer has already handled this case, and we just need to port it from there.

[Eric Wieser]

There is already highlight.js support for lean3, in a package in the leanprover-community organization

[Eric Wieser]

I have a lean 4 version somewhere that I should upload somewhere central

[Utensil Song]

Eric Wieser said:

There is already highlight.js support for lean3, in a package in the leanprover-community organization

Yeah, I know about that one, but it looked obsolete. So I thought, the VS Code syntax file is certainly going to be maintained. Then I found shiki to consume it.

[Patrick Massot]

What would be really really useful would be a way to export semantic syntax highlighting information. It is currently extremely painful to write a paper showing Lean code.

[Eric Wieser]

It is currently extremely painful to write a paper showing Lean code

I think this is no longer true on bleeding edge versions of things; minted now works out of the box, and LuaLaTeX can load JuliaMono without much difficulty

[Eric Wieser]

Of course the export would give better highlighting

[Patrick Massot]

The new version of minted would not do semantic syntax highlighting, right?

[Eric Wieser]

Correct, but it does the same syntax higlihting as Zulip at least