The Coq mailing list

[kirang <kirang AT comp.nus.edu.sg>]

Hi all,

I’m working on a project where for various reasons I’ve found myself 
needing to inspect the intermediate proof contexts of Coq proofs in a 
programmatic way from OCaml.

I’d like to get programatic access to view the corresponding proof 
context at intermediate points of given (possibly unfinished) proof 
scripts from OCaml:
```
1 goal (ID 22)

  x : nat
  IHx : forall y : nat, x + y = y + x
  y : nat
  ============================
  S (x + y) = y + S x
```
Note: I don’t need to modify/update/change the context, simply access 
it.

One simple way to do this would be to run coqtop as a external process 
and feed it in the prefix of the proof, and then use the show tactic and 
parse the result, but this seems fragile.

Seeing as I’m writing in OCaml anyway, I thought I’d try just running 
Coq directly as a library, and then reading the proof context directly 
through Coq’s own API, bypassing the need to do the parsing myself 
(albeit having to deal directly with the proof terms rather than the 
simplified notations).

Unfortunately, there isn’t much documentation on exactly which of Coq’s 
APIs need to be called in which order in order for Coq to be able to 
load a given file, so I’ve been running into issues with my programs 
just crashing at runtime when trying to invoke Coq, with fairly esoteric 
error messages such as “entry [integer] is empty”, etc.

As such, I’m wondering if anyone has had experience with using Coq in 
this way? or is this more difficult than it’s worth, and it’s probably 
better to just bite the bullet and parse the proof state instead?

Thanks,
Kiran.