Enrico Tassi (Jun 25 2021 at 14:02): 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!
Pierre-Marie Pédrot (Jun 25 2021 at 14:06):The whole shelving mess is a bit over my head unfortunately.
Enrico Tassi (Jun 25 2021 at 14:06):Hum, I think I found it, I've a duplicate evar on my side.
Enrico Tassi (Jun 25 2021 at 14:06):sorry for the noise
Pierre-Marie Pédrot (Jun 25 2021 at 14:06)::shrug:
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)
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: Sep 15 2024 at 13:02 UTC