Skip to content

Use custom exception for warn-as-error instead of user_err + polymorphic maps #17141

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 2 commits into from
Jan 24, 2023
Merged

Use custom exception for warn-as-error instead of user_err + polymorphic maps #17141

merged 2 commits into from
Jan 24, 2023

Conversation

SkySkimmer
Copy link
Contributor

This may be a little faster if some tactic code is using warn-as-error
for flow control, but mostly it's because we prefer to avoid user_err.

@SkySkimmer SkySkimmer added kind: cleanup Code removal, deprecation, refactorings, etc. request: full CI Use this label when you want your next push to trigger a full CI. labels Jan 19, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner January 19, 2023 12:50
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 19, 2023
@ejgallego ejgallego self-assigned this Jan 19, 2023
@ejgallego ejgallego added this to the 8.18+rc1 milestone Jan 19, 2023
@ejgallego
Copy link
Member

I guess indeed that's better, couple of comments:

  • not sure adding yet another O(n) printing path is a good thing, don't we have an alternative that doesn't require a linear scan/lookup?
  • should maybe the exception be exported (so it can be reified by document managers for example?) Not a big deal.

@SkySkimmer
Copy link
Contributor Author

SkySkimmer commented Jan 19, 2023 •
edited
Loading

not sure adding yet another O(n) printing path is a good thing, don't we have an alternative that doesn't require a linear scan/lookup?

I guess instead of

type v = ..
val printers : (v -> pp option) list ref

we could have something like

type _ tag = ..
type v = V : 'a tag * 'a -> v
val printers : (polymorphic map from 'a tag to 'a) ref

polymorphic map kinda like in #17145

@ejgallego
Copy link
Member

IMVHO that would be nice, also for errors.

I'm still hoping to make progress one day on #12602 , which could use such a map, as I'd like for IDEs to have the choice to have a richer structure to handle error messages (and actions).

@SkySkimmer SkySkimmer requested a review from a team as a code owner January 19, 2023 16:35
@coqbot-app 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 Jan 19, 2023
@SkySkimmer SkySkimmer changed the title Use custom exception for warn-as-error instead of user_err Use custom exception for warn-as-error instead of user_err + polymorphic maps Jan 19, 2023
@SkySkimmer
Copy link
Contributor Author

added some polymorphic map system and used it also for grammar (subsumes #17145)
@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 Jan 19, 2023
@SkySkimmer
Copy link
Contributor Author

@coqbot bench

1 similar comment
@SkySkimmer
Copy link
Contributor Author

@coqbot bench

ejgallego
ejgallego approved these changes Jan 19, 2023
View reviewed changes
Copy link
Member

@ejgallego ejgallego left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM , I guess @ppedrot wants to have a look at this too.

Maybe it would be better not to expose find but just find_opt so we force callers to handle Not_found ?

@SkySkimmer SkySkimmer added the needs: documentation Documentation was not added or updated. label Jan 19, 2023
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jan 20, 2023

🏁 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-fourcolor │ 1468.62  1485.75  -1.15 │  6703047544993   6773554768634  -1.04 │ 12197008523892  12188386624329   0.07 │ 1425328  1423268   0.14 │
│          coq-category-theory │  773.73   781.39  -0.98 │  3533881244663   3567518005726  -0.94 │  5972298318016   5969093159431   0.05 │  913624   913656  -0.00 │
│           coq-mathcomp-field │   93.22    93.98  -0.81 │   425651861837    429435992889  -0.88 │   705822031805    703886988300   0.27 │  897324   895268   0.23 │
│             coq-math-classes │   93.17    93.92  -0.80 │   422127507722    427138598022  -1.17 │   606159589282    603891055662   0.38 │  511476   510972   0.10 │
│          coq-metacoq-erasure │  207.82   209.48  -0.79 │   941168142546    949576721619  -0.89 │  1504196491169   1502498182955   0.11 │ 1503936  1499284   0.31 │
│            coq-iris-examples │  481.26   485.10  -0.79 │  2183713467951   2201179329306  -0.79 │  3346959251517   3342969292310   0.12 │ 1205012  1202640   0.20 │
│            coq-metacoq-pcuic │  564.26   568.20  -0.69 │  2567715357913   2586514621175  -0.73 │  3792208083993   3777616189573   0.39 │ 1890840  1891896  -0.06 │
│                   coq-geocoq │  682.49   687.15  -0.68 │  3106784588316   3126183102911  -0.62 │  5022307120091   5001149725947   0.42 │  995628   995004   0.06 │
│ coq-fiat-crypto-with-bedrock │ 6247.11  6285.31  -0.61 │ 28401124847185  28574579568796  -0.61 │ 52223422039565  52201402413682   0.04 │ 2827104  2827328  -0.01 │
│                    coq-verdi │   47.80    48.06  -0.54 │   216197753267    217169414234  -0.45 │   332429805969    330297458269   0.65 │  532776   529124   0.69 │
│       coq-mathcomp-odd-order │  422.75   424.87  -0.50 │  1932982561187   1942439785842  -0.49 │  3250285560167   3239367651172   0.34 │ 1576012  1573496   0.16 │
│                  coq-coqutil │   36.45    36.63  -0.49 │   163818296384    164301221200  -0.29 │   238461135147    236660449143   0.76 │  557744   557768  -0.00 │
│                 coq-compcert │  289.39   290.74  -0.46 │  1312827527398   1318276532016  -0.41 │  2026178741691   2004133258792   1.10 │ 1114364  1114516  -0.01 │
│                 coq-bedrock2 │  352.37   353.84  -0.42 │  1611144224021   1618943687207  -0.48 │  3163926167352   3161936025876   0.06 │  951304   952500  -0.13 │
│     coq-metacoq-translations │   14.53    14.59  -0.41 │    64907151805     65265929903  -0.55 │   106047773004    104956637814   1.04 │  739040   739036   0.00 │
│                coq-fiat-core │   58.82    59.00  -0.31 │   253727425476    254499751764  -0.30 │   373464226237    369788760778   0.99 │  491176   491756  -0.12 │
│             coq-fiat-parsers │  334.08   335.09  -0.30 │  1500890359945   1509112249999  -0.54 │  2512251697196   2506013122119   0.25 │ 3462024  3461936   0.00 │
│       coq-mathcomp-character │   67.63    67.81  -0.27 │   308692662165    309058591458  -0.12 │   470182216274    467850034481   0.50 │  748376   748356   0.00 │
│       coq-mathcomp-ssreflect │   26.84    26.91  -0.26 │   122416409010    122443877280  -0.02 │   162681279679    157614586574   3.21 │  568724   569392  -0.12 │
│                     coq-hott │  160.17   160.55  -0.24 │   725621047120    728317404850  -0.37 │  1156125651829   1145243159740   0.95 │  572696   570368   0.41 │
│      coq-metacoq-safechecker │  215.22   215.72  -0.23 │   980296846245    982989972134  -0.27 │  1472049812776   1469212221932   0.19 │ 1392940  1393100  -0.01 │
│               coq-verdi-raft │  570.93   572.22  -0.23 │  2604051523274   2611831430175  -0.30 │  4123717214752   4118382962683   0.13 │  958268   956872   0.15 │
│        coq-engine-bench-lite │  162.41   162.74  -0.20 │   697722338372    700303264610  -0.37 │  1308949002675   1309498017061  -0.04 │ 1066084  1067904  -0.17 │
│                    coq-color │  228.34   228.60  -0.11 │  1031400953234   1035538465698  -0.40 │  1515905031944   1498260502603   1.18 │ 1099560  1100220  -0.06 │
│                  coq-unimath │ 1263.38  1264.23  -0.07 │  5761218370028   5764043489252  -0.05 │ 10719703199836  10694198530605   0.24 │ 1661636  1661560   0.00 │
│        coq-mathcomp-fingroup │   22.40    22.41  -0.04 │   102067839636    102115134339  -0.05 │   151082610693    149247287336   1.23 │  500512   499308   0.24 │
│                 coq-rewriter │  357.97   358.10  -0.04 │  1631835110233   1631328666547   0.03 │  2709477110751   2705339707482   0.15 │ 1345996  1345872   0.01 │
│                coq-perennial │ 5465.58  5467.31  -0.03 │ 24916156766804  24932057777573  -0.06 │ 41316161387176  41291741110752   0.06 │ 2564452  2579632  -0.59 │
│        coq-mathcomp-solvable │   81.41    81.41   0.00 │   371359743628    371199823754   0.04 │   572889460802    568808589489   0.72 │  719600   718924   0.09 │
│   coq-performance-tests-lite │  761.58   761.43   0.02 │  3451835446155   3451936840813  -0.00 │  6069642137989   6067335690782   0.04 │ 1665020  1664908   0.01 │
│  coq-rewriter-perf-SuperFast │  727.67   727.35   0.04 │  3310170362779   3311843600964  -0.05 │  5728612694237   5725184920767   0.06 │ 1441244  1442944  -0.12 │
│         coq-metacoq-template │  131.59   131.53   0.05 │   589980541167    591708211879  -0.29 │   969075348118    964263004803   0.50 │ 1184288  1184124   0.01 │
│                     coq-corn │  817.18   816.37   0.10 │  3718096621314   3715837483005   0.06 │  5837448938640   5815799005192   0.37 │  858248   858416  -0.02 │
│                  coq-bignums │   28.86    28.78   0.28 │   131352714343    131481042864  -0.10 │   188414195772    186638909689   0.95 │  479404   482756  -0.69 │
│                   coq-stdlib │  419.42   417.95   0.35 │  1800529242296   1791069955350   0.53 │  1483631506329   1460614858665   1.58 │  630544   634164  -0.57 │
│               coq-coquelicot │   36.70    36.56   0.38 │   164473952120    163890834961   0.36 │   230728138625    224324004110   2.85 │  784452   798348  -1.74 │
│         coq-mathcomp-algebra │   63.77    63.50   0.43 │   290219431724    289749478663   0.16 │   407774171301    401530278200   1.56 │  578716   578816  -0.02 │
│                     coq-core │  110.90   110.20   0.64 │   458028640395    454771587213   0.72 │   477874951648    477190261424   0.14 │  288364   287076   0.45 │
│                 coq-coqprime │   45.74    45.32   0.93 │   206494032100    205063345417   0.70 │   318606511751    312225570323   2.04 │  770912   767636   0.43 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install coq-vst

🐢 Top 25 slow downs 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SLOW DOWNS                                                            │
│                                                                                                                                         │
│   OLD       NEW      DIFF    %DIFF    Ln                    FILE                                                                        │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  40.4410   42.0330  1.5920    3.94%   222  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html               │
│  41.4090   42.7910  1.3820    3.34%   235  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html    │
│  24.3650   25.2960  0.9310    3.82%    19  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                     │
│   8.7110    9.6280  0.9170   10.53%  1504  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                    │
│  24.3660   25.2670  0.9010    3.70%    24  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                     │
│  41.6980   42.5920  0.8940    2.14%   235  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                   │
│  19.0860   19.7970  0.7110    3.73%    27  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                     │
│  45.3310   45.8890  0.5580    1.23%    84  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html                       │
│  30.6580   31.1880  0.5300    1.73%  1603  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                              │
│   8.9420    9.4250  0.4830    5.40%    38  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html │
│ 131.2650  131.7040  0.4390    0.33%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html              │
│  12.7130   13.1380  0.4250    3.34%    14  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                     │
│  62.3660   62.7090  0.3430    0.55%   137  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                 │
│ 151.5620  151.9020  0.3400    0.22%  1188  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                │
│  35.5300   35.8570  0.3270    0.92%   445  coq-unimath/UniMath/SyntheticHomotopyTheory/Circle2.v.html                                   │
│   0.3080    0.6240  0.3160  102.60%  1092  coq-perennial/src/program_proof/examples/dir_proof.v.html                                    │
│  26.2270   26.5290  0.3020    1.15%   522  coq-perennial/src/program_proof/simplepb/pb_becomeprimary_proof.v.html                       │
│  15.5230   15.8210  0.2980    1.92%    30  coq-performance-tests-lite/src/pattern.v.html                                                │
│   0.1170    0.4140  0.2970  253.85%  1088  coq-perennial/src/program_proof/examples/async_mem_alloc_dir_proof.v.html                    │
│ 131.6220  131.9100  0.2880    0.22%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html              │
│   1.5330    1.8200  0.2870   18.72%   987  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                               │
│ 212.2850  212.5340  0.2490    0.12%   139  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                   │
│ 121.7870  122.0150  0.2280    0.19%   153  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                   │
│   2.2960    2.5230  0.2270    9.89%   248  coq-perennial/src/program_proof/memkv/bank_proof.v.html                                      │
│  26.6190   26.8290  0.2100    0.79%   709  coq-perennial/src/program_proof/simplepb/pb_apply_proof.v.html                               │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SPEED UPS                                                               │
│                                                                                                                                              │
│   OLD       NEW      DIFF    %DIFF    Ln                     FILE                                                                            │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 131.1960  128.3080  -2.8880  -2.20%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                            │
│  46.5370   44.2060  -2.3310  -5.01%   557  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│  80.2690   78.7470  -1.5220  -1.90%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                       │
│ 129.4840  128.3800  -1.1040  -0.85%   692  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html     │
│  27.2850   26.5050  -0.7800  -2.86%    10  coq-fourcolor/theories/job503to506.v.html                                                         │
│  62.4460   61.7040  -0.7420  -1.19%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                          │
│  46.7090   46.0660  -0.6430  -1.38%   547  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                  │
│  33.7830   33.1420  -0.6410  -1.90%    10  coq-fourcolor/theories/job001to106.v.html                                                         │
│  27.1340   26.5180  -0.6160  -2.27%    10  coq-fourcolor/theories/job319to322.v.html                                                         │
│   7.1300    6.5310  -0.5990  -8.40%  1719  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                         │
│  22.7700   22.1790  -0.5910  -2.60%    10  coq-fourcolor/theories/job283to286.v.html                                                         │
│  27.9300   27.3620  -0.5680  -2.03%    10  coq-fourcolor/theories/job499to502.v.html                                                         │
│  31.3280   30.7760  -0.5520  -1.76%  1375  coq-fourcolor/theories/cfmap.v.html                                                               │
│  19.3940   18.8780  -0.5160  -2.66%    10  coq-fourcolor/theories/job550to553.v.html                                                         │
│  66.8800   66.3640  -0.5160  -0.77%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                               │
│  28.2170   27.7080  -0.5090  -1.80%    10  coq-fourcolor/theories/job517to530.v.html                                                         │
│  29.9170   29.4100  -0.5070  -1.69%    10  coq-fourcolor/theories/job287to290.v.html                                                         │
│  19.6860   19.1800  -0.5060  -2.57%    10  coq-fourcolor/theories/job623to633.v.html                                                         │
│ 123.8440  123.3540  -0.4900  -0.40%    47  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                           │
│  25.8730   25.3960  -0.4770  -1.84%    10  coq-fourcolor/theories/job554to562.v.html                                                         │
│   7.2090    6.7350  -0.4740  -6.58%   575  coq-perennial/src/program_proof/simple/getattr.v.html                                             │
│  29.2790   28.8170  -0.4620  -1.58%    10  coq-fourcolor/theories/job611to617.v.html                                                         │
│  20.6970   20.2380  -0.4590  -2.22%    10  coq-fourcolor/theories/job311to314.v.html                                                         │
│  27.8650   27.4080  -0.4570  -1.64%    10  coq-fourcolor/theories/job223to226.v.html                                                         │
│  27.5220   27.0650  -0.4570  -1.66%    10  coq-fourcolor/theories/job227to230.v.html                                                         │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@SkySkimmer
Use custom exception for warn-as-error instead of user_err
99a61d6 
This may be a little faster if some tactic code is using warn-as-error
for flow control, but mostly it's because we prefer to avoid user_err.
@coqbot-app 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 Jan 20, 2023
@SkySkimmer
Copy link
Contributor Author

@coqbot bench

@SkySkimmer SkySkimmer mentioned this pull request Jan 20, 2023
Closed
SkySkimmer
SkySkimmer commented Jan 20, 2023
View reviewed changes
SkySkimmer
SkySkimmer commented Jan 20, 2023
View reviewed changes
@ejgallego ejgallego requested a review from ppedrot January 20, 2023 19:41
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jan 21, 2023

🏁 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-mathcomp-character │   67.31    68.11  -1.17 │   307243419240    310585176289  -1.08 │   468447405919    468215216322   0.05 │  750932   748452   0.33 │
│                coq-fiat-core │   58.46    59.11  -1.10 │   252678552018    254917030626  -0.88 │   371216339300    369818656963   0.38 │  491808   490948   0.18 │
│                    coq-verdi │   47.54    47.97  -0.90 │   215526279786    217604134351  -0.95 │   330927932189    330393299769   0.16 │  528852   531204  -0.44 │
│           coq-mathcomp-field │   93.54    94.30  -0.81 │   427031166292    430401486283  -0.78 │   704625989809    704056845684   0.08 │  875004   875104  -0.01 │
│         coq-metacoq-template │  131.67   132.61  -0.71 │   590570894555    594611976603  -0.68 │   965500738130    964222921660   0.13 │ 1184280  1183620   0.06 │
│               coq-coquelicot │   36.38    36.62  -0.66 │   163568797261    164002431857  -0.26 │   226006161261    224305798418   0.76 │  783808   799072  -1.91 │
│            coq-metacoq-pcuic │  567.02   570.45  -0.60 │  2580079966172   2596703580976  -0.64 │  3780626384480   3777679481948   0.08 │ 1889932  1888812   0.06 │
│            coq-iris-examples │  484.08   486.73  -0.54 │  2195691567382   2208828581200  -0.59 │  3345816332089   3343154362007   0.08 │ 1205288  1203276   0.17 │
│        coq-mathcomp-solvable │   81.31    81.75  -0.54 │   370966964460    372559778069  -0.43 │   570511564430    569451607486   0.19 │  719128   720144  -0.14 │
│                 coq-coqprime │   45.26    45.49  -0.51 │   204771027459    205645617385  -0.43 │   313734723294    312207209520   0.49 │  768496   768440   0.01 │
│                 coq-bedrock2 │  351.45   353.07  -0.46 │  1606056515173   1614766830090  -0.54 │  3161490211958   3161743830160  -0.01 │  953216   951308   0.20 │
│                     coq-corn │  814.67   818.35  -0.45 │  3705214539049   3725776567246  -0.55 │  5816316424224   5815267303718   0.02 │  860120   859644   0.06 │
│               coq-verdi-raft │  575.35   577.92  -0.44 │  2625710886565   2636409920645  -0.41 │  4120335119953   4118169042115   0.05 │  957204   955680   0.16 │
│                    coq-color │  228.30   229.27  -0.42 │  1032266997380   1036328554569  -0.39 │  1502580383739   1498142887467   0.30 │ 1099848  1099568   0.03 │
│                 coq-compcert │  289.45   290.67  -0.42 │  1312095772395   1317576539435  -0.42 │  2010265600082   2004508796159   0.29 │ 1114456  1115568  -0.10 │
│        coq-engine-bench-lite │  162.07   162.67  -0.37 │   696719703865    699713590870  -0.43 │  1308386716502   1306015082131   0.18 │ 1207956  1068004  13.10 │
│      coq-metacoq-safechecker │  216.48   217.27  -0.36 │   985955612332    989789953673  -0.39 │  1470649780888   1468832421257   0.12 │ 1393476  1395820  -0.17 │
│                     coq-hott │  160.35   160.93  -0.36 │   726460408817    729304249765  -0.39 │  1148684370586   1144918537334   0.33 │  572824   569956   0.50 │
│                   coq-geocoq │  683.94   686.25  -0.34 │  3116346873737   3124022565121  -0.25 │  5011672076009   5000780444063   0.22 │  995612   998780  -0.32 │
│  coq-rewriter-perf-SuperFast │  729.08   731.42  -0.32 │  3317262391172   3329744550811  -0.37 │  5726701506309   5724087887111   0.05 │ 1440464  1442696  -0.15 │
│                  coq-bignums │   28.80    28.88  -0.28 │   131399254153    130883756700   0.39 │   187309311932    186584026590   0.39 │  479164   480720  -0.32 │
│                  coq-coqutil │   36.80    36.90  -0.27 │   164304998188    165361783663  -0.64 │   237124722650    236560538305   0.24 │  557804   557776   0.01 │
│                coq-fourcolor │ 1472.43  1476.04  -0.24 │  6719561307636   6732799396390  -0.20 │ 12190512320080  12190927686170  -0.00 │ 1300628  1423508  -8.63 │
│                coq-perennial │ 5483.80  5493.98  -0.19 │ 24994658058402  25053965296815  -0.24 │ 41300995259847  41288891611351   0.03 │ 2556348  2579420  -0.89 │
│             coq-math-classes │   94.08    94.22  -0.15 │   425395189836    428180334577  -0.65 │   603744965913    603965919217  -0.04 │  511108   511184  -0.01 │
│     coq-metacoq-translations │   14.52    14.54  -0.14 │    64779240001     65174445067  -0.61 │   105207855330    104957590710   0.24 │  738968   739052  -0.01 │
│   coq-performance-tests-lite │  763.42   764.44  -0.13 │  3461677773439   3466887849259  -0.15 │  6068545719896   6069451531387  -0.01 │ 1664968  1666728  -0.11 │
│                  coq-unimath │ 1267.60  1268.45  -0.07 │  5781294001682   5784243833907  -0.05 │ 10702403560672  10694393652961   0.07 │ 1659980  1659872   0.01 │
│       coq-mathcomp-odd-order │  425.83   426.08  -0.06 │  1946704175010   1948372183710  -0.09 │  3244431161637   3240928734352   0.11 │ 1574192  1574164   0.00 │
│ coq-fiat-crypto-with-bedrock │ 6269.07  6272.62  -0.06 │ 28498687206976  28520397760148  -0.08 │ 52222362606308  52199294947041   0.04 │ 2827020  2828228  -0.04 │
│         coq-mathcomp-algebra │   63.21    63.21   0.00 │   287973627260    288046460163  -0.03 │   402895669230    401140146920   0.44 │  582548   581856   0.12 │
│             coq-fiat-parsers │  334.82   334.78   0.01 │  1505109826250   1505502817854  -0.03 │  2509192618145   2506998448566   0.09 │ 3470916  3461040   0.29 │
│          coq-metacoq-erasure │  207.86   207.73   0.06 │   940965401162    942164102504  -0.13 │  1501221484243   1502400889332  -0.08 │ 1499132  1499740  -0.04 │
│       coq-mathcomp-ssreflect │   27.28    27.26   0.07 │   124426822166    123694542405   0.59 │   160844717014    159794168828   0.66 │  576396   575032   0.24 │
│          coq-category-theory │  780.45   779.14   0.17 │  3564420431208   3557805896724   0.19 │  5970617266183   5969253064307   0.02 │  913252   914000  -0.08 │
│                   coq-stdlib │  424.22   423.41   0.19 │  1818759868810   1813133401494   0.31 │  1466175433380   1460730952976   0.37 │  632984   635044  -0.32 │
│                 coq-rewriter │  359.10   358.27   0.23 │  1636909125574   1632288563324   0.28 │  2706609661992   2704702014115   0.07 │ 1345992  1345948   0.00 │
│        coq-mathcomp-fingroup │   22.31    22.24   0.31 │   101509322803    101507524650   0.00 │   149827242592    149254185232   0.38 │  504120   500012   0.82 │
│                     coq-core │  111.48   110.44   0.94 │   453647469992    453793012823  -0.03 │   477744467778    477479801684   0.06 │  287016   288548  -0.53 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install coq-vst

🐢 Top 25 slow downs 
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SLOW DOWNS                                                               │
│                                                                                                                                               │
│   OLD       NEW      DIFF   %DIFF    Ln                      FILE                                                                             │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  41.0140   42.6120  1.5980   3.90%   235  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                          │
│  41.2100   42.5400  1.3300   3.23%   235  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html           │
│ 131.8910  132.8680  0.9770   0.74%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                     │
│  61.9770   62.9460  0.9690   1.56%   137  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                        │
│   8.7860    9.7270  0.9410  10.71%  1504  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                           │
│  40.8220   41.7380  0.9160   2.24%   222  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                      │
│ 132.2590  133.1000  0.8410   0.64%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                     │
│ 124.1750  124.9630  0.7880   0.63%    47  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                             │
│  66.0110   66.7600  0.7490   1.13%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                 │
│  52.1070   52.7770  0.6700   1.29%    49  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                │
│  24.4160   25.0720  0.6560   2.69%    19  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                            │
│  24.4240   25.0440  0.6200   2.54%    24  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                            │
│ 211.8490  212.3500  0.5010   0.24%   139  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                          │
│  19.1270   19.6190  0.4920   2.57%    27  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                            │
│  34.9660   35.4420  0.4760   1.36%  1532  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                           │
│  31.0040   31.4740  0.4700   1.52%  1375  coq-fourcolor/theories/cfmap.v.html                                                                 │
│   8.9610    9.4310  0.4700   5.24%    38  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html        │
│  30.2840   30.6900  0.4060   1.34%     6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html │
│  20.1860   20.5870  0.4010   1.99%    10  coq-fourcolor/theories/job311to314.v.html                                                           │
│   1.0380    1.4310  0.3930  37.86%   867  coq-unimath/UniMath/CategoryTheory/Monads/RelativeMonads.v.html                                     │
│  26.5320   26.9230  0.3910   1.47%    10  coq-fourcolor/theories/job503to506.v.html                                                           │
│  23.7840   24.1640  0.3800   1.60%   105  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                │
│  11.3270   11.6930  0.3660   3.23%   155  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                │
│  19.1580   19.5200  0.3620   1.89%    10  coq-fourcolor/theories/job623to633.v.html                                                           │
│  23.9150   24.2760  0.3610   1.51%   113  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                     │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 164.9500  162.8120  -2.1380   -1.30%   232  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  44.2260   43.4060  -0.8200   -1.85%   557  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│   7.2090    6.5840  -0.6250   -8.67%  1719  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                               │
│ 129.7980  129.2140  -0.5840   -0.45%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  20.4270   19.8490  -0.5780   -2.83%    10  coq-fourcolor/theories/job271to278.v.html                                                               │
│  37.7420   37.1650  -0.5770   -1.53%   521  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html                                    │
│   7.3320    6.7630  -0.5690   -7.76%   575  coq-perennial/src/program_proof/simple/getattr.v.html                                                   │
│ 128.4230  127.9180  -0.5050   -0.39%   692  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│  20.4620   19.9770  -0.4850   -2.37%    10  coq-fourcolor/theories/job315to318.v.html                                                               │
│  46.2930   45.8450  -0.4480   -0.97%   547  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│  10.2730    9.8600  -0.4130   -4.02%     6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html     │
│  21.6840   21.2810  -0.4030   -1.86%    10  coq-fourcolor/theories/job239to253.v.html                                                               │
│  30.9130   30.5120  -0.4010   -1.30%   128  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                                   │
│  20.7750   20.3750  -0.4000   -1.93%    10  coq-fourcolor/theories/job207to214.v.html                                                               │
│   1.5680    1.1740  -0.3940  -25.13%  1718  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                               │
│  23.5300   23.1530  -0.3770   -1.60%    10  coq-fourcolor/theories/job542to545.v.html                                                               │
│  14.5660   14.1960  -0.3700   -2.54%   193  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│   4.4640    4.0970  -0.3670   -8.22%   324  coq-perennial/src/program_logic/staged_invariant_use_inuse2.v.html                                      │
│  26.5570   26.1900  -0.3670   -1.38%    10  coq-fourcolor/theories/job231to234.v.html                                                               │
│  32.5850   32.2320  -0.3530   -1.08%    10  coq-fourcolor/theories/job323to383.v.html                                                               │
│  15.1310   14.7800  -0.3510   -2.32%   185  coq-perennial/src/goose_lang/interpreter/disk_interpreter.v.html                                        │
│   3.3640    3.0190  -0.3450  -10.26%  1406  coq-perennial/src/program_proof/wal/installer_proof.v.html                                              │
│   3.1510    2.8120  -0.3390  -10.76%   422  coq-fourcolor/theories/contract.v.html                                                                  │
│  27.7530   27.4350  -0.3180   -1.15%    10  coq-fourcolor/theories/job499to502.v.html                                                               │
│  44.0770   43.7600  -0.3170   -0.72%   557  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@SkySkimmer
Copy link
Contributor Author

@coqbot bench

SkySkimmer
SkySkimmer commented Jan 21, 2023
View reviewed changes
clib/polyMap.ml
Comment on lines +62 to +65
let key t = Obj.Extension_constructor.(id (of_val t))
let onekey t = key (tag_of_onetag t)

module M = Int.Map
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Using Int.Map on the extension constructor feels cleaner than HMap using polymorphic compare and hash

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jan 22, 2023

🏁 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-category-theory │  772.64   784.19  -1.47 │  3502794233580   3557211516124  -1.53 │  5969610360611   5968475052045   0.02 │  912516   913784  -0.14 │
│      coq-metacoq-safechecker │  216.38   219.52  -1.43 │   978045455284    992902267641  -1.50 │  1468644119741   1469263891470  -0.04 │ 1396652  1392976   0.26 │
│       coq-mathcomp-ssreflect │   27.15    27.48  -1.20 │   122154632577    123518354003  -1.10 │   160605493923    159906750344   0.44 │  576356   576232   0.02 │
│             coq-math-classes │   94.27    95.33  -1.11 │   421843770707    426678758026  -1.13 │   604266606396    603771113102   0.08 │  511372   511040   0.06 │
│  coq-rewriter-perf-SuperFast │  734.61   741.60  -0.94 │  3278092607297   3307608891799  -0.89 │  5724694242142   5724079182598   0.01 │ 1442188  1443168  -0.07 │
│     coq-metacoq-translations │   14.72    14.85  -0.88 │    64727690205     65037753073  -0.48 │   105205972983    104945872483   0.25 │  739200   739076   0.02 │
│                coq-perennial │ 5451.56  5493.40  -0.76 │ 24624427422333  24809622975006  -0.75 │ 41289796434219  41288066030607   0.00 │ 2564700  2579148  -0.56 │
│   coq-performance-tests-lite │  765.07   770.83  -0.75 │  3410183483968   3437654989359  -0.80 │  6066404161822   6068615106517  -0.04 │ 1664944  1665012  -0.00 │
│                   coq-stdlib │  423.93   427.06  -0.73 │  1791103179513   1800785680780  -0.54 │  1465519043025   1460618630602   0.34 │  635232   630748   0.71 │
│       coq-mathcomp-odd-order │  423.87   426.97  -0.73 │  1926627636550   1940620167599  -0.72 │  3241492901147   3241225360139   0.01 │ 1574096  1574172  -0.00 │
│ coq-fiat-crypto-with-bedrock │ 6274.67  6320.25  -0.72 │ 28199017410639  28402362387273  -0.72 │ 52196066292555  52188621672833   0.01 │ 2827420  2828364  -0.03 │
│                     coq-corn │  821.98   827.56  -0.67 │  3700073658232   3726085077109  -0.70 │  5821058617982   5814330475859   0.12 │  858332   859592  -0.15 │
│                   coq-geocoq │  687.80   692.29  -0.65 │  3101573373282   3117584185029  -0.51 │  5008524697135   5001328632396   0.14 │  997308   995832   0.15 │
│               coq-verdi-raft │  571.43   575.07  -0.63 │  2589275114207   2607275012588  -0.69 │  4119138979382   4118169393009   0.02 │  955028   955156  -0.01 │
│                    coq-color │  230.28   231.58  -0.56 │  1024901750689   1032751590864  -0.76 │  1502008450586   1498488695670   0.23 │ 1100420  1100292   0.01 │
│                  coq-bignums │   28.98    29.14  -0.55 │   130243789889    131399445853  -0.88 │   187014669281    186760858990   0.14 │  479968   480796  -0.17 │
│                  coq-coqutil │   37.12    37.32  -0.54 │   164206988489    164423826298  -0.13 │   236929646465    236676946468   0.11 │  559620   557992   0.29 │
│                 coq-rewriter │  360.14   362.07  -0.53 │  1623134354614   1631911036160  -0.54 │  2705264595978   2704915424126   0.01 │ 1349804  1345968   0.28 │
│       coq-mathcomp-character │   67.41    67.77  -0.53 │   305834885679    307458543538  -0.53 │   468463950294    468330347911   0.03 │  751020   748932   0.28 │
│                     coq-hott │  161.70   162.50  -0.49 │   723670316112    726922561521  -0.45 │  1147627976894   1145445425163   0.19 │  572656   570388   0.40 │
│                 coq-bedrock2 │  357.54   359.22  -0.47 │  1593580481278   1597751141519  -0.26 │  3161930199080   3161409873784   0.02 │  951152   951408  -0.03 │
│            coq-iris-examples │  484.84   486.84  -0.41 │  2178618750594   2188683084683  -0.46 │  3343710344177   3342354351809   0.04 │ 1209012  1202068   0.58 │
│               coq-coquelicot │   36.86    37.00  -0.38 │   162565251202    162933184655  -0.23 │   225685383361    224364209964   0.59 │  783504   798576  -1.89 │
│                 coq-compcert │  291.14   292.24  -0.38 │  1302225224607   1307157433427  -0.38 │  2009378219376   2004522449520   0.24 │ 1115152  1115140   0.00 │
│         coq-metacoq-template │  133.03   133.53  -0.37 │   590646283928    591746885929  -0.19 │   965307814313    964295342020   0.10 │ 1184056  1185508  -0.12 │
│            coq-metacoq-pcuic │  571.05   573.13  -0.36 │  2572310562227   2581643182507  -0.36 │  3780141946584   3777389741555   0.07 │ 1891084  1892288  -0.06 │
│         coq-mathcomp-algebra │   63.64    63.83  -0.30 │   287339663772    288232458979  -0.31 │   402478281033    401342318222   0.28 │  582016   581924   0.02 │
│           coq-mathcomp-field │   93.71    93.98  -0.29 │   425063587566    426668856047  -0.38 │   704041776047    704094446123  -0.01 │  875024   876916  -0.22 │
│                     coq-core │  112.02   112.34  -0.28 │   448144916946    445592920544   0.57 │   477398880917    477400860306  -0.00 │  289236   286900   0.81 │
│        coq-mathcomp-solvable │   81.71    81.94  -0.28 │   368339700127    369998960509  -0.45 │   569971469661    569529669838   0.08 │  719460   719368   0.01 │
│             coq-fiat-parsers │  340.67   341.45  -0.23 │  1500242489560   1504358736789  -0.27 │  2507919863269   2505869089952   0.08 │ 3463168  3461284   0.05 │
│                  coq-unimath │ 1272.84  1275.67  -0.22 │  5745096101025   5743865314329   0.02 │ 10700649487855  10693750258461   0.06 │ 1661756  1664296  -0.15 │
│                 coq-coqprime │   45.68    45.77  -0.20 │   203620422443    204240966588  -0.30 │   313356573588    312201883481   0.37 │  770692   767800   0.38 │
│                    coq-verdi │   48.16    48.25  -0.19 │   215613844971    216143645191  -0.25 │   330726775064    330183118629   0.16 │  532968   529088   0.73 │
│                coq-fourcolor │ 1506.82  1509.16  -0.16 │  6649106433030   6660654046399  -0.17 │ 12192350953413  12190739659626   0.01 │ 1423376  1423280   0.01 │
│          coq-metacoq-erasure │  209.08   209.32  -0.11 │   937117379063    938875264066  -0.19 │  1501021877679   1502362943062  -0.09 │ 1498788  1498284   0.03 │
│        coq-mathcomp-fingroup │   22.46    22.48  -0.09 │   101044017164    101451483124  -0.40 │   149637075789    149265836723   0.25 │  501404   499580   0.37 │
│        coq-engine-bench-lite │  163.54   163.30   0.15 │   696089298734    695596384975   0.07 │  1312396972113   1307104640284   0.40 │ 1068128  1067904   0.02 │
│                coq-fiat-core │   60.08    59.49   0.99 │   253985718585    253443685330   0.21 │   370927475745    369810183912   0.30 │  489308   491256  -0.40 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install coq-vst

🐢 Top 25 slow downs 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                               │
│                                                                                                                                              │
│   OLD       NEW      DIFF    %DIFF    Ln                     FILE                                                                            │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 131.7860  132.8250  1.0390    0.79%   692  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html     │
│   8.8140    9.7830  0.9690   10.99%  1504  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                         │
│   8.9080    9.5940  0.6860    7.70%    38  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html      │
│  44.9830   45.6350  0.6520    1.45%   557  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                   │
│  45.1270   45.7630  0.6360    1.41%   557  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│ 211.8150  212.4210  0.6060    0.29%   139  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                        │
│  23.5910   24.1770  0.5860    2.48%  2292  coq-perennial/src/goose_lang/logical_reln_fund.v.html                                             │
│  21.8070   22.2230  0.4160    1.91%    10  coq-fourcolor/theories/job507to510.v.html                                                         │
│  37.1330   37.5160  0.3830    1.03%    10  coq-fourcolor/theories/job439to465.v.html                                                         │
│ 121.5090  121.8840  0.3750    0.31%   153  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                        │
│  25.0310   25.3640  0.3330    1.33%   215  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                          │
│   3.8390    4.1680  0.3290    8.57%   691  coq-perennial/src/program_proof/wal/circ_proof_crash.v.html                                       │
│   0.3010    0.6210  0.3200  106.31%  1092  coq-perennial/src/program_proof/examples/dir_proof.v.html                                         │
│   1.4860    1.7990  0.3130   21.06%   987  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                                    │
│   0.1160    0.4230  0.3070  264.66%  1088  coq-perennial/src/program_proof/examples/async_mem_alloc_dir_proof.v.html                         │
│  66.5170   66.8050  0.2880    0.43%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                               │
│  19.3940   19.6770  0.2830    1.46%    10  coq-fourcolor/theories/job550to553.v.html                                                         │
│   6.0190    6.2720  0.2530    4.20%     4  coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.v.html    │
│ 152.9650  153.2090  0.2440    0.16%  1188  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                     │
│   1.2840    1.5140  0.2300   17.91%    19  coq-metacoq-template/template-coq/theories/utils/ByteCompareSpec.v.html                           │
│  30.1830   30.4090  0.2260    0.75%    10  coq-fourcolor/theories/job287to290.v.html                                                         │
│  27.5720   27.7960  0.2240    0.81%  1640  coq-geocoq/Tarski_dev/Ch16_coordinates_with_functions.v.html                                      │
│   0.0840    0.3040  0.2200  261.90%    94  coq-metacoq-erasure/erasure/theories/ETransform.v.html                                            │
│   0.0220    0.2350  0.2130  968.18%   170  coq-metacoq-erasure/erasure/theories/ETransform.v.html                                            │
│  64.2270   64.4270  0.2000    0.31%   137  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                      │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                     │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 164.6130  163.4200  -1.1930   -0.72%   232  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│ 133.2950  132.1550  -1.1400   -0.86%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│ 133.5510  132.4540  -1.0970   -0.82%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  80.5160   79.5630  -0.9530   -1.18%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│ 130.9430  130.0840  -0.8590   -0.66%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│ 126.3760  125.5240  -0.8520   -0.67%    47  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│   7.1660    6.5580  -0.6080   -8.48%  1719  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                               │
│  30.8940   30.3030  -0.5910   -1.91%  1375  coq-fourcolor/theories/cfmap.v.html                                                                     │
│  40.2640   39.7010  -0.5630   -1.40%   833  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                  │
│  62.3150   61.7730  -0.5420   -0.87%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  10.6890   10.1530  -0.5360   -5.01%   823  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│   7.3210    6.8050  -0.5160   -7.05%   575  coq-perennial/src/program_proof/simple/getattr.v.html                                                   │
│  26.8710   26.3670  -0.5040   -1.88%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                                   │
│  14.6370   14.1630  -0.4740   -3.24%   193  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│  52.6920   52.2390  -0.4530   -0.86%    49  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│   8.7690    8.3230  -0.4460   -5.09%   824  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│  25.4050   24.9790  -0.4260   -1.68%   218  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                        │
│  28.2010   27.7770  -0.4240   -1.50%    10  coq-fourcolor/theories/job279to282.v.html                                                               │
│   8.1210    7.7080  -0.4130   -5.09%   825  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│   1.5740    1.1610  -0.4130  -26.24%  1718  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                               │
│  20.1000   19.7080  -0.3920   -1.95%    10  coq-fourcolor/theories/job623to633.v.html                                                               │
│   7.4160    7.0360  -0.3800   -5.12%   826  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│   9.1950    8.8160  -0.3790   -4.12%   910  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│  24.0320   23.6680  -0.3640   -1.51%   233  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                        │
│  10.3890   10.0350  -0.3540   -3.41%     6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html     │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@ejgallego
Copy link
Member

@ppedrot want to have a look at this?

@SkySkimmer SkySkimmer removed the needs: documentation Documentation was not added or updated. label Jan 24, 2023
@SkySkimmer
Copy link
Contributor Author

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 Jan 24, 2023
@ejgallego
Copy link
Member

fiat-crypto needs to be cut down.
@coqbot: merge now

@coqbot-app coqbot-app bot merged commit a290b31 into rocq-prover:master Jan 24, 2023
@SkySkimmer SkySkimmer deleted the wanr-error-exn branch January 25, 2023 08:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ppedrot ppedrot ppedrot approved these changes

@ejgallego ejgallego ejgallego approved these changes

Assignees

@ejgallego ejgallego

Labels
kind: cleanup Code removal, deprecation, refactorings, etc.
Projects
None yet
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.
3 participants
@SkySkimmer @ejgallego @ppedrot