Printing of LEAN4 Manuals

Stream: lean4

[Aaron Gray]

Hello, I am new to LEAN and wanting to learn to use it both for Functional Programming and also for automating existing proofs from Type Theory papers.

I want to get the books in a format and size simular to Graham Hutton's book, "Programming in Haskell".

I am wanting to print paper copies of the following main LEAN4 Manuals and need to get PDF's generated :-

https://lean-lang.org/lean4/doc/
https://lean-lang.org/theorem_proving_in_lean4/
https://lean-lang.org/functional_programming_in_lean/
https://leanprover-community.github.io/lean4-metaprogramming-book/

I have forked the sources I have found :-

https://github.com/AaronNGray/functional_programming_in_lean/tree/gh-pages
https://github.com/AaronNGray/theorem_proving_in_lean4
https://github.com/AaronNGray/lean4-metaprogramming-book

https://github.com/AaronNGray/pandoc-latex-template

I was having some GitHub Release Actions issues with getting the pandoc template zipped output built for the metaprogramming book.

The LEAN Manual seems to be in the LEAN4 Source.

Its would be nice if possible to create covers with appropriate design and LEAN Logo too.

If some one has either thought about, or done this, or can offer me advice, it would be most appreciated.

I am semi familar with TeX, i.e. I know the archetecture, although I have not really used the TeX language in anger. But not with LEAN yet obviously.

Hope you can help, and maybe interested in taking this on as a project. I am looking at a one off printers, but this might be a good project for looking at getting a larger print run and publishing done ?

Many thanks in advance,

Aaron Gray