I'm trying to write a new Command, that when called from within a proof context, prints the lemma of the open proof.

This is the code I have:

VERNAC COMMAND EXTEND TryThis CLASSIFIED AS QUERY

| ![proof_query] [ "TryThis" ] ->

{

fun ~pstate ->

let proof_data = Proof.data (Declare.Proof.get pstate) in

Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Evar.print proof_data.goals)

}

END

But this prints results like:

?X4

?X6

?X7

Instead of the lemma.

Am I using the wrong api for my goal?

not sure what you mean by "the lemma of the open proof"

possible meaning of "lemma of proof": the type of the constant the proof script is defining the body for.

that's in the Proof.Data.entry

@Arpan Agrawal wants to print the goals, see for example https://github.com/ejgallego/coq-lsp/blob/3583019eb3ab79b5a09cacb6a15d62a5c5c6fe2f/coq/goals.ml#L68 for code to get both the goals and the hypothesis

@Emilio Jesús Gallego Arias sorry, I dont fully understand the code you linked to. Is there a place I can read more about this? Or can you tell me what is wrong with the code I wrote initially?

Gaëtan Gilbert said:

that's in the Proof.Data.entry

How do I get a string representation of the entry type? I cant find a function for that in the documentation.

Just to clarify, lets say I have:

Theorem foo: (2 + 2 = 4).

Proof.

TryThis.

Abort.

I want this to print: (2 + 2 = 4)

Is there a way to do this?

Thanks!

oh you want to reimplement `Show`

look at Printer.pr_open_subgoals

Gaëtan Gilbert said:

oh you want to reimplement

`Show`

look at Printer.pr_open_subgoals

Thank you! This is exactly what I was looking for.

Arpan Agrawal has marked this topic as resolved.

@Arpan Agrawal goals in Coq are just numbers, that's what your printer is printing, in Coq terminology these numbers are called "evars". To fetch what _type_ does the evar have, you need to fetch that information from a table, that's what `get_goal_type`

does, the table is in sigma

Gaëtan Gilbert said:

oh you want to reimplement

`Show`

look at Printer.pr_open_subgoals

I think that'd be `Show Goals`

, show printers the underlying proof term IIRC.

The code I posted is just a more generic pr_open_subgoals by the way

Emilio Jesús Gallego Arias said:

Arpan Agrawal goals in Coq are just numbers, that's what your printer is printing, in Coq terminology these numbers are called "evars". To fetch what _type_ does the evar have, you need to fetch that information from a table, that's what

`get_goal_type`

does, the table is in sigma

Thanks! That makes sense.

@Arpan Agrawal what is your real need? I'm asking because writing OCaml code to extend Coq is not super easy.

Maybe there are simpler ways to do what you need.

Arpan Agrawal has marked this topic as unresolved.

@Enrico Tassi my end goal is to build a plugin that calls a proof synthesis model. So ideally, I want a tactic/command that gets the current proof state, all the tactics used in the current proof context and calls a python function with these as arguments, receives the results and displays them.

Last updated: Dec 07 2023 at 14:02 UTC