Refactor coercionops #13912

pi8027 · 2021-03-08T09:30:07Z

This PR does two things as discussed in #13909 (comment):

replacing Bijint and cl_index with ClTypMap and cl_typ, respectively.
adding the coe_source and coe_target fields of type cl_typ to coe_info_typ so that ML plugins can query the classes from a GlobRef.t of a coercion. The coercion record has been replaced with coe_info_typ since they have the same set of fields.

Kind: cleanup / enhancement.

Added / updated test-suite
Entry added in the changelog (see https://github.com/coq/coq/tree/master/doc/changelog#unreleased-changelog for details).

gares · 2021-03-08T16:02:46Z

I think you need to fix these:

dev/base_include:#install_printer  (* cl_index *) ppclindex;;
dev/top_printers.dbg:install_printer Top_printers.ppclindex
dev/top_printers.ml:let ppclindex cl = pp(Coercionops.pr_cl_index cl)
dev/top_printers.mli:val ppclindex : Coercionops.cl_index -> unit

SkySkimmer · 2021-03-08T16:11:04Z

Bench https://gitlab.com/coq/coq/-/jobs/1080957917

pi8027 · 2021-03-08T17:05:04Z

Fixed dev/base_include and added a changelog entry. I did not change anything else.

gares · 2021-03-09T08:38:14Z

┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                             │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │   mem faults    │
│                             │                         │                                       │                                       │                         │                 │
│                package_name │     NEW      OLD  PDIFF │            NEW             OLD  PDIFF │            NEW             OLD  PDIFF │     NEW      OLD  PDIFF │ NEW  OLD  PDIFF │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│       coq-engine-bench-lite │  211.57   215.29  -1.73 │   886756884482    902636555975  -1.76 │  1712870047183   1711684099498   0.07 │ 3547804  3547872  -0.00 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│               coq-fourcolor │ 1548.46  1564.98  -1.06 │  6773059912260   6842599864990  -1.02 │ 12238480108242  12231634782345   0.06 │ 2997288  2981420   0.53 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                  coq-stdlib │  391.87   395.55  -0.93 │  1442587419750   1451254224472  -0.60 │  1399080664772   1399177836813  -0.01 │  576192   575984   0.04 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                   coq-verdi │   88.07    88.76  -0.78 │   381529848764    385080032312  -0.92 │   625148984757    630585270809  -0.86 │ 2981948  2990568  -0.29 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│             coq-lambda-rust │  732.77   738.25  -0.74 │  3205667189027   3229731089987  -0.75 │  5050593877973   5080512286320  -0.59 │ 3160276  3202012  -1.30 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                 coq-unimath │ 2412.48  2424.19  -0.48 │ 10552700927421  10599003275529  -0.44 │ 21253801736882  21236083701452   0.08 │ 1127200  1127892  -0.06 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│       coq-mathcomp-solvable │   98.28    98.65  -0.38 │   430344495308    431320585043  -0.23 │   681401156105    680385918331   0.15 │  641576   640652   0.14 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│          coq-mathcomp-field │  129.20   129.44  -0.19 │   566273671793    566830360137  -0.10 │   952408447264    949434038288   0.31 │  659088   675256  -2.39 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                    coq-corn │  880.52   880.27   0.03 │  3845589908703   3841747597247   0.10 │  5929906561255   5929102077698   0.01 │  861948   863540  -0.18 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│             coq-fiat-crypto │ 2937.48  2935.96   0.05 │ 12818466865897  12813467074428   0.04 │ 23538411156807  23517568472091   0.09 │ 2256524  2264544  -0.35 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                   coq-color │  293.32   293.05   0.09 │  1272757149699   1273009136359  -0.02 │  1748337454908   1732453024279   0.92 │ 1106500  1108548  -0.18 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                   coq-flocq │   85.24    85.09   0.18 │   371290235969    371272951958   0.00 │   504990830962    504468374750   0.10 │  833412   833292   0.01 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-rewriter-perf-SuperFast │  484.94   483.78   0.24 │  2115893192738   2108940808854   0.33 │  3538400689980   3543546626467  -0.15 │ 2996976  3003052  -0.20 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│            coq-math-classes │  123.97   123.62   0.28 │   539019884640    537845840659   0.22 │   764794067389    764201563167   0.08 │  506136   509736  -0.71 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│        coq-mathcomp-algebra │   78.99    78.73   0.33 │   345248663593    344163860003   0.32 │   498364029560    493731050920   0.94 │  543992   541220   0.51 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│      coq-mathcomp-ssreflect │   31.22    31.11   0.35 │   135370095069    134933848564   0.32 │   193024843537    192406939994   0.32 │  520148   520852  -0.14 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-rewriter │  414.21   412.48   0.42 │  1805428973219   1799345933175   0.34 │  2941180270428   2925293191029   0.54 │  998176   998300  -0.01 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│      coq-mathcomp-character │   89.17    88.78   0.44 │   390219522461    388714273122   0.39 │   602410752178    599720460270   0.45 │  740256   738696   0.21 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-verdi-raft │  736.03   732.48   0.48 │  3215700806673   3199278727336   0.51 │  4920011007572   4919882278529   0.00 │ 2987292  2998408  -0.37 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│            coq-fiat-parsers │  369.12   366.90   0.61 │  1595851767414   1587557696047   0.52 │  2627324603039   2613633181570   0.52 │ 2915432  2914880   0.02 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│      coq-mathcomp-odd-order │  621.87   617.96   0.63 │  2725646266104   2707513367223   0.67 │  4698569894105   4690850089456   0.16 │  985636   982756   0.29 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                 coq-bignums │   33.18    32.94   0.73 │   143746112650    143086920203   0.46 │   208779405617    208179581056   0.29 │  468060   467964   0.02 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                         coq │    2.66     2.64   0.76 │    11104435014     11135770414  -0.28 │    22712639735     22733446786  -0.09 │  249048   248600   0.18 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│       coq-mathcomp-fingroup │   27.91    27.70   0.76 │   121650684924    120869227319   0.65 │   187602317168    187480900898   0.06 │  484112   483552   0.12 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│  coq-performance-tests-lite │  967.00   959.68   0.76 │  4197989039263   4165762563220   0.77 │  7281532737191   7283484059066  -0.03 │ 2440512  2438556   0.08 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                    coq-core │  111.31   110.22   0.99 │   392963636572    391774487899   0.30 │   465909796200    465877883192   0.01 │  263208   262716   0.19 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                  coq-geocoq │  824.56   814.89   1.19 │  3596899845671   3555643132694   1.16 │  5680206448402   5663680505442   0.29 │ 1001164  1003552  -0.24 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-bedrock2 │  121.42   119.92   1.25 │   529278949212    522354800835   1.33 │   935129965659    920041898744   1.64 │  756428   754464   0.26 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│               coq-fiat-core │   67.82    66.38   2.17 │   276212260399    270282364292   2.19 │   401961636379    386239863477   4.07 │  485288   485288   0.00 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-coqprime │   48.42    46.97   3.09 │   209144842191    202754727717   3.15 │   325283891324    309529019780   5.09 │  762968   762080   0.12 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-coquelicot │   42.14    40.24   4.72 │   181236087324    173619842291   4.39 │   256063966943    240639500477   6.41 │  565164   568492  -0.59 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                 coq-coqutil │   38.11    36.09   5.60 │   164250818007    155649114553   5.53 │   221550464031    206651405224   7.21 │  524224   524356  -0.03 │   0    0    nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

gares · 2021-03-09T08:56:33Z

This is a file where the slowdown is actually visible
https://coq.gitlab.io/-/coq/-/jobs/1080957917/artifacts/_bench/html/coq-coqutil/src/coqutil/Map/TestGoals.v.html
it is not so clear where it comes from to me

pretyping/coercionops.ml

The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been replaced with `cl_typ` and `ClTypMap` respectively.

`coe_source` and `coe_target` fields of type `cl_typ` have been added to `coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a coercion. The `coercion` record has also been replaced with `coe_info_typ`.

pi8027 · 2021-03-09T09:15:38Z

@SkySkimmer @gares Could you run the benchmark again? Thank you in advance.

SkySkimmer · 2021-03-09T10:31:29Z

The slowdown may have been fake due to the new machines.
New run on old machine https://gitlab.com/coq/coq/-/jobs/1082805881

gares · 2021-03-09T12:33:23Z

FYI @pi8027 you should be able to run the bench too by going to the gitlab pipeline and hit the |> button on the bench job.
If you can't we can surely fix this.

pi8027 · 2021-03-09T19:43:57Z

FYI @pi8027 you should be able to run the bench too by going to the gitlab pipeline and hit the |> button on the bench job.
If you can't we can surely fix this.

Thanks. I didn't know that.

gares · 2021-03-10T09:04:19Z

┌─────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                             │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │   mem faults    │
│                             │                         │                                       │                                       │                         │                 │
│                package_name │     NEW      OLD  PDIFF │            NEW             OLD  PDIFF │            NEW             OLD  PDIFF │     NEW      OLD  PDIFF │ NEW  OLD  PDIFF │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                         coq │    4.00     4.07  -1.72 │    10675295194     10687032331  -0.11 │    21578534844     21562825776   0.07 │  259120   269388  -3.81 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│            coq-fiat-parsers │  590.85   595.46  -0.77 │  1649016261333   1659079546799  -0.61 │  2616689234318   2615741094099   0.04 │ 3688932  3691224  -0.06 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                   coq-color │  470.76   474.23  -0.73 │  1306421277479   1315862668032  -0.72 │  1717082041067   1715328779844   0.10 │ 1069252  1072624  -0.31 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-bedrock2 │  194.39   195.75  -0.69 │   536899661247    541172295671  -0.79 │   917117945255    916044366481   0.12 │  779188   777932   0.16 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│       coq-mathcomp-fingroup │   46.47    46.79  -0.68 │   128363883711    129089461183  -0.56 │   185974683546    185861069574   0.06 │  487396   482788   0.95 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                  coq-stdlib │  380.29   382.89  -0.68 │  1054359565142   1061851353979  -0.71 │  1394007858576   1394094128074  -0.01 │  568004   567932   0.01 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-verdi-raft │ 1153.75  1161.55  -0.67 │  3207755998756   3227941061499  -0.63 │  4679756338269   4678946408521   0.02 │  913356   911552   0.20 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                    coq-corn │ 1421.78  1431.27  -0.66 │  3948708528279   3971929648439  -0.58 │  5896244917765   5895389275838   0.01 │  847528   847436   0.01 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│  coq-performance-tests-lite │ 1519.30  1528.46  -0.60 │  4234749740978   4257073005768  -0.52 │  7272979930625   7264433463618   0.12 │ 2433224  1696216  43.45 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│      coq-mathcomp-odd-order │ 1023.43  1029.44  -0.58 │  2849665562330   2863216985408  -0.47 │  4700138375600   4692821735491   0.16 │  977000   980992  -0.41 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                  coq-geocoq │ 1329.64  1336.92  -0.54 │  3699715940158   3717792642949  -0.49 │  5638199464426   5636339774470   0.03 │  996628   996444   0.02 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                   coq-flocq │  140.42   141.17  -0.53 │   388361809083    389932472432  -0.40 │   500416971372    499822929814   0.12 │  828040   832044  -0.48 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│             coq-lambda-rust │ 1150.00  1155.20  -0.45 │  3196041563310   3210602145522  -0.45 │  4768479668466   4766819038715   0.03 │ 1104932  1104604   0.03 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│               coq-perennial │ 4873.25  4894.83  -0.44 │ 13562143354821  13623891463070  -0.45 │ 21200110571768  21202708823833  -0.01 │ 3055772  3059884  -0.13 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│       coq-mathcomp-solvable │  165.19   165.90  -0.43 │   459046957691    460975199796  -0.42 │   678797469718    677740064764   0.16 │  686848   678224   1.27 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│             coq-fiat-crypto │ 4714.19  4727.15  -0.27 │ 13082674363988  13123414743014  -0.31 │ 23766437840015  23773755737817  -0.03 │ 2226780  2237296  -0.47 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│            coq-math-classes │  196.94   197.48  -0.27 │   546513365091    549047663684  -0.46 │   761111340613    760569831537   0.07 │  501944   501744   0.04 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│               coq-fourcolor │ 2441.18  2446.57  -0.22 │  6803570668650   6809490331382  -0.09 │ 12207977552858  12204467099105   0.03 │  735768   735772  -0.00 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│ coq-rewriter-perf-SuperFast │  737.41   739.00  -0.22 │  2052495590263   2055845855700  -0.16 │  3322732498867   3322724890505   0.00 │ 1104332  1104288   0.00 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│               coq-fiat-core │   97.97    98.11  -0.14 │   276541864703    277234901969  -0.25 │   389742969281    387577441552   0.56 │  484352   482624   0.36 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│       coq-engine-bench-lite │  318.53   318.33   0.06 │   895439571592    894253216600   0.13 │  1695340750076   1691250163578   0.24 │ 3124472  3124500  -0.00 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                 coq-bignums │   53.84    53.76   0.15 │   148043315601    148533270106  -0.33 │   206739487817    206191006647   0.27 │  475236   473556   0.35 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-rewriter │  674.69   673.07   0.24 │  1870476846852   1865985586968   0.24 │  2943376745546   2940419535276   0.10 │ 1104552  1104416   0.01 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│      coq-mathcomp-character │  149.42   149.05   0.25 │   415063721179    414030410355   0.25 │   603439904944    600841532643   0.43 │  725004   735024  -1.36 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│          coq-mathcomp-field │  218.48   217.82   0.30 │   607310077673    605950255150   0.22 │   955832077244    952986398874   0.30 │  668964   670960  -0.30 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                 coq-coqutil │   57.88    57.62   0.45 │   159019648931    158586318816   0.27 │   206738556847    205964989272   0.38 │  522656   523848  -0.23 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│      coq-mathcomp-ssreflect │   51.24    50.98   0.51 │   138777778355    139001749395  -0.16 │   185090404461    184474163054   0.33 │  522180   525520  -0.64 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│        coq-mathcomp-algebra │  136.87   136.02   0.62 │   380355976025    377941896847   0.64 │   512587176611    507776908200   0.95 │  555180   555132   0.01 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                 coq-unimath │ 3895.71  3870.77   0.64 │ 10831590615110  10759151057166   0.67 │ 21271699382685  21264226766028   0.04 │ 1134780  1134496   0.03 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                coq-coqprime │   76.41    75.92   0.65 │   207960925865    207883692336   0.04 │   305191606039    303668586609   0.50 │  763496   761600   0.25 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│              coq-coquelicot │   66.90    66.43   0.71 │   180487398452    180131157483   0.20 │   238141575680    236666184155   0.62 │  564212   564280  -0.01 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                    coq-core │  105.48   104.60   0.84 │   293536205009    293209027829   0.11 │   456235860927    456199296591   0.01 │  279112   280456  -0.48 │   0    0    nan │
├─────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│                   coq-verdi │   97.37    96.31   1.10 │   265547278337    265092617024   0.17 │   386803650118    385504486760   0.34 │  552240   551016   0.22 │   0    0    nan │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

gares · 2021-03-10T09:11:50Z

@coqbot merge now

coqbot-app · 2021-03-10T09:11:53Z

@gares: Please take care of the following overlays:

13912-pi8027-remove-bijint.sh

Fix w.r.t coq/coq#13912: Refactor coercionops

pi8027 added kind: cleanup Code removal, deprecation, refactorings, etc. kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: coercions The coercion mechanism. labels Mar 8, 2021

pi8027 requested review from a team as code owners March 8, 2021 09:30

pi8027 added a commit to pi8027/coq-elpi that referenced this pull request Mar 8, 2021

Fix w.r.t coq/coq#13912

221746f

pi8027 mentioned this pull request Mar 8, 2021

Fix w.r.t coq/coq#13912: Refactor coercionops LPCIC/coq-elpi#221

Merged

pi8027 force-pushed the remove-bijint branch from 2d29e39 to cf916e1 Compare March 8, 2021 15:08

gares approved these changes Mar 8, 2021

View reviewed changes

gares self-assigned this Mar 8, 2021

gares added this to the 8.14+rc1 milestone Mar 8, 2021

pi8027 force-pushed the remove-bijint branch from cf916e1 to 42876e0 Compare March 8, 2021 17:03

gares reviewed Mar 9, 2021

View reviewed changes

pretyping/coercionops.ml Outdated Show resolved Hide resolved

pi8027 added 4 commits March 9, 2021 18:10

Replace cl_index with cl_typ in coercionops.ml

4bbbaff

The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been replaced with `cl_typ` and `ClTypMap` respectively.

Add the source and target classes to the coercion table

b3a8960

`coe_source` and `coe_target` fields of type `cl_typ` have been added to `coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a coercion. The `coercion` record has also been replaced with `coe_info_typ`.

Add overlay

874e39f

Add changelog

fcdca40

pi8027 force-pushed the remove-bijint branch from 42876e0 to fcdca40 Compare March 9, 2021 09:12

coqbot-app bot merged commit e16a731 into coq:master Mar 10, 2021

gares added a commit to LPCIC/coq-elpi that referenced this pull request Mar 10, 2021

Merge pull request #221 from pi8027/coq-overlay-13912

cb2d187

Fix w.r.t coq/coq#13912: Refactor coercionops

pi8027 deleted the remove-bijint branch March 18, 2021 18:10

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor coercionops #13912

Refactor coercionops #13912

pi8027 commented Mar 8, 2021 •

edited

gares commented Mar 8, 2021

SkySkimmer commented Mar 8, 2021

pi8027 commented Mar 8, 2021

gares commented Mar 9, 2021

gares commented Mar 9, 2021

pi8027 commented Mar 9, 2021

SkySkimmer commented Mar 9, 2021

gares commented Mar 9, 2021

pi8027 commented Mar 9, 2021

gares commented Mar 10, 2021

gares commented Mar 10, 2021

coqbot-app bot commented Mar 10, 2021

Refactor coercionops #13912

Refactor coercionops #13912

Conversation

pi8027 commented Mar 8, 2021 • edited

gares commented Mar 8, 2021

SkySkimmer commented Mar 8, 2021

pi8027 commented Mar 8, 2021

gares commented Mar 9, 2021

gares commented Mar 9, 2021

pi8027 commented Mar 9, 2021

SkySkimmer commented Mar 9, 2021

gares commented Mar 9, 2021

pi8027 commented Mar 9, 2021

gares commented Mar 10, 2021

gares commented Mar 10, 2021

coqbot-app bot commented Mar 10, 2021

pi8027 commented Mar 8, 2021 •

edited