Dear Coq developers,
I am working on a Coq plugin that shall be able to extract information about a proof programmatically, i.e. via OCaml.
More specifically, I would like to extract all closed and aborted goals, used tactics and the hypotheses (the environment) for each of the goals…
I already crawled through the source code of Coq 8.9 which I develop against. In the proof.mli file, I found some information which did not help me as I am not sure if the defined structures give me the information I need.
Can you give me some hint about how to get the following information:
- all open, closed and aborted goals in a proof
- the current list of hypotheses for each of those goals
- the tactics that led to the goals
As I want to do it myself, I would be grateful for just the information which data structures and functions can/should be used to fetch the information.
Regards
Mario
Have a look to this file for example: https://github.com/ejgallego/coq-serapi/blob/v8.10/serapi/serapi_goals.ml
I suggest you target 8.10 as the API has changed quite a bit and your dev should be more future proof.
the tactics that led to the goals
That’s hard to know programmaticaly, however you can always use the AST of the document, but beware Coq’s AST is tricky due to its extensibility.
Correct me if I’m wrong here, but couldn’t one use the Ltac profiler to figure out tactics leading up to goals?
Depending on what you want to do it may work or not; AFAIK it is not designed to perform reproducible traces.
Dear Emilio and Karl,
thank you for your Input.
Ltac profiler will not meet my requirements completely but I think at least it gives me some information about how I could record the used tactics. Using the AST may also be a viable solution.
Targeting Coq 8.10 war my previous plan but I had some difficulties with parallel installation of the current Coq 8.9 via OPAM and local installation of Coq 8.10. But I will go for Coq 8.10.
Regards
Mario
Coq 8.10 is almost in Beta so IMHO that’s a good choice and provides some advanced tooling such as Dune which turns out quite handy for plugin development.
You could also use SerAPI of course, I am fully open to extending the query language if you feel this way; IMHO, at the very least playing with it for a while should help you understanding how Coq organizes goals.
Hey, I found an acceptable way based on Coq 8.10 to get the data needed and now have a prototypical implementation.
But I would like to reuse some coqtop functions that are not exposed in the mli files. The relevant functions are Vernac.checknav_simple, Vernac.interp_vernac and Coqtop.fatal_error_exn.
I created a patch based on branch v810. Is it possible to submit this patch for review and inclusion?
Regards,
Mario
My bad. I just read the CONTRIBUTING.md which answers my question.
1 Like
Indeed @mafrank submit a PR and we will try to help! That’s an interesting choice of functions tho 
A pull request is submitted. The choice of functions may indeed seem odd. But what I do is processing vernacular files in batch mode and extract relevant information. So I have to make sure that the files themselves are valid in structure and also in content. And as the reused functions seem to be free from unwished sideeffects, exposing them should be safe.