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.
Expect trouble.
That would most likely mean adding a ProjRef
to global_reference
as well
Most likely we will end up having to add another flag afterwards because we forgot to tweak some transitive behaviour
I believe that the moral of the primitive debacle is precisely that stacking piles of compatibility options is a recipe for disaster
?
like, how are you sure that you successfully deactivated all compatibility code?
there is a lot of it
and in some places it's hard to realize that something is buggy
Well, these projections won't have an expand
function
yes but all the stuff with goal matching, hint patterns and the like?
there is a crapload of code that tries to emulate compatibility
not just expansion to a constant
Nothing special to do there, these rely on expand
??
no no, we store the constant in the projection name
But in the new mode, there will be no constant
the code doesn't give a shit if the constant actually exists
I would make it an option
I agree we have to do something about the current situation
but it's going to be very very painful in any case
It needs the constant to make expand
work, so if there is no constant, expand_projection will return None or raise
but a lot of code doesn't use expand projection at all
and this is the stuff that is the major source of bugs
like, just look at constr_matching
That's what I'm looking at
in PApp / App case we don't rely on expansion
just on the projection as a constant
all calls to Projection.constant are code smell
but these are not the only examples
Yes, but there will be no constant, again, so ocaml will tell me about this.
you mean you want to change the API?
so that it returns an option.
Yes!
but then it's highly problematic from the kernel point of view
Why?
because the constant-projection relation is meaningless in the kernel
we define the projection outside
at the time the projection is defined in the kernel, we don't even know whether it will have a corresponding constant defined
that means that you should define this association map outside of the kernel
and it's not going to be part of the projection anymore (which is a good thing)
but then we'll get a lot of room for state desynchronization
I think somebody (@Gaëtan Gilbert maybe?) tried to write a PR for that already?
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
(in any case, you should assign https://github.com/coq/coq/pull/14033 and merge it)
I'm waiting for metacoq's CI to pass, I re-ran it
but still, I am very afraid that adding such a mode will only make the situation worse
because it means introducing more bugs
the kind of hard to realize they are bugs
(especially when printing tricks you 99% of the time)
I don't see why we would get more bugs. We should just be exercising a subset of the code paths of today
this will introduce more discrepancy, and we will get users relying on these discrepancies
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
I'm afraid we have to introduce discrepancy with the compatibility mode otherwise we're stuck
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
but we must try
I agree that we must get the situation moving
Let's see what Gaëtan (and Hugo?) think about this proposal first.
just expect it to be (at least temporarily) worse
Sure
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
then once Projection.constant is out of the kernel we can look into making it return option
Did I dream or you already wrote a similar PR as mentioned above?
I think I lost motivation halfway when writing it
This is not very conforting
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: May 28 2023 at 16:30 UTC