Enrico Tassi (Jul 04 2022 at 09:27): 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)
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?
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
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.
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
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.
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
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.)
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"
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
Enrico Tassi (Jul 04 2022 at 12:00):I do this let sigma = Evd.restrict_universe_context sigma used in
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
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
Gaëtan Gilbert (Jul 04 2022 at 12:06):also side effect stuff
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
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 *)
?
Gaëtan Gilbert (Jul 04 2022 at 12:09):isn't this what you added demote_global_univs for?
Enrico Tassi (Jul 04 2022 at 12:22):yes
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
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
Enrico Tassi (Jul 04 2022 at 13:52):https://github.com/coq/coq/pull/16280
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)
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).
Enrico Tassi (Jul 04 2022 at 13:57):But I still think it makes sense to have.
Last updated: Sep 09 2024 at 04:02 UTC