Is there a downloadable PDF version of the reference manual?

[euprunin]

Is there a downloadable PDF version of the reference manual?

If not, what’s the recommended way to generate one?

[david-christiansen]

There is no downloadable PDF right now.

I don't have a good way to generate one, I'm afraid. Verso can be made to support generating LaTeX, but the current infrastructure has not been built with this in mind and each extension used in documentation would need to have a LaTeX backend added, so it'd be a fair bit of work.

For proofreading, I used to generate a single-page HTML file and then print it to PDF. Unfortunately, the file got large enough that neither Chrome nor Firefox would reliably generate a PDF for me, so I stopped doing it.

What do you want to use the PDF for? For some use cases, something based on smaller HTML files might work well enough.

[euprunin]

A similar request:

https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Printable.20form.20of.20language.20reference.3F/with/520532042

[euprunin]

@david-christiansen I’d also like to print the manual.

I'm comfortable using the command line—what's the recommended way to generate a single-page HTML file of the reference manual?

[david-christiansen]

lake exe generate-manual --with-html-single should do the trick. Be warned: it's big, and the navigation features are really designed for the multi-page mode. I can't make any browser on my system reliably produce a PDF from it (but I'd merge the PR that did, all else equal)

[euprunin]

Thanks!

This is the best result I've achieved so far:

% lake exe generate-manual --with-html-single
% pandoc _out/html-single/index.html -o reference.pdf --pdf-engine=lualatex

It generates a PDF with 1 591 pages which appears to be complete.

[euprunin]

Some warnings are emitted during the PDF generation process. I'm not sure what impact they have or whether they can be avoided.

Missing character warnings:

7098 [WARNING] Missing character: There is no α (U+03B1) (U+03B1) in font [lmmono10-regular]:!
2313 [WARNING] Missing character: There is no 🔗 (U+1F517) (U+1F517) in font [lmroman10-regular]:+tlig;
1799 [WARNING] Missing character: There is no β (U+03B2) (U+03B2) in font [lmmono10-regular]:!
 830 [WARNING] Missing character: There is no ✝ (U+271D) (U+271D) in font [lmroman10-regular]:+tlig;!
 518 [WARNING] Missing character: There is no ⊢ (U+22A2) (U+22A2) in font [lmroman10-regular]:+tlig;!

Label warnings:

  19 [WARNING] [makePDF] LaTeX Warning: Label `C1___Monoid___ident_right' multiply
  13 [WARNING] [makePDF] LaTeX Warning: Label `S___ptr_2' multiply defined.
   7 [WARNING] [makePDF] LaTeX Warning: Label `Weekday___sa' multiply defined.
   7 [WARNING] [makePDF] LaTeX Warning: Label `RunsMatch' multiply defined.
   7 [WARNING] [makePDF] LaTeX Warning: Label `Exp___app' multiply defined.

Reference warnings:

   1 [WARNING] [makePDF] LaTeX Warning: Hyper reference `lake-option--log-level' on
   1 [WARNING] [makePDF] LaTeX Warning: Hyper reference `lake-flag--verbose' on page
   1 [WARNING] [makePDF] LaTeX Warning: Hyper reference `lake-flag--try-cache' on
   1 [WARNING] [makePDF] LaTeX Warning: Hyper reference `lake-flag--reconfigure' on
   1 [WARNING] [makePDF] LaTeX Warning: Hyper reference `lake-flag--quiet' on page

[Garmelon]

In my experiments for #527, Chromium reliably produced a usable PDF from the single-page manual while the PDF produced by Firefox was broken. Not sure why, or if Chromium will break if the content or style changes.

[I-Al-Istannen]

The Firefox-generated PDF can be repaired with mutool clean "The Lean Language Reference.pdf" out.pdf, but that sounds like a Firefox bug.