I was trying to run the example to add a new constructor to an inductive type with template-coq as given in the metacoq repo.
But I got an error in the beginning itself.
From MetaCoq.Template Require Import utils All. Import MCMonadNotation. (* Error here *)
Cannot find module MCMonadNotation
Is it something that needs to be installed separately?
Not sure if it matters, but I've got coq-ext-lib installed.
I seem to be missing many things.
The reference constructor_body was not found in the current environment. as error too.
What version of MetaCoq are you using? If you are using the latest version available via opam, this will not match the files available on the latest versions of the github branches. You either have to use an older version of add_constructor or a newer MetaCoq version
Yeah, I just installed from opam. Hadn't even realized they were beta versions.
I'm on Coq 8.12.2 and has the following packages:
coq-metacoq 1.0~beta1+8.12 coq-metacoq-checker 1.0~beta1+8.12 coq-metacoq-erasure 1.0~beta1+8.12 coq-metacoq-pcuic 1.0~beta1+8.12 coq-metacoq-safechecker 1.0~beta1+8.12 coq-metacoq-template 1.0~beta1+8.12 coq-metacoq-translations 1.0~beta1+8.12
What can I do make the example work? Should I upgrade/downgrade versions? Or can I just change some syntax and get away with it?
You can keep the version and just use the corresponding version of add_constructor. You will find it in the zip file corresponding to the beta1 release for 8.12, on the right hand side of the github page of MetaCoq
Used the version at here and it worked.
Ju-sh has marked this topic as resolved.
Is the syntax used for metacoq and template-coq not fixed yet? Would converting stuff written for the current version to a later version take lot of effort?
There are mostly just minor differences between the versions. The issue you ran into was that a notation module was renamed to avoid clashes with another module in coq-ext-lib with the exactly same name. Porting just means prefixing MonadNotation by MC. There are other mostly minor changes which don't require a lot of work when porting. On the 8.13 and 8.14 branches, there is one bigger change: following a change in Coq's kernel, the representation of tCase changed. The porting time here can differ depending on the project, but all projects I am involved in which just use MetaCoq as a meta-programming tool without proving properties were easy to port
Last updated: Feb 09 2023 at 02:02 UTC