SkySkimmer
commented
2 weeks ago @coqbot bench
Open SkySkimmer opened 2 weeks ago
SkySkimmer
commented
2 weeks ago @coqbot bench
ppedrot
commented
2 weeks ago Some of the tactics send potentially ill-typed evars. It should be indeed the responsibility of the tactic itself to check that it doesn't generate crap, but 1. this is putting the burden on the caller and 2. maybe there are also user-facing calls to refine that mess with typing invariants. The latter should definitely be wrapped in a sanitizer somehow.
coqbot-app[bot]
commented
2 weeks ago :checkered_flag: 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-equations │ 7.50 7.74 -3.10 │ 31038359599 31020839747 0.06 │ 50925667832 50946517927 -0.04 │ 388912 386984 0.50 │
│ coq-bedrock2 │ 362.68 365.81 -0.86 │ 1642218252790 1651822005276 -0.58 │ 3110558136641 3110527786253 0.00 │ 860080 859328 0.09 │
│ coq-metacoq-safechecker │ 417.78 421.21 -0.81 │ 1904992145199 1920251925347 -0.79 │ 3152787564606 3184333482170 -0.99 │ 2089756 2073112 0.80 │
│ coq-mathcomp-odd-order │ 790.73 796.08 -0.67 │ 3610720185722 3633859802749 -0.64 │ 6075512568177 6078636952576 -0.05 │ 1640604 1652820 -0.74 │
│ coq-metacoq-erasure │ 503.72 507.05 -0.66 │ 2282761320418 2295689981182 -0.56 │ 3562992645864 3581895205120 -0.53 │ 2067528 2101412 -1.61 │
│ coq-mathcomp-character │ 109.31 109.97 -0.60 │ 497066790833 500253041041 -0.64 │ 789790217809 790493156177 -0.09 │ 1133396 1139444 -0.53 │
│ coq-metacoq-pcuic │ 985.94 991.37 -0.55 │ 4400186620147 4423491679991 -0.53 │ 6451672010391 6470643630342 -0.29 │ 2680832 2678144 0.10 │
│ coq-metacoq-template │ 151.03 151.84 -0.53 │ 664692928417 666261758717 -0.24 │ 1046471766427 1046892921983 -0.04 │ 1519836 1516496 0.22 │
│ coq-engine-bench-lite │ 157.93 158.71 -0.49 │ 662655502925 666748063057 -0.61 │ 1222763219746 1223648603483 -0.07 │ 1321316 1321488 -0.01 │
│ coq-coquelicot │ 39.64 39.83 -0.48 │ 175286905527 176041512662 -0.43 │ 248419333236 249035021506 -0.25 │ 853276 853056 0.03 │
│ coq-category-theory │ 690.68 693.51 -0.41 │ 3127958856358 3142073407206 -0.45 │ 5201027828414 5263794586985 -1.19 │ 977128 955384 2.28 │
│ coq-mathcomp-fingroup │ 30.43 30.55 -0.39 │ 137812998890 139057305634 -0.89 │ 207462652759 207787777323 -0.16 │ 565992 569568 -0.63 │
│ coq-mathcomp-solvable │ 118.35 118.78 -0.36 │ 538690043549 540556299443 -0.35 │ 856076287470 857082442228 -0.12 │ 879836 877316 0.29 │
│ coq-fiat-core │ 59.52 59.72 -0.33 │ 245855569797 245305965846 0.22 │ 368606700800 368699281207 -0.03 │ 484236 485068 -0.17 │
│ coq-coqprime │ 48.08 48.20 -0.25 │ 215024486000 215196954726 -0.08 │ 334484645450 334484770530 -0.00 │ 787220 784292 0.37 │
│ coq-math-classes │ 85.57 85.78 -0.24 │ 382891430883 383562195026 -0.17 │ 536167704212 537005223196 -0.16 │ 504408 504920 -0.10 │
│ coq-performance-tests-lite │ 710.01 711.45 -0.20 │ 3178372519747 3183356151044 -0.16 │ 5680128080411 5684884028529 -0.08 │ 2275500 2275896 -0.02 │
│ coq-hott │ 161.58 161.85 -0.17 │ 717379027922 716591925030 0.11 │ 1147003464508 1146949840882 0.00 │ 474628 472400 0.47 │
│ coq-iris-examples │ 466.94 467.43 -0.10 │ 2114374698437 2114908475704 -0.03 │ 3275273754173 3276836145102 -0.05 │ 1122364 1116884 0.49 │
│ coq-fiat-crypto-with-bedrock │ 6250.28 6255.36 -0.08 │ 28326822600894 28341592477191 -0.05 │ 51218445422102 51215934672453 0.00 │ 3246096 3246044 0.00 │
│ coq-rewriter-perf-SuperFast │ 797.07 797.69 -0.08 │ 3565134692974 3567068398277 -0.05 │ 6255560009976 6256738323901 -0.02 │ 1576540 1574488 0.13 │
│ coq-verdi │ 49.24 49.27 -0.06 │ 220379585629 220731174507 -0.16 │ 340365392320 340892852664 -0.15 │ 532260 530892 0.26 │
│ coq-unimath │ 2468.77 2469.44 -0.03 │ 11197520789165 11195126052120 0.02 │ 22212848456002 22211465412118 0.01 │ 1255076 1254904 0.01 │
│ coq-compcert │ 282.46 282.43 0.01 │ 1268765030610 1267490711973 0.10 │ 1945536064286 1945764069818 -0.01 │ 1123380 1124164 -0.07 │
│ coq-mathcomp-field │ 143.82 143.67 0.10 │ 649245054147 649030258100 0.03 │ 1072521466936 1074363625721 -0.17 │ 1457960 1483828 -1.74 │
│ coq-neural-net-interp-computed-lite │ 300.50 300.06 0.15 │ 1370347675340 1368778368744 0.11 │ 3617686080117 3617778193722 -0.00 │ 1112920 1116716 -0.34 │
│ coq-color │ 251.96 251.59 0.15 │ 1125291953444 1123493166743 0.16 │ 1634485294181 1635985568705 -0.09 │ 1217920 1175712 3.59 │
│ coq-core │ 130.74 130.46 0.21 │ 501583765741 497754744059 0.77 │ 532200587481 531929527704 0.05 │ 457140 462372 -1.13 │
│ coq-corn │ 716.16 714.43 0.24 │ 3238703349007 3232400169283 0.19 │ 5064964803798 5077814357710 -0.25 │ 755132 755436 -0.04 │
│ coq-fourcolor │ 1371.28 1367.93 0.24 │ 6238294254805 6221418499314 0.27 │ 12907112446530 12909644095198 -0.02 │ 2188016 2137604 2.36 │
│ coq-mathcomp-algebra │ 262.04 261.24 0.31 │ 1184032042999 1181079817207 0.25 │ 1999997958597 2000634837254 -0.03 │ 1349648 1335580 1.05 │
│ coq-coqutil │ 42.45 42.31 0.33 │ 186045327993 185225589453 0.44 │ 270894267861 270878752164 0.01 │ 560952 560884 0.01 │
│ coq-vst │ 881.57 878.39 0.36 │ 3984855877684 3971572220151 0.33 │ 6741265504691 6743892819349 -0.04 │ 2167572 2167956 -0.02 │
│ coq-test-suite │ 710.01 707.33 0.38 │ 3014955302020 2998179722823 0.56 │ 5377183072259 5377039167942 0.00 │ 2695064 2694692 0.01 │
│ coq-fiat-parsers │ 313.92 312.62 0.42 │ 1389374023320 1384509544196 0.35 │ 2472543965444 2471316429140 0.05 │ 2410460 2406872 0.15 │
│ coq-metacoq-translations │ 17.11 17.01 0.59 │ 75092433573 75129308249 -0.05 │ 125115811109 125097399981 0.01 │ 843568 846340 -0.33 │
│ coq-rewriter │ 393.13 390.39 0.70 │ 1772748050578 1762434102460 0.59 │ 2990734293179 2990660599104 0.00 │ 1478028 1477036 0.07 │
│ coq-verdi-raft │ 584.31 580.03 0.74 │ 2651032779412 2632818343811 0.69 │ 4161364034507 4161577790161 -0.01 │ 847636 847800 -0.02 │
│ coq-bignums │ 29.69 29.45 0.81 │ 133125334884 133115163183 0.01 │ 192278384838 192277099373 0.00 │ 477572 478092 -0.11 │
│ coq-mathcomp-ssreflect │ 224.07 221.52 1.15 │ 1010260713729 999737376025 1.05 │ 1676413775099 1675999605010 0.02 │ 1720820 1718752 0.12 │
│ coq-stdlib │ 352.96 348.88 1.17 │ 1480157963639 1467549461932 0.86 │ 1257442431814 1258446238642 -0.08 │ 721552 719776 0.25 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 3.9050 4.9690 1.0640 27.25% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 10.9520 11.7590 0.8070 7.37% 2103 coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html │ │ 2.6530 3.3320 0.6790 25.59% 34 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 1.6310 2.1990 0.5680 34.83% 196 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 44.2400 44.7430 0.5030 1.14% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 2.4640 2.9030 0.4390 17.82% 1001 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 27.4760 27.8590 0.3830 1.39% 147 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 29.3000 29.6220 0.3220 1.10% 12 coq-fourcolor/theories/job001to106.v.html │ │ 28.5220 28.8320 0.3100 1.09% 12 coq-fourcolor/theories/job323to383.v.html │ │ 24.1020 24.4110 0.3090 1.28% 12 coq-fourcolor/theories/job503to506.v.html │ │ 10.1850 10.4920 0.3070 3.01% 496 coq-rewriter/src/Rewriter/Rewriter/Wf.v.html │ │ 17.1400 17.4460 0.3060 1.79% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 29.2980 29.5910 0.2930 1.00% 12 coq-fourcolor/theories/job165to189.v.html │ │ 7.0890 7.3810 0.2920 4.12% 2089 coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html │ │ 37.7920 38.0810 0.2890 0.76% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html │ │ 24.4920 24.7800 0.2880 1.18% 12 coq-fourcolor/theories/job291to294.v.html │ │ 29.2280 29.5120 0.2840 0.97% 144 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 20.9160 21.1930 0.2770 1.32% 213 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 6.6750 6.9470 0.2720 4.07% 1075 coq-rewriter/src/Rewriter/Language/Inversion.v.html │ │ 1.6460 1.9180 0.2720 16.52% 165 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 0.5520 0.8200 0.2680 48.55% 816 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.5520 0.8070 0.2550 46.20% 422 coq-stdlib/MSets/MSetList.v.html │ │ 20.4300 20.6830 0.2530 1.24% 2736 coq-metacoq-safechecker/safechecker/theories/PCUICTypeChecker.v.html │ │ 39.7710 40.0240 0.2530 0.64% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 0.6320 0.8840 0.2520 39.87% 736 coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 259.4420 255.3860 -4.0560 -1.56% 1629 coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html │ │ 220.8970 217.8840 -3.0130 -1.36% 103 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 64.8390 62.3840 -2.4550 -3.79% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 64.6730 62.7400 -1.9330 -2.99% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 49.6360 47.9160 -1.7200 -3.47% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 96.1020 94.9250 -1.1770 -1.22% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 83.8810 82.8220 -1.0590 -1.26% 365 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 69.6670 68.6750 -0.9920 -1.42% 368 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 96.0570 95.0700 -0.9870 -1.03% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 154.9220 154.0180 -0.9040 -0.58% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 102.1480 101.2510 -0.8970 -0.88% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 49.0280 48.1950 -0.8330 -1.70% 558 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 6.0570 5.3020 -0.7550 -12.46% 823 coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html │ │ 20.5540 19.9970 -0.5570 -2.71% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 8.1020 7.6030 -0.4990 -6.16% 881 coq-vst/veric/binop_lemmas4.v.html │ │ 13.9520 13.5090 -0.4430 -3.18% 850 coq-unimath/UniMath/CategoryTheory/Profunctors/Transformation.v.html │ │ 20.6240 20.1890 -0.4350 -2.11% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 3.6330 3.2120 -0.4210 -11.59% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 36.8700 36.4790 -0.3910 -1.06% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 1.3400 0.9800 -0.3600 -26.87% 854 coq-stdlib/FSets/FMapAVL.v.html │ │ 82.2940 81.9420 -0.3520 -0.43% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 4.1430 3.7930 -0.3500 -8.45% 275 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 27.5140 27.1720 -0.3420 -1.24% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 23.5820 23.2610 -0.3210 -1.36% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 24.4920 24.1770 -0.3150 -1.29% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
I can't see a reason to have it.