Stream: jsCoq

Topic: Zulip code playgrounds


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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