in this Coq PR, we discuss(ed) the difference between library and plugin, and broke down plugin into at least MetaCoq-based plugin and raw ML plugin (there's also Elpi, etc.).
Can one say something definite about how much safer MetaCoq-based extensions (that add new vernacular commands or tactics, etc.) are than OCaml hacking? Could all the ML parts of MetaCoq in principle be upstreamed into Coq itself so we could get the whole TCB of Coq+MetaCoq into the Coq repo?
Is it supposed to be safer? Or is it rather more convenient as it should offer a more stable API?
but the API is also much smaller, no? A stable, smaller API vs. a bigger ever-changing one seems like obviously less prone to unsafe code (in the sense of bugs, crashes, reliability, trustworthiness, etc.)
Aren't the ML parts of MetaCoq basically confined to Template Coq?
Ah yes indeed.
Last updated: Jun 03 2023 at 15:31 UTC