Zulip has a code playground feature:
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