Printing Lean source code

Stream: new members

[Aki Hideaki Kawai]

What is the common way to (physically) print out the lean source code? I tried "Print" extension on VSCode but syntax highlighting was not functioning. I just wanted to print out what I see on VSCode.

[Notification Bot]

This topic was moved here from #lean4 > Printing Lean source code by Kevin Buzzard.

[Kevin Buzzard]

I don't think this is really a question about Lean -- it sounds like a question about VS Code and could be asked about any programming language. Does a web search asking for printing code with syntax highlighting show up anything?

[Snir Broshi]

vscode#5953

[Snir Broshi]

The easy way is to copy-paste the code into powerpoint (or similar).
All the syntax highlighting is preserved, you just have to set the background color.

[Aki Hideaki Kawai]

Thanks for the response. I found copy-paste into TextEdit works.

[Aki Hideaki Kawai]

Sorry for the unclear wording in my original question, but I wasn’t really asking about VS Code itself. What I’m actually wondering is whether there is any Lean-community–recommended way to export or print Lean code with proper syntax highlighting.

My impression is that this may be related to the current state of Lean’s syntax-highlighting infrastructure (e.g. how parsing/highlighting is implemented in editors), but I may be mistaken.
Is there any recommended approach, or is copy-paste into rich-text editors currently the de facto solution?

[Snir Broshi]

I imagine you won't find many people interested in printing code, this sounds super niche
(however exporting code to Latex/Powerpoint/Keynote/HTML is probably a common occurrence)

[Kevin Buzzard]

When I display code blocks in talks I just take a screenshot and insert that.

[Michael Rothgang]

Do you specifically want to print source code, or quote it when you're giving a presentation? (These are different.)

[Michael Rothgang]

The easiest way to ensure perfectly matching syntax highlighting is to take a screenshot: always works, no potential for failures somewhere, but updating them as code changes is more annoying.

[Michael Rothgang]

Other ways depend on your goal: are you doing a powerpoint presentations? (No idea then; good luck.) LaTeX beamer (people have managed; I've struggled with it)? Typst (heard good things, but not tried yet). Writing a paper (then typst won't help you.)
If you tell us what you really want to do, we can answer your real question :-)

[Mirek Olšák]

For example, I wanted some basic syntax highlighting for a poster, and used this code2svg.

[Aki Hideaki Kawai]

Thanks for the suggestions.

To be more specific, I wanted review a few hundred lines of Lean code. For me, reading on paper is sometimes easier than on screen, and thus, having good syntax/semantic highlighting matters for legibility.
In that sense my question is about printing/exporting rather than presentation or publication.

I learned that copy-pasting into a rich-text editor works, which is good to know. I was just wondering whether there is any other approach people use in this situation, especially when doing this repeatedly.

[Jakub Nowak]

That sounds like a very bad idea to me tbh. You lose all the interactive feature like hover information, which for me are essential for understanding Lean code, because of type inference.

[Aki Hideaki Kawai]

That makes sense, thanks for sharing your thoughts!