Théo Zimmermann (Jul 03 2022 at 16:37): Théo Zimmermann (Jul 03 2022 at 16:37):Zulip has a code playground feature:
image.png
I wonder if we could activate it using jsCoq. All we would need is a way to pass a code to jsCoq's scratchpad as a URL argument. Is this already supported? Would it be easy to add?
Emilio Jesús Gallego Arias (Jul 03 2022 at 16:57):That would be easy to add I think, maybe indeed we even support it.
Shachar Itzhaky (Jul 03 2022 at 17:03):Oh interesting. We do not support it but what is the API? does it just open this URL in a separate tab? So it does not need to have any particular format of the page it is redirecting the request to.
Shachar Itzhaky (Jul 03 2022 at 17:57):actually I am perplexed. Even when the META.coq-equations is there, running coqdep fails with *** Error: in file Loader.v, could not find META.coq-equations.. Still, compiling with -j1 succeeds while compiling multiprocess fails.
Last updated: Jan 31 2023 at 11:01 UTC