Stream: MetaCoq

Topic: Example plugins with metacoq


view this post on Zulip Julin Shaji (Feb 10 2024 at 05:25):

Hi.

Are there any example plugins made with the help of metacoq that we can look up?

If we want to make new vernacular commands in a plugin, can metacoq by itself do it?
Or do we still need some degree of ocaml for that?

view this post on Zulip Julin Shaji (Feb 10 2024 at 05:58):

Or is having separate vernacular commands irrelevant if metacoq is used?

view this post on Zulip Matthieu Sozeau (Feb 11 2024 at 05:23):

You can run plug-ins using MetaCoq Run, but if you extract your plugin to OCaml and want to use that code you will have to define a wrapper OCaml and .mlg file that defines a vernacular grammar extension as for any other OCaml plugin.

view this post on Zulip Matthieu Sozeau (Feb 11 2024 at 05:25):

That is what is done for the MetaCoq Erase and MetaCoq Check plug-ins. See safechecker-plug-in and erasure-plugin folders in MetaCoq’s source for examples. The translations/ folder has more traditional plug-ins that we run only using MetaCoq Run.


Last updated: Jul 23 2024 at 21:01 UTC