FPIL and TPIL with internal tables of contents?

Stream: general

[mars0i]

Apologies if this has been asked before. I didn't succeed in finding anything like it.

One of the nice things about Lean is that there are good, freely available books for learning Lean. Functional Programming in Lean has been very helpful to me, and I've started reading Theorem Proving in Lean as well.

I find it helpful to annotate books I read--highlighting or commenting on parts. I see that there are tools for annotating web pages, but I'm not sure I trust them. On the other hand, I'm very used to annotating PDFs (in iAnnotate, but there are probably better tools), and it's easy for me to create PDFs of the books using the Print icon.

The problem for me is that the table of contents for these books is in a part of the web UI that's not included in what gets printed, so I end up with a PDF with no table of contents--not in the text, and not in the separate table of contents information that some PDFs include. Hundreds of pages with no table of contents is not very useful.

I'm wondering how easy it would be to at least add a table of contents page within the text of FPIL and TPIL. (This seems simpler than generating an extra table of contents structure that appears in a PDF's separate contents window.) Ideally, the table of contents would provide links to the chapters or sections listed, but even a dead table of contents would be useful. (TPIL at least, contains a few crosslinks within some paragraphs, to other parts of the book. However, in the PDF, they are links to the web version rather than to other places in the PDF.)

I know that an intended use of these books is with a Lean-enabled editor handy, and I use the books that way, too. But I like reading a on tablets and I don't need to try out every code sample. (There must be others like me.)

(Mathematics in Lean does generate PDFs with a table of contents page, including links to the chapters and sections.)

[Patrick Massot]

The whole pipeline generating Lean documentation is being completely reworked by @David Thrane Christiansen so nothing will change very soon but I’m sure he will note this request and this will be fixed in a couple of months.

[mars0i]

Ah--excellent. Thanks @Patrick Massot, and @David Thrane Christiansen.

[David Thrane Christiansen]

Glad you are getting value from FPiL! PDF (via TeX) and epub output are planned as important components of the new docs tool. Once we port the content, I'd appreciate feedback - supporting your use case and e-readers is important.

[mars0i]

(deleted)

[Shanghe Chen]

tpil4.pdf

tpil4.epub

fpil.epub

fpil.pdf

[Shanghe Chen]

Hi I converted tpil4 and fpil to pdf and epub for temporary usage, using https://github.com/LegNeato/mdbook-typst and https://github.com/Michael-F-Bryan/mdbook-epub. It does not work 100 percent right but does contain some internal outlines:tada:

[Shanghe Chen]

Btw the lean version in the source repo for fpil seems 4.1.0 and a little old?