Stream: Coq devs & plugin devs

Topic: Command to print current lemma statement

Arpan Agrawal (Jan 12 2023 at 21:40):

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?

Gaëtan Gilbert (Jan 12 2023 at 22:11):

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

Karl Palmskog (Jan 12 2023 at 22:13):

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

Gaëtan Gilbert (Jan 12 2023 at 22:17):

that's in the Proof.Data.entry

Emilio Jesús Gallego Arias (Jan 12 2023 at 22:18):

@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

Arpan Agrawal (Jan 13 2023 at 17:39):

@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?

Arpan Agrawal (Jan 13 2023 at 18:50):

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!

Gaëtan Gilbert (Jan 13 2023 at 18:56):

oh you want to reimplement Show
look at Printer.pr_open_subgoals

Arpan Agrawal (Jan 13 2023 at 19:00):

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.

Notification Bot (Jan 13 2023 at 19:00):

Arpan Agrawal has marked this topic as resolved.

Emilio Jesús Gallego Arias (Jan 13 2023 at 19:00):

@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

Emilio Jesús Gallego Arias (Jan 13 2023 at 19:01):

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.

Emilio Jesús Gallego Arias (Jan 13 2023 at 19:01):

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

Arpan Agrawal (Jan 13 2023 at 19:03):

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.

Enrico Tassi (Jan 13 2023 at 19:32):

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

Enrico Tassi (Jan 13 2023 at 19:32):

Maybe there are simpler ways to do what you need.

Notification Bot (Jan 16 2023 at 17:43):

Arpan Agrawal has marked this topic as unresolved.

Arpan Agrawal (Jan 16 2023 at 17:43):

@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: Sep 15 2024 at 13:02 UTC