Lean code for Arxiv

Stream: general

[Vasily Ilin]

Hi. What is the recommended way to format Lean code to post on Arxiv? I am currently using listings with pdfLatex. Even though the pdf looks fine, it produces errors that prevent the arxiv submission.

[Johannes Tantow]

Vasily Ilin schrieb:

it produces errors that prevent the arxiv submission

You might want to be more concrete if you want help.

Are you aware of the following: https://github.com/leanprover-community/lean/blob/master/extras/latex/lstlean.md

[Martin Dvořák]

This is how we do it:
https://github.com/Ivan-Sergeyev/seymour/blob/cdeb84d60eb068d902ae2ad4c48e982d1618bf71/paper/src/00%20preamble.tex#L50

[Kevin Buzzard]

I encourage the use of minted with my students; here's something one of them wrote.
minted.pdf But I cannot comment on compatibility with ArXiv; my understanding is that ArXiv uses archaic technology and that the easiest way to get around it is just to upload the pdf and not the LaTeX.

[Martin Dvořák]

Will arXiv accept a PDF generated from a LaTeX source?

[Eric Wieser]

If you email them explaining that you can't use pdflatex because it is dumb, supposedly yes

[Eric Wieser]

Otherwise you can rename all the fonts in the PDF to thwart their detection

[Michael Rothgang]

Martin Dvořák said:

This is how we do it:
https://github.com/Ivan-Sergeyev/seymour/blob/cdeb84d60eb068d902ae2ad4c48e982d1618bf71/paper/src/00%20preamble.tex#L50

Does that enable you to avoid the --shell-escape flag for minted? My understanding is that this is not compatible with the way the arXiv works at the moment.

[Martin Dvořák]

I don't know! I haven't tried submitting it to arXiv yet.

What I did last time and what worked on arXiv perfectly is this
https://github.com/madvorak/duality/blob/db8a785db20438eb379d8fe5a423e5e07469a707/nonLean/duality.tex#L61
where minted isn't used.

[Eric Wieser]

Does that enable you to avoid the --shell-escape flag for minted? My understanding is that this is not compatible with the way the arXiv works at the moment.

The way you're supposed to submit things with minted is to use the finalize-cache and frozen-cache options