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:

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.

Last updated: Sep 25 2023 at 14:01 UTC