Hi, is there an instance somewhere of JSCoq that contains MetaCoq as well? Like maybe one that comes with the Platform. It seems https://coq.vercel.app/ doesn't have MetaCoq.
We have not compiled it. It can be done, but would be much easier if MetaCoq can be compiled with Dune. Then it can be easily added to coq-universe.
making MetaCoq compile with Dune is what one might describe as a challenge (just the regular build has seen quite a lot of trouble)
Actually it compiles with Dune just fine, except for an extraction problem that needs a workaorund
Oh I see, I didn't think of that.
Last updated: Jun 04 2023 at 22:30 UTC