Aadith C (May 10 2021 at 20:45): 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?
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 :(
Shachar Itzhaky (May 11 2021 at 13:49):There is a pending issue on this: https://github.com/jscoq/jscoq/issues/216
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.
Emilio Jesús Gallego Arias (May 11 2021 at 13:51):But indeed see the discussion @Shachar Itzhaky pointed
Last updated: Sep 15 2024 at 12:01 UTC