Janno (Mar 22 2021 at 19:08): Janno (Mar 22 2021 at 19:08):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?
Pierre-Marie Pédrot (Mar 22 2021 at 19:09):I'd go for Evarutil.new_evar
Janno (Mar 22 2021 at 19:11):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!
Pierre-Marie Pédrot (Mar 22 2021 at 19:20):Look at tactics.ml, there are plenty of examples there.
Janno (Mar 22 2021 at 19:24):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
Janno (Mar 22 2021 at 19:24):(And I was indeed using the wrong environment in my first attempt with Evarutil.new_evar)
Janno (Mar 22 2021 at 19:40):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.
Gaëtan Gilbert (Mar 22 2021 at 20:38):_ : ty is just new_evar in a cast afaict
Janno (Mar 23 2021 at 10:05):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.
Janno (Mar 23 2021 at 10:06):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.
Pierre-Marie Pédrot (Mar 23 2021 at 10:14):Typical stuff you should look for lives in the corresponding evar info.
Pierre-Marie Pédrot (Mar 23 2021 at 10:14):I wouldn't be surprised if for instance the infamous evar_kind were different.
Pierre-Marie Pédrot (Mar 23 2021 at 10:15):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.
Matthieu Sozeau (Mar 23 2021 at 17:17):I would look into a difference of TYPECLASS EVARS as reported by pr_evar_map and the like
Matthieu Sozeau (Mar 23 2021 at 17:18):Also, maybe there are filters around (represented by {})
Janno (Mar 23 2021 at 18:17):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