Stream: Coq devs & plugin devs

Topic: tac-in-terms and shelve


view this post on Zulip Enrico Tassi (Jun 25 2021 at 14:02):

I'm adding some glue in Coq-Elpi to let one use tactics written in Elpi in the middle of terms. It is working quite nice, but I've a problem with "shelved goals". Elpi tactics return the list of subgoals and shelved goals, so I have the choice of what to do when the tac-in-term leaves goals open.
But I get a wrong behavior, namely the leftover goal, no matter how I declare it, gets duplicate when I call Unshelve.

Goal bool * bool.
epose ( X := (true , ltac:(shelve) : bool) ).
Unshelve. (* works , 1 extra *)
exact X.
exact false. (* extra *)
Qed.

Goal forall T (a b : T), G.
Proof.
move=> T a b.
epose (A := A.pack T (_ : hasA T)). (* this hides ltac:(elpi mytac ...) *)
Unshelve. (* I have 3 goals now! G + "hasA T" twice *)

These are the last lines of my tactic, where declared_goals and shelved_goals come from the Elpi code, and I did check that they contain no duplicate (in my tests, only one list is non empy).

  tclTHENLIST [
    tclEVARS (S.get engine state).sigma;
    tclSETGOALS @@ List.map Proofview.with_empty_state declared_goals;
    Proofview.shelve_goals shelved_goals
  ]

@Pierre-Marie Pédrot help!

view this post on Zulip Pierre-Marie Pédrot (Jun 25 2021 at 14:06):

The whole shelving mess is a bit over my head unfortunately.

view this post on Zulip Enrico Tassi (Jun 25 2021 at 14:06):

Hum, I think I found it, I've a duplicate evar on my side.

view this post on Zulip Enrico Tassi (Jun 25 2021 at 14:06):

sorry for the noise

view this post on Zulip Pierre-Marie Pédrot (Jun 25 2021 at 14:06):

:shrug:

view this post on Zulip Matthieu Sozeau (Jun 25 2021 at 14:17):

After Maxime's last PR, the mess is much smaller (I think it got in, but I might be wrong)

view this post on Zulip Enrico Tassi (Jun 25 2021 at 14:44):

In the end, it all makes sense. I'll add a rechability check in Coq-Elpi, so that a spurious evar does not turn out to be a goal. The API on the Coq side is very picky, if there was a "garbage collector" it would have just dropped the extra one :-/


Last updated: Oct 16 2021 at 02:03 UTC