Stream: Coq users

Topic: ✔ coq vs literate coq


view this post on Zulip Quinn (Nov 07 2021 at 19:33):

what's the difference between coq and literate coq?

view this post on Zulip 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

view this post on Zulip Quinn (Nov 07 2021 at 19:37):

software foundations "available as literate coq files", also it's all over the place in Alectryon documentation

view this post on Zulip 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]"

view this post on Zulip Karl Palmskog (Nov 07 2021 at 19:40):

also: https://en.wikipedia.org/wiki/Literate_programming

view this post on Zulip Quinn (Nov 07 2021 at 19:43):

i like executable textbooks

view this post on Zulip 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).

view this post on Zulip Notification Bot (Nov 07 2021 at 21:38):

Quinn has marked this topic as resolved.


Last updated: Feb 06 2023 at 13:03 UTC