Directly set universes in the global wrapper.

[ppedrot]

We trust that the set of universes in the evarmap is synchronized with the global environment, which allows setting the constraints in O(1) instead of pushing them in superlinear time. This is seemingly critical for some clients of coq-elpi.

[ppedrot]

(Unfortunately I don't have an easy way to bench mathcomp-analysis without fiddling with Coq bench files.)

[SkySkimmer]

(Unfortunately I don't have an easy way to bench mathcomp-analysis without fiddling with Coq bench files.)

Let's see if we can change that coq/coq#19400

[SkySkimmer]

┌────────────────────────┬────────────────────────┬──────────────────────────────────────┬──────────────────────────────────────┬─────────────────────────┐
│                        │     user time [s]      │              CPU cycles              │           CPU instructions           │  max resident mem [KB]  │
│                        │                        │                                      │                                      │                         │
│      package_name      │  NEW     OLD    PDIFF  │      NEW            OLD       PDIFF  │      NEW            OLD       PDIFF  │   NEW      OLD    PDIFF │
├────────────────────────┼────────────────────────┼──────────────────────────────────────┼──────────────────────────────────────┼─────────────────────────┤
│ coq-mathcomp-ssreflect │ 111.70  138.93  -19.60 │  509871465628   634934882925  -19.70 │  723377884663   920090908746  -21.38 │ 1667708  1667080   0.04 │
│ coq-mathcomp-classical │  61.56   74.01  -16.82 │  278619313727   335361980102  -16.92 │  429116725669   502832470969  -14.66 │ 1455796  1465080  -0.63 │
│     coq-mathcomp-field │ 101.77  111.34   -8.60 │  464642809463   508211124331   -8.57 │  735811138531   800508905731   -8.08 │ 1241412  1240444   0.08 │
│   coq-mathcomp-algebra │ 169.77  182.63   -7.04 │  774633996613   833706881364   -7.09 │ 1185867139116  1278964985214   -7.28 │ 1206292  1283672  -6.03 │
│               coq-elpi │  40.64   42.16   -3.61 │  181545854932   188708274128   -3.80 │  325647997503   340113521363   -4.25 │  523400   521364   0.39 │
│ coq-mathcomp-odd-order │ 553.42  571.15   -3.10 │ 2532825646360  2613420131152   -3.08 │ 3912843248327  4008901163897   -2.40 │ 1644968  1675296  -1.81 │
│  coq-mathcomp-analysis │ 609.68  628.11   -2.93 │ 2785548347174  2869620562684   -2.93 │ 4499730227848  4624086839459   -2.69 │ 1736892  1766888  -1.70 │
│             coq-stdlib │ 344.98  351.83   -1.95 │ 1474719417637  1504824696588   -2.00 │ 1218933761971  1219011461933   -0.01 │  628592   625600   0.48 │
│ coq-mathcomp-character │  89.68   91.43   -1.91 │  410056712809   417255891716   -1.73 │  643462650834   650409045048   -1.07 │ 1016968  1044960  -2.68 │
│  coq-mathcomp-fingroup │  26.23   26.73   -1.87 │  119587529461   121322330452   -1.43 │  175091165003   176249232233   -0.66 │  557996   559992  -0.36 │
│    coq-mathcomp-finmap │  10.45   10.51   -0.57 │   47521832501    47619292872   -0.20 │   67616465469    67723897164   -0.16 │  567788   558940   1.58 │
│               coq-core │ 129.23  129.42   -0.15 │  509633726144   507711855688    0.38 │  536799596231   536635897430    0.03 │  464572   463748   0.18 │
│  coq-mathcomp-solvable │  97.54   97.52    0.02 │  445163494273   445274804976   -0.02 │  675841912841   675214517685    0.09 │  895212   896492  -0.14 │
│            coq-bignums │  29.93   29.69    0.81 │  135826265091   134384429892    1.07 │  192754332881   192671599002    0.04 │  469316   468668   0.14 │
│ coq-mathcomp-bigenough │   0.37    0.36    2.78 │    1465407922     1433717261    2.21 │    2466589421     2466197521    0.02 │  433688   432128   0.36 │
└────────────────────────┴────────────────────────┴──────────────────────────────────────┴──────────────────────────────────────┴─────────────────────────┘

[gares]

I start to think that the best advertisement for Rocq 8.21 will be a bench...

[SkySkimmer]

This change is strictly elpi side though, isn't it compatible with coq 8.19 and 8.20?