Recommended ways to convert Lean4 code to LaTeX?

Stream: new members

[Eduardo Ochs]

Hi all! In 2022 I published this article about a diagrammatic language for statements and proofs in Category Theory, and I left its formalization in a proof assistant as "future work"... now I am trying to work on the translation of my diagrams to Lean, but I don't know how to convert my Lean code to LaTeX to publish my notes... which tools do you recommend?

[Eduardo Ochs]

Let me try to explain a bit more. My diagrams look like this,

[Eduardo Ochs]

sshot.png

[Eduardo Ochs]

and to produce them I use heavy LaTeX trickery, including a preprocessor that understands 2D diagrams in ascii art embedded in comments and converts them to DiagXY code - for example, the source for the diagram above is here.

[Eduardo Ochs]

I sort of know how people can write Markdown code with embedded chunks of Lean code - like this...

[Eduardo Ochs]

...but how can I write LaTeX code with non-embedded Lean code, in which each chunk of Lean code is in an external file instead of being embedded?

[Eduardo Ochs]

I hope that this question makes sense! Thanks in advance...

[Shanghe Chen]

How about treating Lean files as the main source files and writing latex in the comments like https://github.com/avigad/mathematics_in_lean_source

[Shanghe Chen]

Or just add some links or anchors in the latex files and use some scripts/preprocessors to embed them when necessary?

[Eduardo Ochs]

Thanks!

I'm trying another approach... minted uses pygments, and I've just discovered that I can call pygments directly like this,

pygmentize -O full -o luatree1.lean.full.tex luatree1.lean
lualatex              luatree1.lean.full.tex

[Eduardo Ochs]

or like this:

# Extract the defs
cat luatree1.lean.full.tex | gawk '
  /makeatletter/ { out = 1 }
  out == 1       { print }
  /makeatother/  { out = 0 }
' | tee luatree1.lean.defs.tex

# Generate just a Verbatim block
pygmentize         -o luatree1.lean.mini.tex luatree1.lean

# Incomplete!

[Eric Wieser]

Note that lean4 support is not present in pygments' most recent release, though will be in the next one