Stream: jsCoq

Topic: Instance with MetaCoq


view this post on Zulip Théo Winterhalter (Feb 13 2023 at 13:35):

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.

view this post on Zulip Shachar Itzhaky (Feb 25 2023 at 16:10):

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.

view this post on Zulip Karl Palmskog (Feb 25 2023 at 16:12):

making MetaCoq compile with Dune is what one might describe as a challenge (just the regular build has seen quite a lot of trouble)

view this post on Zulip Shachar Itzhaky (Feb 25 2023 at 16:13):

Oh :melting_face:

view this post on Zulip Emilio Jesús Gallego Arias (Feb 26 2023 at 03:12):

Actually it compiles with Dune just fine, except for an extraction problem that needs a workaorund

view this post on Zulip Théo Winterhalter (Feb 26 2023 at 08:02):

Oh I see, I didn't think of that.


Last updated: Jun 04 2023 at 22:30 UTC