Coq Plugin to output hypotheses, goal and tactic in JSON

Developing plugins
1

Hello!
I want the following as JSON. In proofs:

  • Goal (top one / first)
  • all hypotheses
  • last applied tactics

For those I do not just need the string representation, but names and also the types (like variable, …). It looks that coqtopide XML output provides this information, but it is a nightmare to parse. So I’m currently trying to write a plugin to get this information.

I managed to setup everything for the plugin and the skeleton kind of works:

let hypothesis_to_json sigma env (name: Names.Id.t) (typ: Constr.t) =
  let typ_str = Printer.pr_ltype_env env sigma typ in
  let name_str = Names.Id.to_string name in
  "{ \"name\": \"" ^ name_str ^ "\", \"type\": \"" ^ (Pp.string_of_ppcmds typ_str) ^ "\" }"

let extract_hypotheses sigma env =
  let named_ctx = Environ.named_context env in
  let hypotheses_json_list = List.map (fun decl ->
      let name = Context.Named.Declaration.get_id decl in
      let typ = Context.Named.Declaration.get_type decl in
      hypothesis_to_json sigma env name typ
    ) named_ctx in
  String.concat ", " hypotheses_json_list

let printProofStateAsJson ~pstate =
  let sigma, env = Declare.Proof.get_current_context pstate in
  let hypotheses_json = extract_hypotheses sigma env in
  let goals_json = "{ \"dummy\": \"goal\" }" in
  Feedback.msg_notice
    (Pp.str (Printf.sprintf "{ \"hypotheses\": [%s], \"goals\": [%s] }"
             hypotheses_json goals_json))

Test / Example:

Theorem add_0_r : forall n:nat, n + 0 = n.
Proof.
  ProofStateAsJson. intros n. ProofStateAsJson. induction n as [| n' IHn'].
  - ProofStateAsJson. (* n = 0 *)    reflexivity. ProofStateAsJson.
  - ProofStateAsJson. (* n = S n' *) simpl. ProofStateAsJson. rewrite -> IHn'. ProofStateAsJson. reflexivity.  ProofStateAsJson. Qed.

Currently I’m stuck as I have no idea how to get the the goal and last tactic information and also how to get the more detailed information of the hypotheses (like type, name, …).

I had a look at different plugins, but did not find any decent way.

Any help and hint is highly welcome!

2

Hi @florath , a Coq plugin is not going to work for your case, unless you do some big hacks. Coq plugins are per-sentence, so they cannot observe documents as you want.

You want instead a document-level plugin. The way I recommend now is to create a plugin for the fcc extensible Coq compiler, see an example here [plugin] Goal dump plugin. by ejgallego · Pull Request #619 · ejgallego/coq-lsp · GitHub

Note that several people has already forked the above plugin, I’d be great folks if you would coordinate.

Please come to coq-lsp Zulip if you have any questions.

3

Hello @ejgallego,
thanks a lot for this reply. This helps a lot.

Maybe I miss something, but I do not find the plugin itself (the link is to a not merged PR where the original branch is deleted).

Will check the Zulip stream.

4

Oh sorry, indeed the plugin is now merged in the plugins/goaldump directory.

I will try to document it and clean up it a bit more.

5

SerAPI works great for this, and there’s a wrapper for it in Alectryon (scroll to Output (minimal.json.io.json in the README).

(And when SerAPI gets retired I’ll port Alectryon to whatever the replacement is.)

1 Like