Can/how do I use verso on the command line to generate PDFs

Stream: general

[Aaron Gray]

I am wanting a PDF version to print a version of https://github.com/leanprover/fp-lean on my printer. HTML does not seem to print very well. But also I am interested in changing the size of the result if I am able to print in PDF format ? Many thanks in advance.

[David Ledvinka]

Unfortunately a PDF feature is not currently available (see #general > Verso and the FPiL Book @ 💬)

[Joscha Mennicken]

I've had success with creating a PDF of the language reference in the past (with some CSS tweaks necessary, see #new members > Printable form of language reference? @ 💬 and https://github.com/leanprover/reference-manual/pull/527), though I haven't checked how applicable it is to FPiL.

[Joscha Mennicken]

The browser print options usually have a setting for the scale you want to print at, meaning you can fit more or less content on a single page.

[Aaron Gray]

(deleted)

[Joscha Mennicken]

I did the following for the reference:

1. Clone the repo
2. Generate the single-page HTML (for FPiL, this would be lake exe fp-lean --without-html-multi --with-html-single in the book directory)
3. Open it in Chromium (Firefox struggled to generate PDFs that large)
4. Use Chromium's print dialog to print the page to a PDF file

[David Thrane Christiansen]

@Aaron Gray Is this solved for you now?

Verso has some support for generating LaTeX, and while I don't presently have time to improve it, I'd be happy to provide support in what needs doing. FPiL has fewer fancy features than the language reference, so it'd be less work to get them all implemented in LaTeX than the reference manual.

[Aaron Gray]

David Thrane Christiansen said:

Aaron Gray Is this solved for you now?

Hi David, I am still investigating but have not tried anything as of yet. Do you mean the --with-tex option in https://github.com/leanprover/verso/blob/main/generate.sh ?

Aaron

[David Thrane Christiansen]

No, that won't work for the Lean reference manual. The issue is that each custom element included in the manual would need to have a TeX generator implemented. I was referring to the instructions above for generating a PDF via Chromium, which is not as typographically nice as TeX but perhaps solves your immediate need?