The Coq mailing list

[e+coq-club AT x80.org (Emilio Jesús Gallego Arias)]

Hi Hani,

Hani Awni 
<hani.awni AT gmail.com>
 writes:

> I can design this translation, but the first step in this is getting
> my hands on Coq's current goals list, whether in OCaml or Lisp or
> Python.

As suggested by Gregory, you can use the XML protocol and ideslave to
get the goals. I don't have the details at hand but it shouldn't be
difficult to setup.

If you need more control over the goals you can see what the ocaml code
does here:

https://github.com/coq/coq/blob/trunk/ide/ide_slave.ml#L212

and this for coqtop:

https://github.com/coq/coq/blob/trunk/printing/printer.ml#L621

Also you may be interested in:

https://bitbucket.org/coqpide/pidetop/

jsCoq is quite boring for now, as it just calls pr_open_subgoals.

However, we have done some incomplete experiments with automatic
serialization of terms at:

https://github.com/ejgallego/jscoq/blob/master/coq-js/jssexp.ml

I have been working on an evolution of the current XML protocol for
JsCoq that in theory would allow you to get a bit more information of
what is currently possible, however don't hold your breath for it to
happen anytime soon.

Best,
E.