Théo Winterhalter (Feb 13 2023 at 13:35): 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.
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.
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)
Shachar Itzhaky (Feb 25 2023 at 16:13):Oh :melting_face:
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
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