Li-yao (Mar 06 2023 at 22:56): Li-yao (Mar 06 2023 at 22:56):This function Hints.FullHint.pattern was removed recently. It is used here in the QuickChick plugin. Are we not supposed to look at that pattern?
Pierre-Marie Pédrot (Mar 07 2023 at 07:23):This was introduced recently I guess? This function was not used there at the time of removal, since it would have broken CI compilation otherwise. In any case you shouldn't look at the pattern, this was most of the time (badly) generated from the type of the underlying clenv. I guess that the sanest way to emulate this is to look at the repr output, but even that is not really recommended.
Janno (Mar 07 2023 at 08:03):repr seems to be basically deprecated without being fully deprecated.
This function is for backward compatibility only, not to use in newly written code.
Janno (Mar 07 2023 at 08:06):I wonder what is wrong with the way that the hint patterns are computed. AFAICT the pattern is still used in the dnet code, isn't it? We also use FullHint.pattern and it seems to work without issues. In fact, we actually rely on more details in the patterns than what is used in the dnet and haven't found any problems so far.
Pierre-Marie Pédrot (Mar 07 2023 at 08:07):No, the pattern used in the dnet is unrelated to the one exposed in the pattern function. It was only used in a broken way by the filtered typeclass option.
Pierre-Marie Pédrot (Mar 07 2023 at 08:08):Both are (used to, for pattern) generated from the type of the hint.
Janno (Mar 07 2023 at 08:34):Oh, this is news to me. How is the pattern used in the dnet computed? I thought it was based on the same data returned by FullHint.pattern.
Janno (Mar 07 2023 at 08:35):I've followed a bunch of definitions from Bounded_net.add to make_apply_entry and that calls Patternops.pattern_of_constr env (clenv_evd ce) c' (when no explicit pattern was provided by the user) so it seems to be based on clenv stuff?
Pierre-Marie Pédrot (Mar 07 2023 at 09:39):Yes, the clenv type is just the type of the hint (with products instantiated by metas)
Janno (Mar 07 2023 at 10:06):I do not understand but I think that might be because I actually have no idea what clenv is. I suppose the most important question to me is: what could go wrong in relying on FullHint.pattern and is there going to be a replacement for it in 8.18? (Possibly even a better one that returns the same pattern that the dnet uses to compute the dnet-internal pattern?)
Pierre-Marie Pédrot (Mar 07 2023 at 10:10):pattern_of_constr is a very dubious function, so there is no plan to put the hint pattern back in 8.18. I imagine we could expose the internals of the Dnet implementation but this is fragile. Judging from the QuickChick implementation, this looks like an XY problem. They really want to access the type of the hint.
Janno (Mar 07 2023 at 10:16):I see. I wouldn't advocate for exposing dnet internals. I suppose we'll start relying on FullHint.repr instead of FullHint.pattern and we'll call the dubious pattern_of_constr function explicitly. We already use it in other parts of the code..
Pierre-Marie Pédrot (Mar 07 2023 at 10:19):Why can't you work directly on the underlying constr?
Pierre-Marie Pédrot (Mar 07 2023 at 10:21):Constr is pretty much the only term structure which is really observable, all other ones are quirky. For instance, constr_expr, glob_constr and patterns should only be used for consumption of dedicated functions. Funind famously tried to build glob_constr by hand and the results is interesting to say the least.
Janno (Mar 07 2023 at 10:21):Mostly for compatibility with typeclasses eauto. We could emulate the effect of going through pattern_of_constr without leaving (E)Constr.t but that just sounds like extra work for no benefit.
Pierre-Marie Pédrot (Mar 07 2023 at 10:22):The thing is that there is a lot of stuff going on already in the dnet pattern interpretation, so there are a myriad of cornercases. Luckily they tend to to happen in real code, but they're there nonetheless.
Pierre-Marie Pédrot (Mar 07 2023 at 10:23):I'm thinking about stuff like the call to hnf_constr in some but not all cases and all the built-in hack to approximate βι-weak rigid heads in the dnet.
Pierre-Marie Pédrot (Mar 07 2023 at 10:24):We should probably expose a saner API instead, poking in there is definitely not recommended.
Li-yao (Mar 07 2023 at 11:37):Pierre-Marie Pédrot said:
This was introduced recently I guess?
More or less. That happened in a separate branch, so it was not tracked by Coq CI. Using repr instead seems like a good guess, at least until someone else finds a better way. Thanks!
Janno (Mar 17 2023 at 10:19):Is there a solution for retrieving the pattern in Hint Resolve my_term | pattern : ..? pattern can't be reconstructed from the type of my_term.
Pierre-Marie Pédrot (Mar 17 2023 at 10:51):Probably not, nowadays this pattern is immediately turned into a Dnet pattern and kept there.
Janno (Mar 17 2023 at 11:01):Hm. So this change to remove FullHint.pattern is turning out to be a real headache for us.
Pierre-Marie Pédrot (Mar 17 2023 at 11:25):What are you trying to achieve exactly? The Hints API exposes something that is really not fit for external consumption, I really think we should give you something more principled (as a reasonable iterator, notably).
Janno (Mar 17 2023 at 12:06):The short summary is that we are bypassing typeclasses eauto because it's far too slow for us but we still use the various Hint/Instance commands to register hints, modes, etc. We could implement some kind of custom Hint-like command that replicates most of what exists today and gives us access to patterns but it's not going to be as nicely integrated as the existing infrastructure in coq (for example :> fields in Classwouldn't just work, we couldn't use Instance, etc.).
Pierre-Marie Pédrot (Mar 17 2023 at 12:10):What do you need more than what typeclasses eauto requires? Do you still use dnets or you just don't care and reimplement everything from scratch?
Janno (Mar 17 2023 at 12:13):We were using dnets but we are moving away from that. And it's not that we need more than typeclasses eauto it's just that typeclasses eauto is just too slow for the kind and number of queries that we run. The only thing we really do differently is that we decouple the opacity used in interpreting hint patterns from the database the hint comes from but that's a minor detail.
Pierre-Marie Pédrot (Mar 17 2023 at 12:18):Ah, so indeed this goes against the current dnet implem.
Pierre-Marie Pédrot (Mar 17 2023 at 12:19):The dnet pattern is computed relatively to the db transparent state, if you decouple that in the current implem you'll have weird things going on.
Janno (Mar 17 2023 at 12:20):We are not directly relying on the existing dnet code. We've had to add quite a few missing functions that make it all fast enough for our use case. I am not sure I can say much more since the automation is considered secret sauce :(
Janno (Mar 17 2023 at 12:26):In any case, we are basically regarding Coq's existing hint registration infrastructure as a black box and extracting whatever we can using the existing functions. This worked well enough and we can probably make it work even if we have to recompute patterns for Hint Resolves without explicit patterns but we need access to the patterns given explicitly for Hint Extern and Hint Resolve.
Paolo Giarrusso (Mar 17 2023 at 12:27):Is this question solvable via more mutable hooks at some suitable places, say for :>, Instance, ...?
Paolo Giarrusso (Mar 17 2023 at 12:27):We're not the only one who want to replace typeclasses eauto, @Enrico Tassi also had interest
Janno (Mar 17 2023 at 12:28):We are not replacing typeclasses eauto. We are replacing its use in specific queries. I'd really like to avoid re-doing the whole hint registration infrastructure if we can at all avoid that.
Paolo Giarrusso (Mar 17 2023 at 12:29):right sorry; you just want Coq to persist the explicit pattern and expose a way to retrieve it?
Paolo Giarrusso (Mar 17 2023 at 12:30):(but feel free to ignore my comments if they don't help)
Janno (Mar 17 2023 at 12:35):Yes, access to the explicit patterns would be enough for us
Rodolphe Lepigre (Mar 17 2023 at 12:43):@Pierre-Marie Pédrot I'm not sure I follow why you think relying on the function that was removed is so bad. It seems to work fine for our use case (at least in cases we encountered), so we'd really prefer for it to be put back in the interface, since otherwise we'll need a pretty complicated workaround. As long as the pattern is still computed internally, and the implementation of the function remains trivial, do you see a good reason not to just reinstate it?
Pierre-Marie Pédrot (Mar 17 2023 at 12:47):There is a cost to this, as the old interface was uselessly translating hint types to patterns, which is useless since it's was essentially never used.
Pierre-Marie Pédrot (Mar 17 2023 at 12:47):I could have the function return an option set to Some if the pattern is indeed passed at hint creation.
Janno (Mar 17 2023 at 12:48):That would work
Rodolphe Lepigre (Mar 17 2023 at 12:48):Indeed.
Pierre-Marie Pédrot (Mar 17 2023 at 12:48):Also, I consider that FullHint is a purely internal API. The one that should be exposed that doesn't exist today would correspond to raw_hint in the internals of the Hint module.
Pierre-Marie Pédrot (Mar 17 2023 at 12:49):FullHint tells to much about how this stuff is supposed to work as a clenv.
Rodolphe Lepigre (Mar 17 2023 at 12:52):It is a purely internal API that is accessible to plugins, so how can we know we're not supposed to use it? :big_smile:
In any case, as you said, we have no alternative right now.
Pierre-Marie Pédrot (Mar 17 2023 at 12:53):Ah, but you haven't read the disclaimer about the OCaml API of Coq: basically we promise nothing.
Rodolphe Lepigre (Mar 17 2023 at 12:54):I guess we'll need to rewrite Coq then.
Janno (Mar 17 2023 at 12:54):We are using: FullHint.name, FullHint.pattern, FullHint.print, FullHint.priority, FullHint.repr, FullHint.run. We can drop name but the others I think are unavoidable for us.
Pierre-Marie Pédrot (Mar 17 2023 at 12:54):I'll readd the pattern function, but that will only be there for the upcoming 8.18 as IIUC 8.17 was shipped without the function.
Janno (Mar 17 2023 at 12:55):I thought the change went into 8.18
Gaëtan Gilbert (Mar 17 2023 at 12:55):17 isn't shipped yet
Pierre-Marie Pédrot (Mar 17 2023 at 12:55):@Rodolphe Lepigre also we recommend that plugins are put in the Coq CI precisely to avoid this kind of situation
Gaëtan Gilbert (Mar 17 2023 at 12:55):Janno said:
I thought the change went into 8.18
yes https://github.com/coq/coq/pull/16911
Pierre-Marie Pédrot (Mar 17 2023 at 12:56):Good.
Rodolphe Lepigre (Mar 17 2023 at 12:56):If that were up to me, our plugins would be made public, but I don't think that's possible for now.
Gaëtan Gilbert (Mar 17 2023 at 12:57):plugins outside CI are supported only when we feel like it
if they break and fixing it is annoying, we don't care
sort of like a bit less strict linux kernel modules policy replacing "in tree" with "in CI"
(in this case readding the optional pattern API may be non annoying)
Matthieu Sozeau (Mar 17 2023 at 12:58):Janno said:
We were using dnets but we are moving away from that. And it's not that we need more than
typeclasses eautoit's just thattypeclasses eautois just too slow for the kind and number of queries that we run. The only thing we really do differently is that we decouple the opacity used in interpreting hint patterns from the database the hint comes from but that's a minor detail.
Can you hint why it's too slow for your cases?
Janno (Mar 17 2023 at 13:00):We are batching queries to exploit commonalities between subsets of queries
Janno (Mar 17 2023 at 13:00):I don't really see a generic way to provide the same speedup in general
Janno (Mar 17 2023 at 13:00):It's very specific to our automation
Andres Erbsen (Mar 17 2023 at 13:01):Just +1 to typeclasses eauto being slow: I've also tried to understand why it is slow, without success. The best current (barely usable) examples are in cross-crypto.
Pierre-Marie Pédrot (Mar 17 2023 at 13:02):@Andres Erbsen you mean, even assuming a sane TC database?
Pierre-Marie Pédrot (Mar 17 2023 at 13:03):(i.e. with all modes set, no weird redudancies and the like)
Janno (Mar 17 2023 at 13:05):One of the issues is that in a big development with many dependencies outside of our control it's almost always the case that typeclass_instances is not a sane database
Janno (Mar 17 2023 at 13:05):It's a dumping ground basically
Andres Erbsen (Mar 17 2023 at 13:07):It was typeclass_instances with the standard library and little else Required :shrug:
Janno (Mar 17 2023 at 13:08):Well, that's even worse then! :D
Pierre-Marie Pédrot (Mar 17 2023 at 13:36):there you go: https://github.com/coq/coq/pull/17401
Janno (Mar 17 2023 at 13:51):Just to make sure I understand this: this seems to be the exact same function as before but does it also compute the same thing it computes in 8.16/8.17 or has the underlying data changed? In any case, would it make sense to add an explicit_pattern function that only returns a pattern if that was explicitly set at hint registration time? Do the internals allow for making that distinction after the fact?
Gaëtan Gilbert (Mar 17 2023 at 13:51):it's not the same, it returns option
basically it's the explicit_pattern you talk about
Janno (Mar 17 2023 at 13:52):So that means it is different from the one in 8.16? Because that one gives out patterns even when they are merely derived from a term
Gaëtan Gilbert (Mar 17 2023 at 13:52):yes
Janno (Mar 17 2023 at 13:52):Okay, that's somewhat confusing but it will be very useful for us :)
Matthieu Sozeau (Mar 17 2023 at 13:58):Janno said:
It's a dumping ground basically
You have typeclasses eauto with but indeed you lose all the declared instances etc...
Hugo Herbelin (Mar 17 2023 at 15:30):also we recommend that plugins are put in the Coq CI precisely to avoid this kind of situation
In passing: a reminder could be sent on coq-club. I'm pretty sure that in a "second" or "third" circle of users, there are plugins developed.
Karl Palmskog (Mar 17 2023 at 16:04):if you send a reminder via email, we recommend sending it both to Coq-Club and Discourse Announcements topic: https://github.com/coq/coq/wiki/Discourse
Janno (Mar 31 2023 at 13:55):It seems another change to FullHint.pattern made it into 8.17: Hint Resolve T only has a pattern if T has premises (or an explicit pattern given in Hint Resolve .. | pattern). Which MR changed this?
Janno (Mar 31 2023 at 14:12):I guess it's https://github.com/coq/coq/pull/16815, isn't it?
Pierre-Marie Pédrot (Mar 31 2023 at 14:25):Looks like it.
Last updated: Oct 12 2024 at 12:01 UTC