Please create a tag for the version of MetaCoq that CertiCoq can depend on

MetaCoq / metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

https://metacoq.github.io

MIT License

367 stars 79 forks source link

Please create a tag for the version of MetaCoq that CertiCoq can depend on #1062

Closed liyishuai closed 5 months ago

liyishuai commented 5 months ago

CertiCoq currently depends on 98b0360169ba1dbc54f92ef50abd4c9dea7dfdc4, and does not compile with the coq-8.17 branch. Please create a tag for this version, for the convenience of tracking CertiCoq on OPAM extra-dev.

mattam82 commented 5 months ago

The dev versions are still very much moving and are quite tightly coupled, so I don't think we want the certicoq extra-dev package to point to an opam package for metacoq yet but rather use the metacoq submodule in certicoq. However, I'll make a release of certicoq working with metacoq 1.3.1+8.18 and 1.3.1+8.19 at least this week.