Lean code in .md file

Stream: general

[Flo (Florent Schaffhauser)]

On Zulip, Lean code is highlighted:

example : 1 + 1 = 2 := by rfl

If I input the code block corresponding to the above in a markdown file

```lean
example : 1 + 1 = 2 := by rfl
```

then the rendering depends on the viewer.

I get something nice if I upload the .md file to GitHub and then access it via my browser, but typically not as nice if I use markdown preview in VS Code, even with an extension like bierner.markdown-preview-github-styles.

Is there a way to get more colourful highlighting of lean code when displayed in a .md file?

[Joscha Mennicken]

Whether code is syntax highlighted depends on whether the markdown viewer knows the language. The markdown format does not specify which languages exist, so it is up to the viewer which languages to support.

Since markdown files allow embedding HTML, you could probably generate highlighted HTML with a tool like pygments which lists Lean as a supported language though it does not mention whether this is lean 3 or 4.

[Eric Wieser]

I think the problem here is https://github.com/microsoft/vscode/issues/91279

[Eric Wieser]

merging https://github.com/highlightjs/highlight.js/pull/1689 would fix this, but it was rejected

[Utensil Song]

This is an issue of VS Code Markdown Preview. It doesn't support highlighting Lean.

Look how nice it highlights Lean in markdown editor but not in preview:

image.png

The issue @Eric Wieser posted is probably only part of the cause. To make it obvious, install bierner.markdown-shiki as suggested in the issue, see how other languages become fancier but Lean stays the same:

image.png

[Eric Wieser]

Specifically, VS Code Markdown Preview uses highlight.js (with no plugins), and highlight.js does not accept PRs adding new languages. This also means that highlighting doesn't work on Gitter and Discord, and there's nothing we can do about it other than complain more loudly.

[Eric Wieser]

It might be possible to inject our highlight.js language support from within a vscode extension, but it's not clear how to do so

[Utensil Song]

bierner.markdown-shiki changes highlight.js to shiki, which still doesn't support Lean but at least it's extensible.

[Eric Rodriguez]

I can see why highlight.js doesn't want to add more languages, but I think there should be pressure to make downstream users such as discord and vscode to be able to add languages manually

[Eric Rodriguez]

I guess it's a huge security risk though because it could be used to instead allow the installation of some virus

[Flo (Florent Schaffhauser)]

Eric Wieser said:

It might be possible to inject our highlight.js language support from within a vscode extension, but it's not clear how to do so

That would quite nice, yes :smile: