Calling Coq from OCaml

Developing plugins
1

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.

Example:

(* proof.v *)

Lemma add_comm: forall x y, x + y = y + x.
Proof.
  intros x; induction x as [| x IHx].
  - intros y; induction y; auto.
  - intros y.
    rewrite plus_Sn_m.
    (* [view proof context here] *)
    rewrite IHx.
    rewrite plus_n_Sm.
    auto.
Qed.

I’d like to get programatic access to view the corresponding proof context at the marked intermediate point 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.

Naive Solution
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.

Problem
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 could point me to any examples of Coq being used in this way? or some minimal code snippet that I could use as a starting point for doing this?

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?

2 Likes
2

For reference, this is the code that I’ve been using so far to try and use Coq from OCaml to load a particular proof file, mostly based of what I could pick up from the Js-of-coq codebase.

let load_proof () =
  Lib.init ();
  Global.set_VM false;
  Global.set_native_compiler false;
  Flags.set_native_compiler false;
  Loadpath.add_vo_path Loadpath.{
    unix_path="../../_build/default/resources/proofs/";
    coq_path=Names.DirPath.make [(Names.Id.of_string "Proofs")];
    implicit=false;
    has_ml=false;
    recursive=true;
  };
  Stm.init_core ();
  let (doc, state) = Stm.new_doc Stm.{
    doc_type=VoDoc "../../_build/default/resources/proofs/proof.v";
    injections=[];
    stm_options=AsyncOpts.default_opts
  } in
  let vernac_state = Vernac.State.{
    doc; sid=state; proof=None; time = false
  } in
  Vernacstate.Parser.parse
  let _vernac_state' = 
    Vernac.load_vernac ~echo:false ~check:true ~interactive:false ~state:vernac_state
      "../../_build/default/resources/proofs/proof.v" in
  ()