Stream: Coq devs & plugin devs

Topic: Primitive Projection mode


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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:40):

Expect trouble.

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:40):

That would most likely mean adding a ProjRef to global_reference as well

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

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

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:41):

?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:42):

like, how are you sure that you successfully deactivated all compatibility code?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:42):

there is a lot of it

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:42):

and in some places it's hard to realize that something is buggy

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:42):

Well, these projections won't have an expand function

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:43):

yes but all the stuff with goal matching, hint patterns and the like?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:43):

there is a crapload of code that tries to emulate compatibility

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:43):

not just expansion to a constant

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:43):

Nothing special to do there, these rely on expand

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:43):

??

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:43):

no no, we store the constant in the projection name

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:44):

But in the new mode, there will be no constant

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:44):

the code doesn't give a shit if the constant actually exists

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:44):

I would make it an option

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:44):

I agree we have to do something about the current situation

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:44):

but it's going to be very very painful in any case

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:45):

but a lot of code doesn't use expand projection at all

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:45):

and this is the stuff that is the major source of bugs

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:45):

like, just look at constr_matching

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:45):

That's what I'm looking at

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:46):

in PApp / App case we don't rely on expansion

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:46):

just on the projection as a constant

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:46):

all calls to Projection.constant are code smell

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:47):

but these are not the only examples

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:47):

Yes, but there will be no constant, again, so ocaml will tell me about this.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:47):

you mean you want to change the API?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:47):

so that it returns an option.

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:47):

Yes!

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:48):

but then it's highly problematic from the kernel point of view

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:48):

Why?

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:48):

because the constant-projection relation is meaningless in the kernel

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:48):

we define the projection outside

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:49):

that means that you should define this association map outside of the kernel

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:50):

but then we'll get a lot of room for state desynchronization

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

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

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

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:52):

I'm waiting for metacoq's CI to pass, I re-ran it

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:53):

because it means introducing more bugs

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:53):

the kind of hard to realize they are bugs

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:54):

(especially when printing tricks you 99% of the time)

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:56):

this will introduce more discrepancy, and we will get users relying on these discrepancies

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

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:58):

I'm afraid we have to introduce discrepancy with the compatibility mode otherwise we're stuck

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

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:58):

but we must try

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:59):

I agree that we must get the situation moving

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:59):

Let's see what Gaëtan (and Hugo?) think about this proposal first.

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 08:59):

just expect it to be (at least temporarily) worse

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 09:00):

Sure

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

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

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

Did I dream or you already wrote a similar PR as mentioned above?

view this post on Zulip Gaëtan Gilbert (Mar 31 2021 at 10:56):

I think I lost motivation halfway when writing it

view this post on Zulip Pierre-Marie Pédrot (Mar 31 2021 at 11:01):

This is not very conforting

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

However, I'm unsure about the model we want:

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: Oct 16 2021 at 07:02 UTC