Lean to LaTeX

Stream: general

[Vasily Ilin]

I would like to copy-paste some Lean code snippets to a LaTeX file. It would be nice to keep the highlighting. Is there a LaTeX package for that?
A more general question: how does one get around the fact that LaTeX outputs a static document, while Lean is inherently interactive?

[Utensil Song]

For Q1, https://lean-lang.org/lean4/doc/syntax_highlight_in_latex.html provides 2 options.

[Vasily Ilin]

I saw this but it seems to want a whole file instead of a snippet.

[Vasily Ilin]

Er, no, I did not look closely enough

[Utensil Song]

For Q2, you can check papers about Lean for how to walk the reader through some goal states manually (most don't and focus on formalizing ideas, refering readers to the books and VSCode). Particularly, 2.1. Interactive proofs in Diagram Chasing in Interactive Theorem Proving did it for Lean 3, and I was very impressed by the way it presents Lean, and how it interweaves Math and Lean together.

But if not limited to LaTeX, there's LeanInk which annotates Lean code with type information and goal states then renders it to an interactive web page. How to prove it with Lean presents goal states with Lean code, mimicking the interactive behavior in VSCode, is also very cool (manually crafted).

There will be a new documentation tool which is introduced in 16. Documentation Authoring Tool in Lean Fro Roadmap and demonstrated in page 39 of this community meeting slide . Hopefully it would output interactive web page too.

[Lucas Viana]

If you're comfortable with emacs, there is also a package called engrave-faces that exports LaTeX code for any code snippet keeping the (active theme) highligting. Since a good part of lean's syntax is dynamic and depends on the LSP server I find it an interesting option.

https://github.com/tecosaur/engrave-faces

[Utensil Song]

Ah, it's also nice to have VSCode to support copying semantic highlighted Lean to LaTeX/Web.