Stream: MetaCoq

Topic: The META file


view this post on Zulip Enrico Tassi (Nov 26 2021 at 17:53):

Can someone explain what the META file in the template coq sub folder is for? Also, there are two mlpack files (two plugins). What are they exactly? Why only one is on the META file?

view this post on Zulip Matthieu Sozeau (Nov 30 2021 at 10:10):

I don't think we updated the META file in a while. There are two plugins indeed: the "light" template-coq reification/quotation stuff used to run MetaCoq live in Coq and the extractable version that is used for ocaml plugins (e.g. the implementations of MetaCoq Erase and MetaCoq Check link to that)

view this post on Zulip Enrico Tassi (Nov 30 2021 at 14:05):

Thanks, I found that info in a comment at some point. I'll open a PR soon, let's see if my changes to the META file are OK


Last updated: Aug 11 2022 at 02:03 UTC