HOL-Theorem-Prover
Tutorial and/or manuals on the website
The HOL Description Manual has a lot of excellent learning material, and there are also good shorter tutorials. But currently these tend to be rendered as PDFs, which are a little inaccessible, especially for newcomers who expect to be able to easily see things in a browser (especially with live content - although that's harder to implement - but at least with search). This issue is to generate a web browsable version of at least the Description manual rendered in great-looking HTML and CSS (some book/docs template maybe?). Bonus for adding any other learning or tutorial material in the same format.
I would be fine if this became the default / main sources, but the ideal would be if the existing sources could be used to generate both the website version and the PDF. Maybe there would need to be a once-off translation into markdown or something.
LaTeX is still the best option for producing high-quality PDF documents for printing purposes (I believe there are still people who print the manual and read it as a book). I think TeX4ht should be investigated.
I agree with the goal of getting nice HTML versions of the HOL docs. Right now, the doc sources are Latex. I wonder if we should port them to Markdown. My assumption is that better tooling exists for the "doc.md --> doc.{tex,html}" translation path than for "doc.tex --> doc.html", but I don't have any in-depth knowledge of the existing tool support for this stuff. The Discord conversation seems to imply that some people on the Discord are well informed, so we should take advantage of that.
On Tue, Dec 31, 2024 at 7:06 PM Chun Tian @.***> wrote:
LaTeX is still the best option for producing high-quality PDF documents for printing purposes (I believe there are still people who print the manual and read it as a book). I think TeX4ht https://tug.org/tex4ht/ should be investigated.
— Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/1380#issuecomment-2566783971, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAIOAD4KFWVBCL2BZL2CMUL2IM5PRAVCNFSM6AAAAABUNIBQU6VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDKNRWG44DGOJXGE . You are receiving this because you are subscribed to this thread.Message ID: @.***>
I have started to convert the first chapter of the description manual to markdown, from which I can then generate PDFs and HTML (see the generated system.html and system.pdf). Both outputs are fairly vanilla, but seem promising.
