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?
That would be easy to add I think, maybe indeed we even support it.
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.
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