Stream: Coq devs & plugin devs

Topic: Creating evars the same way `open_constr` does.


view this post on Zulip 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?

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 19:09):

I'd go for Evarutil.new_evar

view this post on Zulip 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!

view this post on Zulip Pierre-Marie Pédrot (Mar 22 2021 at 19:20):

Look at tactics.ml, there are plenty of examples there.

view this post on Zulip 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

view this post on Zulip Janno (Mar 22 2021 at 19:24):

(And I was indeed using the wrong environment in my first attempt with Evarutil.new_evar)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Mar 22 2021 at 20:38):

_ : ty is just new_evar in a cast afaict

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2021 at 10:14):

Typical stuff you should look for lives in the corresponding evar info.

view this post on Zulip Pierre-Marie Pédrot (Mar 23 2021 at 10:14):

I wouldn't be surprised if for instance the infamous evar_kind were different.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Matthieu Sozeau (Mar 23 2021 at 17:18):

Also, maybe there are filters around (represented by {})

view this post on Zulip 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: Oct 16 2021 at 03:02 UTC