PDF, single HTML, and LaTeX versions of learning materials

Stream: lean4 dev

[xarinemm]

General idea: PDFs are useful for printing for course materials for example when not everyone has a laptop, single HTML is useful for searching across entire doc copying code, LaTeX source is useful for parsing to LLMs or just educational itself. Honestly, this should be nonnegotiable for every learning material. ArXiV does all three.

Further reasoning: building PDFs, single HTML pages, LaTeX source could all be automated without much drag on the authors. Since it does require some one-time development effort, it can't be expected out of every reader to do it themselves and duplicate the work. Some readers are not even technical enough to do it, even if it's just a few github files to be compiled, but would find these options useful if they were just a click away.

[xarinemm]

excuse my English pls

[Niels Voss]

PDF output of Verso (the lean documentation system used for the reference manual) is on the roadmap (https://lean-lang.org/fro/roadmap/1900-1-1-the-lean-fro-year-3-roadmap/) however these things take time to implement.