search

leanprover / fp-lean

Functional Programming in Lean
Other
71 stars 20 forks source link

Investigate epub via Pandoc from print.html #130

Open david-christiansen opened 1 year ago

david-christiansen commented 1 year ago

On Mastodon, it was pointed out that Pandoc is good at consuming the print HTML file and producing an epub. If this will work for making a good epub, then we might as well make it part of the standard release process.

ehamberg commented 1 year ago

I ran the following command to generate an epub from the print HTML file:

pandoc --toc --from html+smart print.html --to epub -o Functional\ Programming\ in\ Lean.epub

The +smart will convert typewriter quotation marks to proper quotation marks. It leaves code blocks alone, but for some reason, the code in exercises gets the wrong quotation marks (e.g. String.append “A” (String.append “B” “C”)).

The resulting epub file seems to be pretty good, but I'm quite sure it could be improved with a bit of work. The lack of syntax highlighting support for Lean in pandoc is a bit annoying, though, maybe the same CSS file can be used? I'm not sure.