Getting Lean highlighting and proof state for a blog

Stream: general

[l1mey]

I have an existing blog implemented using pandoc, with a lot of functionality implemented using Lua. Pandoc doesn't currently support Lean highlighting, but I'm looking to find a way to get syntax highlighting, types, and (possibly) proof state as per verso.

Is there a low level library I can use to feed it Lean code and have it return to me the HTML code? This can be easily automated and put as a Lua script in Pandoc.

[l1mey]

What I am seeing right now is the subverso library and subverso-extract-mod, but to get HTML it seems I'll need to hook into the verso library.

[Henrik Böving]

Why would you not just use verso directly?

[l1mey]

It doesn't seem there is a nice way to use it without basing my entire website around verso, I just want to use it for short code snippets that I can get HTML to inject into my website using some Lua scripts in pandoc.

[l1mey]

I don't want to pull in the entirety of verso, just enough to get some HTML out.

[Hagb (Junyu Guo)]

l1mey said:

I have an existing blog implemented using pandoc, with a lot of functionality implemented using Lua. Pandoc doesn't currently support Lean highlighting, but I'm looking to find a way to get syntax highlighting, types, and (possibly) proof state as per verso.

Is there a low level library I can use to feed it Lean code and have it return to me the HTML code? This can be easily automated and put as a Lua script in Pandoc.

There's a KDE syntax definition for Lean, which can be used by pandoc to support highlighting Lean: #general > KDE syntax highlighting definition for Lean? @ 💬