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
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!
The whole shelving mess is a bit over my head unfortunately.
Hum, I think I found it, I've a duplicate evar on my side.
sorry for the noise
After Maxime's last PR, the mess is much smaller (I think it got in, but I might be wrong)
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: Dec 06 2023 at 14:01 UTC