Stream: Coq devs & plugin devs

Topic: 8.9 Proof.run_tactic getting new context and subgoals


view this post on Zulip RanDair Scott Porter (May 10 2021 at 21:43):

I'm using Proof.run_tactic in Coq 8.9, and I would like to get back the new contexts (an env) and conclusions (a constr) for each subgoal.
I am able to get a Goal.goal list, and I am able to use the functions Goal.V82.env, Goal.V82.concl, and Goal.V82.abstract_type.

Any tips? Thank you!

view this post on Zulip Talia Ringer (May 12 2021 at 17:41):

buuump we'd super love help if anyone knows :). @Emilio Jesús Gallego Arias ?

view this post on Zulip Talia Ringer (May 12 2021 at 17:43):

RanDair does val hyps : t -> EConstr.named_context get you anything?

view this post on Zulip Talia Ringer (May 12 2021 at 17:43):

I think that would be what maps the vars

view this post on Zulip Gaëtan Gilbert (May 12 2021 at 18:42):

have a look around https://github.com/coq/coq/blob/5714656cb3f8a676c126a8d8e67ea2d92781d780/engine/proofview.mli#L517 (8.9 api should be similar)

Goal.V82.env seems to return nothing.

I don't know what you mean by "nothing"

Goal.V82.concl returns the correct conclusion, but all of the Rel indices are replaced with Vars.

Var is correct, I don't know why you expect Rel

view this post on Zulip Emilio Jesús Gallego Arias (May 12 2021 at 18:45):

I don't even have a 8.9 tree around that works in my current dev workflow sorry @Talia Ringer , I was hesitant to give thus incorrect advice; one thing that may help is to look at the goal printer, there you can see how the different bits of goals are extracted from the proof state, but that API is still a bit in flux (Proof.t and friends)

view this post on Zulip RanDair Scott Porter (May 12 2021 at 18:56):

Gaëtan Gilbert said:

I don't know what you mean by "nothing"

My bad, I meant that I did not see any indices pushed onto that environment.

Var is correct, I don't know why you expect Rel

I think I expected a Rel because I want to use the goal to call Proof.run_tactic again with the proper goal and context.

view this post on Zulip Gaëtan Gilbert (May 12 2021 at 19:13):

My bad, I meant that I did not see any indices pushed onto that environment.

context variables are in the named_context part of the env

I think I expected a Rel because I want to use the goal to call Proof.run_tactic again with the proper goal and context.

I don't see how the 2 parts of this sentence are connected


Last updated: Oct 21 2021 at 21:03 UTC