# Coq Plugin to output hypotheses, goal and tactic in JSON

**URL:** <https://discourse.rocq-prover.org/t/coq-plugin-to-output-hypotheses-goal-and-tactic-in-json/2220>\
**Category:** Developing plugins\
**Created:** [March 12, 2024, 2:03pm UTC](https://discourse.rocq-prover.org/t/coq-plugin-to-output-hypotheses-goal-and-tactic-in-json/2220 "2024-03-12T14:03:45Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![florath](https://avatars.discourse-cdn.com/v4/letter/f/cab0a1/32.png) [@florath](https://discourse.rocq-prover.org/u/florath)\
**Post date:** [March 12, 2024, 2:03pm UTC](https://discourse.rocq-prover.org/t/coq-plugin-to-output-hypotheses-goal-and-tactic-in-json/2220/1 "2024-03-12T14:03:45Z")

</div>

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:

```auto
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:

```auto
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!

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [March 12, 2024, 2:36pm UTC](https://discourse.rocq-prover.org/t/coq-plugin-to-output-hypotheses-goal-and-tactic-in-json/2220/2 "2024-03-12T14:36:32Z")

</div>

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](https://github.com/ejgallego/coq-lsp/pull/619)

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.

---

<div class="post-metadata">

**Author:** ![florath](https://avatars.discourse-cdn.com/v4/letter/f/cab0a1/32.png) [@florath](https://discourse.rocq-prover.org/u/florath)\
**Post date:** [March 12, 2024, 4:27pm UTC](https://discourse.rocq-prover.org/t/coq-plugin-to-output-hypotheses-goal-and-tactic-in-json/2220/3 "2024-03-12T16:27:36Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![ejgallego](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/ejgallego/32/10_2.png) [@ejgallego](https://discourse.rocq-prover.org/u/ejgallego)\
**Post date:** [May 10, 2024, 8:38pm UTC](https://discourse.rocq-prover.org/t/coq-plugin-to-output-hypotheses-goal-and-tactic-in-json/2220/4 "2024-05-10T20:38:38Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![cpitclaudel](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/cpitclaudel/32/337_2.png) [@cpitclaudel](https://discourse.rocq-prover.org/u/cpitclaudel)\
**Post date:** [May 11, 2024, 8:11am UTC](https://discourse.rocq-prover.org/t/coq-plugin-to-output-hypotheses-goal-and-tactic-in-json/2220/5 "2024-05-11T08:11:38Z")

</div>

SerAPI works great for this, and there’s a wrapper for it in Alectryon (scroll to `Output (minimal.json.io.json` in [the README](https://github.com/cpitclaudel/alectryon?tab=readme-ov-file#as-a-standalone-program)).

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