Stream: jsCoq

Topic: Javascript Access


view this post on Zulip Aadith C (May 10 2021 at 20:45):

Hi, new JsCoq user here. While working on a project that requires integrating JsCoq with a Geometry visualization software, I ran into a problem where I needed to know what the outcome of the Coq Worker was. For example, I need to know whether it runs into any problems before reaching the "Qed." statement. Is there any way to use javascript to get this information?

view this post on Zulip Shachar Itzhaky (May 11 2021 at 13:49):

Sounds interesting! Is it enough for you to know if the current document contains an error sentence (i.e. a sentence marked in red)? Because this is easy to get although we have not documented the API so much :(

view this post on Zulip Shachar Itzhaky (May 11 2021 at 13:49):

There is a pending issue on this: https://github.com/jscoq/jscoq/issues/216

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2021 at 13:51):

As of today there is little structure on Coq documents, indeed most of you can do is to query a particular sentence for information, in this case for example you could ask indeed for goals or for success status kind of easily.

view this post on Zulip Emilio Jesús Gallego Arias (May 11 2021 at 13:51):

But indeed see the discussion @Shachar Itzhaky pointed


Last updated: Jan 31 2023 at 09:01 UTC