Julin S (Dec 30 2021 at 06:11): Julin S (Dec 30 2021 at 06:11):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 *)
saying
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.
Julin S (Dec 30 2021 at 06:31):I seem to be missing many things.
Check constructor_body.
says The reference constructor_body was not found in the current environment. as error too.
Yannick Forster (Dec 30 2021 at 06:33):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
Julin S (Dec 30 2021 at 06:47):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?
Yannick Forster (Dec 30 2021 at 09:44):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
Julin S (Dec 30 2021 at 10:09):Thanks!
Used the version at here and it worked.
Notification Bot (Dec 30 2021 at 10:09):Ju-sh has marked this topic as resolved.
Julin S (Dec 30 2021 at 10:18):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?
Yannick Forster (Dec 30 2021 at 10:36):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: May 31 2023 at 02:31 UTC