Stream: MetaCoq

Topic: plugins in MetaCoq vs. ML

Karl Palmskog (Dec 26 2022 at 23:40):

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?

Théo Winterhalter (Dec 27 2022 at 10:06):

Is it supposed to be safer? Or is it rather more convenient as it should offer a more stable API?

Karl Palmskog (Dec 27 2022 at 10:49):

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?

Théo Winterhalter (Dec 27 2022 at 11:11):

Ah yes indeed.

Last updated: Jun 03 2023 at 15:31 UTC