What is the right OCaml function to create an evar such that the result is the same that I would get from open_constr:(_ : my_type)
(+ removing the cast afterwards) in Ltac2? I've cobbled something together but it is either 100x slower than the Ltac2 variant in some cases or it triggers a diverging code path somewhere. In any case, before I try to debug my code I thought I'd ask.. There must be something I can just call, right?
I'd go for Evarutil.new_evar
Okay. That's what I tried initially but it didn't give me same evar context as open_constr
. Now that I think about it maybe I was using tclENV
instead of goal.env gl
. I'll try again!
Look at tactics.ml, there are plenty of examples there.
Indeed, I see plenty of uses of new_evar
there. (And we use it in Mtac2 as well, which is why I tried it first.) However, it has the same problem as my more complicated attempt that used new_pure_evar
: it is very, very, very, very slow. I don't think it is stuck exactly but it is slowly grinding to a halt. Here's perf top
of the process that is running a tactic call that takes maybe 10s with open_constr:
and has now been running for almost 10 minutes with Evarutil.new_evar
:
image.png
(And I was indeed using the wrong environment in my first attempt with Evarutil.new_evar
)
Ah, I am beginning to realize what is going on. The divergence is in the tactic. So new_evar
is not a drop-in replacement. I just need to figure out where the difference is.
_ : ty
is just new_evar in a cast afaict
Well, it took me several hours and I still do not understand what the actual difference is. But I got a bit closer. At this point I know that a certain Hint Extern
triggered by TC search (on a subgoal generated by an instance) runs Rtauto.rtauto
and if the original TC query is executed on an evar generated by open_constr:
the call to rtauto
succeeds, but if the evar was generated by make_evar
rtauto
does not succeed. The goals that rtauto
is run on look 100% identical (including all hypotheses) in both cases. Executing rtauto
on that goal in a fresh Goal
also succeeds. I can't spend any more time on this so at this point I'll throw out rtauto
since it seems to be the only tactic that exhibits this problem when using make_evar
.
The evars also look 100% identical under Set Printing Existential Instances
but I think there is quite a bit of extra state there that I wouldn't be able to observe in coqtop.
Typical stuff you should look for lives in the corresponding evar info.
I wouldn't be surprised if for instance the infamous evar_kind were different.
The evar_kind ADT is a potpourri of half-baked state used sometimes merely for display and debugging, and sometimes it actually changes the behaviour of the unification engine.
I would look into a difference of TYPECLASS EVARS as reported by pr_evar_map and the like
Also, maybe there are filters around (represented by {})
Thanks for the suggestions! I am already way over time budget with this so I probably won't come back to it any time soon. But having some clue regarding next debugging steps will be very helpful if I find any more breakage around this in the future.
Last updated: Dec 07 2023 at 09:01 UTC