Matthieu Sozeau (Mar 31 2021 at 08:37): Matthieu Sozeau (Mar 31 2021 at 08:37):How about we allow a mode which disables the primitive projections compatibility layer to help migrate? E.g. We would stop creating the compatibility constant and ignore the "unfolded" flag in that mode.
Pierre-Marie Pédrot (Mar 31 2021 at 08:40):Expect trouble.
Matthieu Sozeau (Mar 31 2021 at 08:40):That would most likely mean adding a ProjRef to global_reference as well
Pierre-Marie Pédrot (Mar 31 2021 at 08:41):Most likely we will end up having to add another flag afterwards because we forgot to tweak some transitive behaviour
Pierre-Marie Pédrot (Mar 31 2021 at 08:41):I believe that the moral of the primitive debacle is precisely that stacking piles of compatibility options is a recipe for disaster
Matthieu Sozeau (Mar 31 2021 at 08:41):?
Pierre-Marie Pédrot (Mar 31 2021 at 08:42):like, how are you sure that you successfully deactivated all compatibility code?
Pierre-Marie Pédrot (Mar 31 2021 at 08:42):there is a lot of it
Pierre-Marie Pédrot (Mar 31 2021 at 08:42):and in some places it's hard to realize that something is buggy
Matthieu Sozeau (Mar 31 2021 at 08:42):Well, these projections won't have an expand function
Pierre-Marie Pédrot (Mar 31 2021 at 08:43):yes but all the stuff with goal matching, hint patterns and the like?
Pierre-Marie Pédrot (Mar 31 2021 at 08:43):there is a crapload of code that tries to emulate compatibility
Pierre-Marie Pédrot (Mar 31 2021 at 08:43):not just expansion to a constant
Matthieu Sozeau (Mar 31 2021 at 08:43):Nothing special to do there, these rely on expand
Pierre-Marie Pédrot (Mar 31 2021 at 08:43):??
Pierre-Marie Pédrot (Mar 31 2021 at 08:43):no no, we store the constant in the projection name
Matthieu Sozeau (Mar 31 2021 at 08:44):But in the new mode, there will be no constant
Pierre-Marie Pédrot (Mar 31 2021 at 08:44):the code doesn't give a shit if the constant actually exists
Matthieu Sozeau (Mar 31 2021 at 08:44):I would make it an option
Pierre-Marie Pédrot (Mar 31 2021 at 08:44):I agree we have to do something about the current situation
Pierre-Marie Pédrot (Mar 31 2021 at 08:44):but it's going to be very very painful in any case
Matthieu Sozeau (Mar 31 2021 at 08:44):It needs the constant to make expand work, so if there is no constant, expand_projection will return None or raise
Pierre-Marie Pédrot (Mar 31 2021 at 08:45):but a lot of code doesn't use expand projection at all
Pierre-Marie Pédrot (Mar 31 2021 at 08:45):and this is the stuff that is the major source of bugs
Pierre-Marie Pédrot (Mar 31 2021 at 08:45):like, just look at constr_matching
Matthieu Sozeau (Mar 31 2021 at 08:45):That's what I'm looking at
Pierre-Marie Pédrot (Mar 31 2021 at 08:46):in PApp / App case we don't rely on expansion
Pierre-Marie Pédrot (Mar 31 2021 at 08:46):just on the projection as a constant
Pierre-Marie Pédrot (Mar 31 2021 at 08:46):all calls to Projection.constant are code smell
Pierre-Marie Pédrot (Mar 31 2021 at 08:47):but these are not the only examples
Matthieu Sozeau (Mar 31 2021 at 08:47):Yes, but there will be no constant, again, so ocaml will tell me about this.
Pierre-Marie Pédrot (Mar 31 2021 at 08:47):you mean you want to change the API?
Pierre-Marie Pédrot (Mar 31 2021 at 08:47):so that it returns an option.
Matthieu Sozeau (Mar 31 2021 at 08:47):Yes!
Pierre-Marie Pédrot (Mar 31 2021 at 08:48):but then it's highly problematic from the kernel point of view
Matthieu Sozeau (Mar 31 2021 at 08:48):Why?
Pierre-Marie Pédrot (Mar 31 2021 at 08:48):because the constant-projection relation is meaningless in the kernel
Pierre-Marie Pédrot (Mar 31 2021 at 08:48):we define the projection outside
Pierre-Marie Pédrot (Mar 31 2021 at 08:48):at the time the projection is defined in the kernel, we don't even know whether it will have a corresponding constant defined
Pierre-Marie Pédrot (Mar 31 2021 at 08:49):that means that you should define this association map outside of the kernel
Pierre-Marie Pédrot (Mar 31 2021 at 08:50):and it's not going to be part of the projection anymore (which is a good thing)
Pierre-Marie Pédrot (Mar 31 2021 at 08:50):but then we'll get a lot of room for state desynchronization
Pierre-Marie Pédrot (Mar 31 2021 at 08:50):I think somebody (@Gaëtan Gilbert maybe?) tried to write a PR for that already?
Matthieu Sozeau (Mar 31 2021 at 08:52):Ok, fair point. We could live with an API where when you build the projection you are allowed to optionally pass a constant, no? And then just the higher layers need to know about it
Pierre-Marie Pédrot (Mar 31 2021 at 08:52):(in any case, you should assign https://github.com/coq/coq/pull/14033 and merge it)
Matthieu Sozeau (Mar 31 2021 at 08:52):I'm waiting for metacoq's CI to pass, I re-ran it
Pierre-Marie Pédrot (Mar 31 2021 at 08:53):but still, I am very afraid that adding such a mode will only make the situation worse
Pierre-Marie Pédrot (Mar 31 2021 at 08:53):because it means introducing more bugs
Pierre-Marie Pédrot (Mar 31 2021 at 08:53):the kind of hard to realize they are bugs
Pierre-Marie Pédrot (Mar 31 2021 at 08:54):(especially when printing tricks you 99% of the time)
Matthieu Sozeau (Mar 31 2021 at 08:55):I don't see why we would get more bugs. We should just be exercising a subset of the code paths of today
Pierre-Marie Pédrot (Mar 31 2021 at 08:56):this will introduce more discrepancy, and we will get users relying on these discrepancies
Matthieu Sozeau (Mar 31 2021 at 08:57):And there would be no more confusion possible in this mode: a projection name refers to a single object and is always printed the same
Matthieu Sozeau (Mar 31 2021 at 08:58):I'm afraid we have to introduce discrepancy with the compatibility mode otherwise we're stuck
Pierre-Marie Pédrot (Mar 31 2021 at 08:58):given that the last time somebody tried to introduce a GProj node and failed miserably, I have a hard time having faith in your claims
Pierre-Marie Pédrot (Mar 31 2021 at 08:58):but we must try
Pierre-Marie Pédrot (Mar 31 2021 at 08:59):I agree that we must get the situation moving
Matthieu Sozeau (Mar 31 2021 at 08:59):Let's see what Gaëtan (and Hugo?) think about this proposal first.
Pierre-Marie Pédrot (Mar 31 2021 at 08:59):just expect it to be (at least temporarily) worse
Matthieu Sozeau (Mar 31 2021 at 09:00):Sure
Gaëtan Gilbert (Mar 31 2021 at 10:40):IMO the first step of making progress with projections is to get Projection.constant out of the kernel
the kernel only uses it for transparent state stuff IIRC
so it means adding transparent state for projections, and in the higher layers where we change the state make sure to change the projection's state when we change the constant
Gaëtan Gilbert (Mar 31 2021 at 10:41):then once Projection.constant is out of the kernel we can look into making it return option
Pierre-Marie Pédrot (Mar 31 2021 at 10:53):Did I dream or you already wrote a similar PR as mentioned above?
Gaëtan Gilbert (Mar 31 2021 at 10:56):I think I lost motivation halfway when writing it
Pierre-Marie Pédrot (Mar 31 2021 at 11:01):This is not very conforting
Hugo Herbelin (Jul 26 2021 at 18:52):PR #14706 is starting to explore what happens when we let the path CProj/GProj/Proj and the path Const(cst) (for cst satisfying Structures.PrimitiveProjections.mem cst) remain autonomous. This leads to about 25 tests failing (but maybe only 4 or 5 different issues: coercions/canonical-structure, unification, notations, printing, ...).
I started to fix e.g. the following problems:
w_unify) would not unify two different presentations of the projections (but I don't know which)However, I'm unsure about the model we want:
Const, e.g. for partial application, and the Proj for the compact representation, i.e. exit the unfold flag?It seems that the opacity of a projection is often used in reduction. Shall we need to support that a projection is added to a transparency state, even when it is represented as a Proj?
What were otherwise the typical problems in the past?
Last updated: Dec 05 2023 at 06:01 UTC