Quinn (Nov 07 2021 at 19:33): Quinn (Nov 07 2021 at 19:33):what's the difference between coq and literate coq?
Karl Palmskog (Nov 07 2021 at 19:35):where did you get "literate Coq" from? Usually, it just refers to "literate programming" by Knuth applied to Coq, as in, e.g., Alectryon, see the Alectryon paper
Quinn (Nov 07 2021 at 19:37):software foundations "available as literate coq files", also it's all over the place in Alectryon documentation
Karl Palmskog (Nov 07 2021 at 19:39):I recently wrote about this distinction of books (literate vs. non-literate) in this preprint, see page 10, I call them "executable textbooks" vs. "traditional textbooks [with Coq libraries]"
Karl Palmskog (Nov 07 2021 at 19:40):also: https://en.wikipedia.org/wiki/Literate_programming
Quinn (Nov 07 2021 at 19:43):i like executable textbooks
Karl Palmskog (Nov 07 2021 at 19:46):what the Software Foundations authors mean at a low level with "literate Coq files" is that their book content is written as special comments in Coq code, and then the coqdoc tool and/or jsCoq generates HTML that interleaves code/prose which is how people usually consume the book (through their browsers).
Notification Bot (Nov 07 2021 at 21:38):Quinn has marked this topic as resolved.
Last updated: Apr 18 2024 at 09:02 UTC