Kernel sort polymorphism #17836

SkySkimmer · 2023-07-10T13:00:03Z

Depends:

Rebuild case info in nativenorm #18036

Binder syntax is Definition foo@{sort_vars | univ_vars | univ_constraints} := ..., if there is only one | it means no sort variables (ie backwards compatible syntax).
Instance syntax is foo@{sort_vars | univ_vars}.

Sort polymorphic declarations need universe polymorphism to be on.

All non-named sort variables get collapsed, so sort poly is always explicit (although note that Unset Strict Universe Declaration works for qvars too, so Definition foo := Type@{s | u} is sort poly).

Inductives with sort poly output in a future PR (notably this means mind_relevance is constant)

There is no variance for sort variables, so eg with (once sort poly inductives fully work)

Inductive prod@{s | u v |} (A:Type@{s | u}) (B@{s | v}) : Type@{s | max(u,v)} := pair : A -> B -> prod A B.

prod@{Prop | Set Set} True True and prod@{Type | Set Set} True True are not convertible.
Not clear what the consequences are either way, I think we need them to be non convertible if we want to use the explicit instanciation to avoid extraction issues but it may prevent replacing template poly with sort poly.
It should be easier to add variance later if we want it than removing it if we don't want it so let's start without it.

TODO:

doc, changelog
native compile
sort variable unification doesn't handle named variables properly (if we get a problem QVar q = QVar q' it will try q := q', if q is named it will fail, the failure is incorrect if q' is anonymous such that q' := q would have been possible)

Set Universe Polymorphism.

Definition zog@{s| |} (A:Type@{s|Set}) := A.

Definition zig@{s| |} A := zog@{s|} A.

Definition zag@{s| |} (A:Type@{s|Set}) := zog A.

inductives
tests for inductives
overlays

Nice to have but maybe for another PR:

nicer API for sort variable unification error (currently when we fail to unify q1 and q2 we generate a univ inconsistency between Type@{q1|Set} and Type@{q2|Set})

Overlays:

SkySkimmer · 2023-07-10T13:01:07Z

@coqbot bench

coqbot-app · 2023-07-10T21:09:05Z

🏁 Bench results:

┌────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┐
│                            │      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-engine-bench-lite │  157.49   157.37   0.08 │   670107482293    670079609734   0.00 │  1268864959236   1259420684115   0.75 │ 1207292  1207132    0.01 │
│                   coq-core │  116.55   116.39   0.14 │   466180741280    460565464644   1.22 │   491436075184    488410071765   0.62 │  372128   371688    0.12 │
│                   coq-corn │  783.71   779.51   0.54 │  3535917207783   3517309598461   0.53 │  5552683760987   5485603717066   1.22 │  757408   741740    2.11 │
│ coq-performance-tests-lite │  771.95   766.35   0.73 │  3444512771846   3418932756974   0.75 │  6132700607649   6035211319664   1.62 │ 1669680  1667452    0.13 │
│                coq-bignums │   28.17    27.95   0.79 │   127043278145    125759553473   1.02 │   184243503973    180205663445   2.24 │  486084   482448    0.75 │
│                 coq-stdlib │  415.95   412.50   0.84 │  1770847745859   1749574436692   1.22 │  1463412573229   1445304916597   1.25 │  767944   750868    2.27 │
│                  coq-color │  223.85   221.92   0.87 │   999068388867    990478976847   0.87 │  1473378062785   1456251807314   1.18 │ 1140044  1158168   -1.56 │
│               coq-coqprime │   45.52    45.06   1.02 │   203292851909    201294353962   0.99 │   313468072132    308621228972   1.57 │  775360   775716   -0.05 │
│                  coq-verdi │   47.07    46.52   1.18 │   211752355140    209565368274   1.04 │   323796141695    318596029681   1.63 │  526256   526436   -0.03 │
│             coq-verdi-raft │  562.09   555.36   1.21 │  2551401354566   2521515727092   1.19 │  3997249918384   3951018047504   1.17 │  819536   810944    1.06 │
│              coq-fiat-core │   58.81    58.09   1.24 │   249290015739    247165076698   0.86 │   366295826033    365494762472   0.22 │  487320   488516   -0.24 │
│                coq-coqutil │   38.66    38.16   1.31 │   172059829479    170080799906   1.16 │   250005482395    246874957463   1.27 │  558512   558388    0.02 │
│           coq-math-classes │   85.68    84.48   1.42 │   385037367573    378744376960   1.66 │   542317331073    535037551843   1.36 │  519212   517008    0.43 │
│           coq-fiat-parsers │  330.54   325.77   1.46 │  1459682771110   1438007121606   1.51 │  2450196105411   2413989524534   1.50 │ 2417840  2415316    0.10 │
│                    coq-vst │  864.65   849.71   1.76 │  3900051574735   3828723072489   1.86 │  6489130912377   6351464603365   2.17 │ 1877960  2160128  -13.06 │
│               coq-compcert │  288.32   282.63   2.01 │  1289835926286   1264893110216   1.97 │  1974503002706   1950970964310   1.21 │ 1119132  1125024   -0.52 │
│          coq-iris-examples │  486.66   476.63   2.10 │  2197292323496   2151917119377   2.11 │  3388118291862   3311024660208   2.33 │ 1065836  1053848    1.14 │
│               coq-bedrock2 │  290.84   284.81   2.12 │  1310794429274   1282721944646   2.19 │  2588320091259   2508505622347   3.18 │  789500   784744    0.61 │
│              coq-perennial │ 5999.98  5854.74   2.48 │ 27189164930643  26506268964391   2.58 │ 45622901793702  44347189924543   2.88 │ 2224116  2224056    0.00 │
│                coq-unimath │ 1570.75  1531.51   2.56 │  7125030068789   6938534747584   2.69 │ 13548775012231  13067191326780   3.69 │ 1422892  1326020    7.31 │
└────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
coq-hott
coq-mathcomp-ssreflect (dependency install failed in NEW)
coq-equations
coq-rewriter

coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-algebra (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-solvable (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-field (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-character (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-odd-order (dependency coq-mathcomp-ssreflect failed)
coq-metacoq-template (dependency coq-equations failed)
coq-metacoq-pcuic (dependency coq-equations failed)
coq-metacoq-safechecker (dependency coq-equations failed)
coq-metacoq-erasure (dependency coq-equations failed)
coq-metacoq-translations (dependency coq-equations failed)
coq-geocoq (dependency coq-mathcomp-ssreflect failed)
coq-fiat-crypto-with-bedrock (dependency coq-rewriter failed)
coq-coquelicot (dependency coq-mathcomp-ssreflect failed)
coq-fourcolor (dependency coq-mathcomp-ssreflect failed)
coq-rewriter-perf-SuperFast (dependency coq-rewriter failed)
coq-category-theory (dependency coq-equations failed)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                     TOP 25 SLOW DOWNS                                                     │
│                                                                                                                           │
│   OLD       NEW      DIFF   %DIFF    Ln                  FILE                                                             │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 142.5400  149.3610  6.8210   4.79%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html   │
│  24.1850   27.8100  3.6250  14.99%   618  coq-perennial/src/program_proof/simplepb/pb_applybackup_proof.v.html            │
│  20.0350   23.3340  3.2990  16.47%   269  coq-perennial/src/program_proof/memkv/memkv_coord_start_proof.v.html            │
│  45.7470   48.6590  2.9120   6.37%  1002  coq-perennial/src/program_proof/simplepb/pb_apply_proof.v.html                  │
│  55.2240   58.0160  2.7920   5.06%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                     │
│  31.4420   33.6270  2.1850   6.95%   577  coq-perennial/src/program_proof/simplepb/pb_becomeprimary_proof.v.html          │
│  36.8100   38.9830  2.1730   5.90%   522  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html            │
│  21.5010   23.4300  1.9290   8.97%   420  coq-perennial/src/program_proof/simplepb/pb_setstate_proof.v.html               │
│  17.6830   19.5210  1.8380  10.39%   875  coq-perennial/src/program_proof/simple/setattr.v.html                           │
│  31.3890   33.2110  1.8220   5.80%   839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html   │
│  20.4200   22.0290  1.6090   7.88%   808  coq-perennial/src/program_proof/wal/logger_proof.v.html                         │
│  13.3070   14.7980  1.4910  11.20%  1230  coq-perennial/src/program_proof/simplepb/apps/eesm_proof.v.html                 │
│  29.1140   30.6030  1.4890   5.11%  1449  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/KleisliEnriched.v.html │
│  26.7830   28.2160  1.4330   5.35%   824  coq-perennial/src/program_proof/aof/proof.v.html                                │
│  26.7170   28.0650  1.3480   5.05%   898  coq-perennial/src/program_proof/simplepb/admin_proof.v.html                     │
│  24.5140   25.8170  1.3030   5.32%   667  coq-perennial/src/program_proof/simplepb/pb_roapply_proof.v.html                │
│  20.8470   22.1400  1.2930   6.20%   595  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html   │
│  24.9620   26.2360  1.2740   5.10%   373  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html   │
│  20.5940   21.8080  1.2140   5.89%  1357  coq-perennial/src/program_proof/wal/installer_proof.v.html                      │
│   3.2700    4.4530  1.1830  36.18%   901  coq-perennial/src/goose_lang/interpreter/interpreter.v.html                     │
│   5.5520    6.7240  1.1720  21.11%  1391  coq-perennial/src/program_proof/aof/proof.v.html                                │
│  25.8330   26.9070  1.0740   4.16%  2293  coq-perennial/src/goose_lang/logical_reln_fund.v.html                           │
│   6.6540    7.7170  1.0630  15.98%   281  coq-perennial/src/program_proof/memkv/memkv_shard_start_proof.v.html            │
│   9.9300   10.9900  1.0600  10.67%   343  coq-perennial/src/program_proof/simplepb/pb_getstate_proof.v.html               │
│  27.6300   28.6610  1.0310   3.73%   194  coq-vst/veric/expr_lemmas4.v.html                                               │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                           TOP 25 SPEED UPS                                                                           │
│                                                                                                                                                                      │
│   OLD      NEW     DIFF     %DIFF    Ln                          FILE                                                                                                │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  3.1790   2.3870  -0.7920  -24.91%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                                                                     │
│  9.4770   8.7480  -0.7290   -7.69%   192  coq-vst/veric/binop_lemmas5.v.html                                                                                         │
│  7.2670   6.6680  -0.5990   -8.24%  1724  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                                                  │
│  7.6620   7.2010  -0.4610   -6.02%   881  coq-vst/veric/binop_lemmas4.v.html                                                                                         │
│  0.4110   0.0430  -0.3680  -89.54%  1004  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                                                             │
│  0.3990   0.0460  -0.3530  -88.47%   370  coq-perennial/src/program_proof/wal/circ_proof_crash.v.html                                                                │
│  9.4270   9.0770  -0.3500   -3.71%  1020  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                                                             │
│  3.9440   3.6060  -0.3380   -8.57%   154  coq-vst/veric/binop_lemmas5.v.html                                                                                         │
│  3.1400   2.8420  -0.2980   -9.49%   475  coq-vst/veric/binop_lemmas3.v.html                                                                                         │
│  1.4400   1.1750  -0.2650  -18.40%   853  coq-stdlib/FSets/FMapAVL.v.html                                                                                            │
│  3.3770   3.1130  -0.2640   -7.82%   163  coq-vst/veric/Clight_mapsto_memory_block.v.html                                                                            │
│  1.2780   1.0250  -0.2530  -19.80%    88  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html                                                      │
│  1.8280   1.5780  -0.2500  -13.68%   937  coq-vst/veric/binop_lemmas2.v.html                                                                                         │
│  1.2330   1.0220  -0.2110  -17.11%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                                                                                   │
│  3.9680   3.7580  -0.2100   -5.29%     8  coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html                                                            │
│ 14.3580  14.1510  -0.2070   -1.44%   308  coq-perennial/src/Helpers/byte_explode.v.html                                                                              │
│  0.3280   0.1440  -0.1840  -56.10%  1037  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html                                                                         │
│  0.5010   0.3200  -0.1810  -36.13%  1363  coq-stdlib/FSets/FMapAVL.v.html                                                                                            │
│  2.1430   1.9640  -0.1790   -8.35%   209  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                                                   │
│  0.2820   0.1050  -0.1770  -62.77%    61  coq-perennial/src/program_proof/mvcc/index_proof.v.html                                                                    │
│  0.1870   0.0120  -0.1750  -93.58%   361  coq-unimath/UniMath/CategoryTheory/Monoidal/AlternativeDefinitions/EquivalenceWhiskeredNonCurriedMonoidalCategories.v.html │
│  0.4540   0.2800  -0.1740  -38.33%   860  coq-stdlib/FSets/FMapAVL.v.html                                                                                            │
│  0.3410   0.1710  -0.1700  -49.85%   498  coq-color/Term/Lambda/LCompClos.v.html                                                                                     │
│  0.2560   0.0880  -0.1680  -65.62%  1097  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html                                                                         │
│  0.1680   0.0040  -0.1640  -97.62%    90  coq-perennial/src/program_proof/txn/wrapper_init_proof.v.html                                                              │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

SkySkimmer · 2023-07-11T12:34:32Z

@coqbot bench

SkySkimmer · 2023-07-11T14:13:49Z

@coqbot bench

coqbot-app · 2023-07-11T22:40:45Z

🏁 Bench results:

┌────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬──────────────────────────┐
│                            │      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-engine-bench-lite │  157.99   159.54  -0.97 │   672272686366    678363282611  -0.90 │  1265882421967   1261853677379   0.32 │ 1100480  1207044   -8.83 │
│ coq-performance-tests-lite │  768.10   765.21   0.38 │  3426060124212   3410612052073   0.45 │  6137025011565   6041114256221   1.59 │ 1667992  1665732    0.14 │
│                   coq-corn │  783.31   779.61   0.47 │  3532529232176   3517573002680   0.43 │  5563321352022   5491042795754   1.32 │  789604   741628    6.47 │
│                   coq-core │  116.41   115.38   0.89 │   469523020134    473267658735  -0.79 │   491601115200    488237632649   0.69 │  372596   371104    0.40 │
│             coq-verdi-raft │  561.69   556.02   1.02 │  2546422364513   2521553266666   0.99 │  4003971481563   3958241149858   1.16 │  821488   811476    1.23 │
│                coq-coqutil │   39.37    38.97   1.03 │   175362094140    172827266182   1.47 │   252956674964    249853891391   1.24 │  558708   558276    0.08 │
│              coq-fiat-core │   59.61    58.98   1.07 │   253137182341    250325843223   1.12 │   371783712535    370793478089   0.27 │  488896   489608   -0.15 │
│           coq-fiat-parsers │  332.71   329.03   1.12 │  1466694863719   1449711795126   1.17 │  2461371023346   2431168052915   1.24 │ 2424612  2736736  -11.40 │
│               coq-compcert │  288.00   284.19   1.34 │  1289648606030   1272111059552   1.38 │  1979157747759   1955734980340   1.20 │ 1126308  1127472   -0.10 │
│               coq-coqprime │   45.87    45.22   1.44 │   205548892682    201552836979   1.98 │   315312432849    310156683053   1.66 │  776476   775136    0.17 │
│               coq-bedrock2 │  291.94   286.35   1.95 │  1316376501407   1290821120147   1.98 │  2593100097379   2511475027498   3.25 │  784716   789216   -0.57 │
│           coq-math-classes │   87.12    85.29   2.15 │   389501796175    381355220187   2.14 │   545854773261    538589382271   1.35 │  520056   518400    0.32 │
│                  coq-verdi │   47.40    46.38   2.20 │   212391138681    208207698495   2.01 │   325201656749    319974404280   1.63 │  526072   524864    0.23 │
│                    coq-vst │  874.00   855.11   2.21 │  3943237782838   3850605452882   2.41 │  6505542451002   6353494243745   2.39 │ 1935584  2158004  -10.31 │
│                  coq-color │  227.27   222.23   2.27 │  1016089154286    991774789137   2.45 │  1480412104481   1462881646959   1.20 │ 1142196  1157680   -1.34 │
│                coq-unimath │ 1568.99  1532.54   2.38 │  7109530856224   6943196540533   2.40 │ 13573208977903  13090545695009   3.69 │ 1423940  1328116    7.22 │
│          coq-iris-examples │  490.12   477.95   2.55 │  2212186128564   2155389031024   2.64 │  3392531275549   3313652389306   2.38 │ 1063108  1055268    0.74 │
│                 coq-stdlib │  418.51   407.90   2.60 │  1781164047534   1735576689954   2.63 │  1463545120425   1445097495367   1.28 │  767844   752232    2.08 │
│                coq-bignums │   28.50    27.73   2.78 │   127878373213    125647269129   1.78 │   184146421335    180161722596   2.21 │  482344   484252   -0.39 │
│              coq-perennial │ 6046.35  5853.34   3.30 │ 27391459464464  26507994248117   3.33 │ 45649139141113  44355614286716   2.92 │ 2226004  2219416    0.30 │
│                   coq-hott │  155.62   148.59   4.73 │   696158337039    665015999787   4.68 │  1112275361504   1057955167379   5.13 │  581320   622424   -6.60 │
└────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
coq-mathcomp-ssreflect (dependency install failed in NEW)
coq-equations
coq-rewriter

coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-algebra (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-solvable (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-field (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-character (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-odd-order (dependency coq-mathcomp-ssreflect failed)
coq-metacoq-template (dependency coq-equations failed)
coq-metacoq-pcuic (dependency coq-equations failed)
coq-metacoq-safechecker (dependency coq-equations failed)
coq-metacoq-erasure (dependency coq-equations failed)
coq-metacoq-translations (dependency coq-equations failed)
coq-geocoq (dependency coq-mathcomp-ssreflect failed)
coq-fiat-crypto-with-bedrock (dependency coq-rewriter failed)
coq-coquelicot (dependency coq-mathcomp-ssreflect failed)
coq-fourcolor (dependency coq-mathcomp-ssreflect failed)
coq-rewriter-perf-SuperFast (dependency coq-rewriter failed)
coq-category-theory (dependency coq-equations failed)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                    TOP 25 SLOW DOWNS                                                    │
│                                                                                                                         │
│   OLD       NEW      DIFF   %DIFF    Ln                 FILE                                                            │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 141.8220  149.3840  7.5620   5.33%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │
│  24.1860   27.6240  3.4380  14.21%   618  coq-perennial/src/program_proof/simplepb/pb_applybackup_proof.v.html          │
│  20.5560   23.2010  2.6450  12.87%   269  coq-perennial/src/program_proof/memkv/memkv_coord_start_proof.v.html          │
│  45.8200   47.9670  2.1470   4.69%  1002  coq-perennial/src/program_proof/simplepb/pb_apply_proof.v.html                │
│  31.2790   33.1460  1.8670   5.97%   839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │
│  21.4470   23.2140  1.7670   8.24%   420  coq-perennial/src/program_proof/simplepb/pb_setstate_proof.v.html             │
│  17.5540   19.3110  1.7570  10.01%   875  coq-perennial/src/program_proof/simple/setattr.v.html                         │
│  55.8200   57.4480  1.6280   2.92%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                   │
│  13.1980   14.7650  1.5670  11.87%  1230  coq-perennial/src/program_proof/simplepb/apps/eesm_proof.v.html               │
│  46.3600   47.8860  1.5260   3.29%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html               │
│  20.5190   21.9530  1.4340   6.99%  1357  coq-perennial/src/program_proof/wal/installer_proof.v.html                    │
│  31.4150   32.8240  1.4090   4.49%   577  coq-perennial/src/program_proof/simplepb/pb_becomeprimary_proof.v.html        │
│  24.4020   25.7630  1.3610   5.58%   667  coq-perennial/src/program_proof/simplepb/pb_roapply_proof.v.html              │
│  37.1160   38.4300  1.3140   3.54%   522  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html          │
│  20.8390   22.1280  1.2890   6.19%   595  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │
│  27.0090   28.2260  1.2170   4.51%   824  coq-perennial/src/program_proof/aof/proof.v.html                              │
│   6.7040    7.8950  1.1910  17.77%   281  coq-perennial/src/program_proof/memkv/memkv_shard_start_proof.v.html          │
│  26.9390   28.1030  1.1640   4.32%   898  coq-perennial/src/program_proof/simplepb/admin_proof.v.html                   │
│  24.9730   26.1030  1.1300   4.52%   373  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │
│   8.5530    9.6710  1.1180  13.07%  1508  coq-perennial/src/program_proof/wal/recovery_proof.v.html                     │
│   3.3790    4.4130  1.0340  30.60%   901  coq-perennial/src/goose_lang/interpreter/interpreter.v.html                   │
│  20.4380   21.4660  1.0280   5.03%   808  coq-perennial/src/program_proof/wal/logger_proof.v.html                       │
│  33.4440   34.4700  1.0260   3.07%    97  coq-vst/veric/binop_lemmas5.v.html                                            │
│   8.4150    9.4400  1.0250  12.18%   350  coq-perennial/src/program_proof/simple/read.v.html                            │
│  18.2700   19.2910  1.0210   5.59%  1286  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SPEED UPS                                                           │
│                                                                                                                                      │
│   OLD       NEW      DIFF     %DIFF    Ln                   FILE                                                                     │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 131.1530  129.9870  -1.1660   -0.89%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html          │
│ 131.3630  130.3830  -0.9800   -0.75%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html          │
│  63.3250   62.4090  -0.9160   -1.45%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                             │
│  41.9980   41.1510  -0.8470   -2.02%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html           │
│   7.2810    6.6620  -0.6190   -8.50%  1724  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                │
│   7.7800    7.2170  -0.5630   -7.24%   881  coq-vst/veric/binop_lemmas4.v.html                                                       │
│  21.6410   21.1910  -0.4500   -2.08%  1495  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/UnivalentKleisliEnriched.v.html │
│   1.2570    0.8890  -0.3680  -29.28%   382  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                             │
│   4.1750    3.8280  -0.3470   -8.31%   125  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                             │
│   4.7660    4.4250  -0.3410   -7.15%   102  coq-engine-bench-lite/coq/PerformanceDemos/rewrite_strat_repeated_app.v.html             │
│  16.2280   15.9220  -0.3060   -1.89%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                │
│   1.4250    1.1240  -0.3010  -21.12%   853  coq-stdlib/FSets/FMapAVL.v.html                                                          │
│   2.5050    2.2050  -0.3000  -11.98%  1383  coq-perennial/src/program_proof/aof/proof.v.html                                         │
│   0.5740    0.2780  -0.2960  -51.57%   301  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html                                      │
│   0.4550    0.1640  -0.2910  -63.96%   925  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                           │
│   1.2910    1.0060  -0.2850  -22.08%    88  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html                    │
│   0.6980    0.4190  -0.2790  -39.97%   870  coq-stdlib/MSets/MSetRBT.v.html                                                          │
│   3.9820    3.7130  -0.2690   -6.76%     8  coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html                          │
│   4.3700    4.1160  -0.2540   -5.81%   128  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                             │
│  33.2040   32.9560  -0.2480   -0.75%  1730  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                          │
│   1.8670    1.6270  -0.2400  -12.85%   937  coq-vst/veric/binop_lemmas2.v.html                                                       │
│   0.7620    0.5230  -0.2390  -31.36%  2052  coq-stdlib/FSets/FMapFacts.v.html                                                        │
│   1.4610    1.2320  -0.2290  -15.67%   372  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                             │
│   9.2670    9.0440  -0.2230   -2.41%  1020  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                           │
│   0.7640    0.5420  -0.2220  -29.06%   422  coq-stdlib/MSets/MSetList.v.html                                                         │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

coqbot-app · 2023-08-31T02:08:50Z

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

JasonGross · 2023-09-06T14:53:14Z

Not clear what the consequences are either way, I think we need them to be non convertible if we want to use the explicit instanciation to avoid extraction issues but it may prevent replacing template poly with sort poly.

Sort polymorphic cumulativity could be guarded behind a flag like polymorphic indicative cumulativity, and the flag could emit a warning that this setting may result in broken extraction (though it's not clear to me what would break), right? Then we should be able to replace template poly with sort poly without risking extraction any more than we already do.

coqbot-app · 2023-11-06T15:43:01Z

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

ppedrot · 2023-11-06T20:43:25Z

Let's merge, this has waited long enough. @coqbot merge now

coqbot-app · 2023-11-06T20:43:29Z

@ppedrot: Please take care of the following overlays:

17836-SkySkimmer-sort-poly.sh

Adapt to coq/coq#17836 (sort poly)

yannl35133 · 2023-11-07T13:41:01Z

engine/univNames.mli

-val pr_with_global_universes : ?binders:universe_binders -> Level.t -> Pp.t
+type full_name_list = lname list * lname list
+
+val pr_level_with_global_universes : ?binders:universe_binders -> Level.t -> Pp.t


coq/kernel/univ.mli

Lines 57 to 58 in 1e74738

val pr : t -> Pp.t

[@@deprecated "Use [UnivNames.pr_with_global_universes] instead if possible, otherwise [raw_pr]."]

The name change was not reflected there

Adapt to coq/coq#17836 (sort poly)

SkySkimmer added needs: progress Work in progress: awaiting action from the author. kind: feature New user-facing feature request or implementation. part: universes The universe system. labels Jul 10, 2023

SkySkimmer added this to the 8.19+rc1 milestone Jul 10, 2023

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jul 10, 2023

coq deleted a comment from coqbot-app bot Jul 10, 2023

SkySkimmer force-pushed the sort-poly branch from 34fb7c5 to 3d27afc Compare July 11, 2023 12:34

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jul 11, 2023

SkySkimmer force-pushed the sort-poly branch from 3d27afc to 0cf909b Compare July 11, 2023 14:08

coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jul 11, 2023

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Aug 1, 2023

coqbot-app bot added the stale This PR will be closed unless it is rebased. label Aug 31, 2023

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 6, 2023

SkySkimmer force-pushed the sort-poly branch from 0cf909b to f456cbd Compare September 6, 2023 14:37

coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. stale This PR will be closed unless it is rebased. request: full CI Use this label when you want your next push to trigger a full CI. labels Sep 6, 2023

SkySkimmer mentioned this pull request Sep 7, 2023

Memory issue math-comp/math-comp#1059

Merged

4 tasks

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 7, 2023

SkySkimmer force-pushed the sort-poly branch from f456cbd to 8a072b5 Compare September 7, 2023 12:49

coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Sep 7, 2023

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Nov 6, 2023

SkySkimmer force-pushed the sort-poly branch from b916076 to c27ba97 Compare November 6, 2023 10:23

coqbot-app bot removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. request: full CI Use this label when you want your next push to trigger a full CI. labels Nov 6, 2023

coqbot-app bot merged commit 986eaae into coq:master Nov 6, 2023
5 of 8 checks passed

ppedrot added a commit to coq-community/coq-dpdgraph that referenced this pull request Nov 6, 2023

Merge pull request #123 from SkySkimmer/sort-poly

85660ac

Adapt to coq/coq#17836 (sort poly)

ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request Nov 6, 2023

Merge pull request #562 from SkySkimmer/sort-poly

dbc5fbb

Adapt to coq/coq#17836 (sort poly)

ppedrot added a commit to MetaCoq/metacoq that referenced this pull request Nov 6, 2023

Merge pull request #984 from SkySkimmer/sort-poly

472ac7b

Adapt to coq/coq#17836 (sort poly)

ppedrot added a commit to coq-community/paramcoq that referenced this pull request Nov 6, 2023

Merge pull request #114 from SkySkimmer/sort-poly

2d25c4c

Adapt to coq/coq#17836 (sort poly)

SkySkimmer added a commit to SkySkimmer/QuickChick that referenced this pull request Nov 6, 2023

Adapt to coq/coq#17836 (sort poly)

6621d65

SkySkimmer added a commit to SkySkimmer/rewriter that referenced this pull request Nov 6, 2023

Adapt to coq/coq#17836 (sort poly)

246791a

SkySkimmer added a commit to SkySkimmer/coqutil that referenced this pull request Nov 6, 2023

Adapt to coq/coq#17836 (sort poly)

97fec61

ppedrot added a commit to ejgallego/coq-serapi that referenced this pull request Nov 6, 2023

Merge pull request #358 from SkySkimmer/sort-poly

4bbd657

Adapt to coq/coq#17836 (sort poly)

LasseBlaauwbroek added a commit to coq-tactician/coq-tactician that referenced this pull request Nov 6, 2023

Merge pull request #65 from SkySkimmer/sort-poly

3db75ac

Adapt to coq/coq#17836 (sort poly)

samuelgruetter mentioned this pull request Nov 6, 2023

Adapt to coq/coq#17836 (sort poly) mit-plv/coqutil#95

Closed

JasonGross pushed a commit to mit-plv/rewriter that referenced this pull request Nov 6, 2023

Adapt to coq/coq#17836 (sort poly) (#109)

5e74224

JasonGross mentioned this pull request Nov 7, 2023

Reformulating the grammar of rewstrategy with GRAMMAR EXTEND #17832

Merged

1 task

jim-portegies pushed a commit to impermeable/coq-waterproof that referenced this pull request Nov 7, 2023

Adapt to coq/coq#17836 (sort poly) (#28)

a333601

SkySkimmer deleted the sort-poly branch November 7, 2023 09:09

Janno added a commit to unicoq/unicoq that referenced this pull request Nov 7, 2023

Merge pull request #85 from SkySkimmer/sort-poly

d7b2812

Adapt to coq/coq#17836 (sort poly)

ejgallego pushed a commit to SkySkimmer/coq-lsp that referenced this pull request Nov 7, 2023

[upstream] Adapt to coq/coq#17836 (sort poly)

4cd466e

ejgallego pushed a commit to SkySkimmer/coq-lsp that referenced this pull request Nov 7, 2023

[upstream] Adapt to coq/coq#17836 (sort poly)

ce3f9f5

ejgallego added a commit to ejgallego/coq-lsp that referenced this pull request Nov 7, 2023

Merge pull request #549 from SkySkimmer/sort-poly

53e12d3

Adapt to coq/coq#17836 (sort poly)

yannl35133 reviewed Nov 7, 2023

View reviewed changes

lukaszcz pushed a commit to lukaszcz/coqhammer that referenced this pull request Nov 7, 2023

Adapt to coq/coq#17836 (sort poly)

3b59f1e

Janno added a commit to Mtac2/Mtac2 that referenced this pull request Nov 8, 2023

Merge pull request #392 from SkySkimmer/sort-poly

afc6ee3

Adapt to coq/coq#17836 (sort poly)

liyishuai pushed a commit to QuickChick/QuickChick that referenced this pull request Nov 8, 2023

Adapt to coq/coq#17836 (sort poly)

802d3e6

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Kernel sort polymorphism #17836

Kernel sort polymorphism #17836

SkySkimmer commented Jul 10, 2023 •

edited

SkySkimmer commented Jul 10, 2023

coqbot-app bot commented Jul 10, 2023

SkySkimmer commented Jul 11, 2023

SkySkimmer commented Jul 11, 2023

coqbot-app bot commented Jul 11, 2023

coqbot-app bot commented Aug 31, 2023

JasonGross commented Sep 6, 2023 •

edited

coqbot-app bot commented Nov 6, 2023

ppedrot commented Nov 6, 2023

coqbot-app bot commented Nov 6, 2023

yannl35133 Nov 7, 2023

	val pr : t -> Pp.t
	[@@deprecated "Use [UnivNames.pr_with_global_universes] instead if possible, otherwise [raw_pr]."]

Kernel sort polymorphism #17836

Kernel sort polymorphism #17836

Conversation

SkySkimmer commented Jul 10, 2023 • edited

SkySkimmer commented Jul 10, 2023

coqbot-app bot commented Jul 10, 2023

SkySkimmer commented Jul 11, 2023

SkySkimmer commented Jul 11, 2023

coqbot-app bot commented Jul 11, 2023

coqbot-app bot commented Aug 31, 2023

JasonGross commented Sep 6, 2023 • edited

coqbot-app bot commented Nov 6, 2023

ppedrot commented Nov 6, 2023

coqbot-app bot commented Nov 6, 2023

yannl35133 Nov 7, 2023

Choose a reason for hiding this comment

SkySkimmer commented Jul 10, 2023 •

edited

JasonGross commented Sep 6, 2023 •

edited