Semantic highlighting export

Stream: lean4

[Patrick Massot]

Does anyone know a way to somehow export semantic highlighting to LaTeX? I recently wrote a paper where all code snippets are ugly compared to what I see in VSCode or vim because they make crucial use of semantic highlighting. If no easy solution exist, I will probably have to use screenshots in the final version…

[Utensil Song]

Maybe in the similar spirit of https://stu.dev/using-vs-code-for-my-blog-code-formatting/ or https://marketplace.visualstudio.com/items?itemName=pdconsec.vscode-print .

The idea underneath is that VSCode has rendered the code to HTML and it's just one step away from getting the HTML to SVG, PDF etc.

[Utensil Song]

Also note that the default copy action in VS Code is the same as the command "Copy With Syntax Highlighting". That means one can copy and paste highlighted code into a rich text editor like Word or a Web based one, then save it as PDF, without any extra technical support. I had done this before on Win/Mac, Linux should also have good support for rich text copy-paste.

[Siddhartha Gadgil]

Some level of highlighting is done in the listings package, for example this paper but I don't know if that is good enough.

[Mario Carneiro]

The lstlean.tex file in lean4 repo is ancient (I used it anyway), it's got stuff from lean 2 in it

[Eric Wieser]

Hopefully pygments will do a release soon, then lean4 will be supported by default with minted

[Utensil Song]

Eric Wieser said:

Hopefully pygments will do a release soon, then lean4 will be supported by default with minted

As long as Lean LSP is not involved, there can't be semantic highlighting in such workflows, particularly for metaprogramming-rich Lean code.

[Utensil Song]

My (mid-term) bet is on Verso, it has access to Lean environment, supports multiple output format (which could be a series of tex or directly small PDF images for the consumption of LaTeX and the main TeX file can simplely reference them by IDs), it only needs be able to interface with existing themes for other highlighters like the one used by VSCode.

[David Thrane Christiansen]

The subverso library is what Verso uses for subprocesses in different Lean versions. It's supposed to be a tool for querying compiler metadata that maintains compatibility with a variety of Lean versions (specific policies TBD). It includes a step that exports marked examples to a JSON format, and a Lean library that parses this. I don't yet have a TeX tenderer for it (only HTML), but it could be a reasonable easy starting point to build proper TeX output.

To use it, add a dependency on the library and then run lake build :examples. That'll get you JSON files.

This function will go ahead and build the JSON for a Lean project, then parse it into a more convenient datatype. A command-line wrapper for this that then emits TeX should be fairly easy to write.

Warning: this is rapidly evolving software. I won't yet be able to support many external users, but I hope it will settle down and stably support many Lean versions in the future.