Stream: Coq devs & plugin devs

Topic: Duplicate universes when declaring constans


view this post on Zulip Enrico Tassi (Jul 04 2022 at 09:27):

I'm fighting against Environ.add_universes which complains if the universe is already there. The are similar APIs which don't fail in that case as well as other places where the system is "lenient" because some components push universe more than once.

I'm in that situation, I've a single evar map out of which I declare multiple constants. I'm now trying to make them universe polymorphic, but I clash with that API. So I'd like to understand what the problem really is, why the API is complaining about universes and so on.

I'm open to any solution (other than having multiple evar maps) but I'm on a stable Coq, so I can't tweak the APIs (although I'm fine writing code for nex Coq)

view this post on Zulip Gaëtan Gilbert (Jul 04 2022 at 10:06):

Environ.add_universes

I don't know that function, where is it?
Can you link your code attempt?

view this post on Zulip Enrico Tassi (Jul 04 2022 at 11:17):

Sorry the public API is Environ.push_context which internally calls add_universes.
The code sample is a bit messy, it is shit branch https://github.com/LPCIC/coq-elpi/pull/315 of coq-elpi, against 8.16rc1. The file which fails is apps/locker/tests/test_locker.v

view this post on Zulip Enrico Tassi (Jul 04 2022 at 11:19):

That code adds 3 constant, the first one is a proof of unit, then a definition, and then another thing. The definition fails because of a duplicate universe.

Anyway, I'd like to understand what this check is for, and what happens if I remove it. Maybe I'm doing something silly.
In this case the "input" is a univ poly definition which was "typechecked" by Coq, but not added yet to the env. Indeed the command does mangle it, and finally add it. My guess is that the type checking done by coq pushed to sigma stuff which then ends in the env because of the first proof and then boom.

view this post on Zulip Enrico Tassi (Jul 04 2022 at 11:20):

Maybe I should restrict the evar map by hand (and I do for inductives for example) trimming unused things here and there... but really, I'd like to understand which is the intended way of using these APIs

view this post on Zulip Enrico Tassi (Jul 04 2022 at 11:34):

Actually, on my side I do a merge_universe_context after Constrintern.interp_univ_decl_opt on the univ declaration of the definition.

view this post on Zulip Gaëtan Gilbert (Jul 04 2022 at 11:39):

the test is needed to prevent inconsistency https://github.com/coq/coq/pull/8341/commits/eb4171d50d340e19e87a7a592b3d9c0d48654337

view this post on Zulip Pierre-Marie Pédrot (Jul 04 2022 at 11:41):

One has to delineate kernel APIs from upper APIs. In the kernel we must error when sending duplicate universes, but the upper layers could be more lenient and just ignore them. (It's still a code smell though.)

view this post on Zulip Enrico Tassi (Jul 04 2022 at 11:43):

I'll dig a bit more but then I'd really call for a short call with you guys, since I'm calling APIs "at random"

view this post on Zulip Enrico Tassi (Jul 04 2022 at 11:59):

Is there a UState.restriction like which also prunes universe binders? That would be enough for me.
My use case is that an elpi command receives an evar map in which some universe binders are declared, but then it also declares (before) an auxiliary constant which is not even polymorphic, so I restrict the evar map, but that operation does not prune the binder (even if it is not used) so I end up pushing it twice

view this post on Zulip Enrico Tassi (Jul 04 2022 at 12:00):

I do this let sigma = Evd.restrict_universe_context sigma used in

view this post on Zulip Enrico Tassi (Jul 04 2022 at 12:00):

but if u is a binder, and u is not in used then u is still there

view this post on Zulip Gaëtan Gilbert (Jul 04 2022 at 12:06):

the API is not really designed to have an evar map or ustate be used for multiple declarations, we get problems when we try to restrict in obligations too

view this post on Zulip Gaëtan Gilbert (Jul 04 2022 at 12:06):

also side effect stuff

view this post on Zulip Pierre-Marie Pédrot (Jul 04 2022 at 12:07):

+1 but I think this is a fundamental problem somehow, not only an API limitation

view this post on Zulip Gaëtan Gilbert (Jul 04 2022 at 12:07):

IIUC you do

Definition foo@{u} := Type@{u}.
Polymorphic Definition bar := whatever. (* kernel gets the univ of foo in the ucontext for bar *)

?

view this post on Zulip Gaëtan Gilbert (Jul 04 2022 at 12:09):

isn't this what you added demote_global_univs for?

view this post on Zulip Enrico Tassi (Jul 04 2022 at 12:22):

yes

view this post on Zulip Enrico Tassi (Jul 04 2022 at 13:38):

OK, I made it to work with a hammer. I'll open a PR with the APIs I need in master so that you can comment

view this post on Zulip Gaëtan Gilbert (Jul 04 2022 at 13:42):

not sure it makes sense to use restrict for this
suppose you do

Definition foo@{u} := Type@{u}.
Polymorphic Definition bar := Type@{foo.u}.

restrict will do nothing

view this post on Zulip Enrico Tassi (Jul 04 2022 at 13:52):

https://github.com/coq/coq/pull/16280

view this post on Zulip Enrico Tassi (Jul 04 2022 at 13:55):

Technically, I want to elaborate

Definition foo@{u} := ...

to

Definition bar := tt.
Definition foo@{u} := match bar with tt => ... end

and for convenience reasons I start with an evar map which contains u as a binder (since the input data, the definition, asks for so).
So I need a restriction which purges also binders to get a smaller sigma to declare bar, and continue with the pristine map to declare foo.

The other API is because you want to "programmatically" write Definition f@{u}, but you work with levels... not with named levels (by default)

view this post on Zulip Enrico Tassi (Jul 04 2022 at 13:57):

So internally @{u} is @{level.22}. This is only needed until the other change you already did is effective (e.g. don't use names in the API to declare constants/inductives). So part of the API I add is unnecessary (but I can't test it, since I'm on 8.16rc1).

view this post on Zulip Enrico Tassi (Jul 04 2022 at 13:57):

But I still think it makes sense to have.


Last updated: Feb 02 2023 at 13:03 UTC