Experiment: process nursery

[SkySkimmer]

No description provided.

[SkySkimmer]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬────────────────────────────────────────┬──────────────────────────┐
│                                     │      user time [s]      │            CPU instructions            │  max resident mem [KB]   │
│                                     │                         │                                        │                          │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF  │   NEW      OLD    PDIFF  │
├─────────────────────────────────────┼─────────────────────────┼────────────────────────────────────────┼──────────────────────────┤
│                         coq-coqutil │   42.35    46.52  -8.96 │   249174374648    289351409068  -13.89 │  572820   568192    0.81 │
│                            coq-hott │  154.25   159.63  -3.37 │   999418911554   1065684176749   -6.22 │  524720   464916   12.86 │
│                    coq-math-classes │   79.87    82.39  -3.06 │   465438115361    495363810600   -6.04 │  534664   516172    3.58 │
│                        rocq-bignums │   24.63    25.30  -2.65 │   150982509736    159732763656   -5.48 │  469312   460324    1.95 │
│                            coq-core │    2.73     2.78  -1.80 │    19013462380     19016854533   -0.02 │   92864    93880   -1.08 │
│                        coq-coqprime │   54.68    55.50  -1.48 │   367918618491    381731053814   -3.62 │  819936   830704   -1.30 │
│              rocq-mathcomp-solvable │   97.53    98.62  -1.11 │   641838095412    665057388567   -3.49 │ 1114660  1111864    0.25 │
│                        coq-rewriter │  325.33   328.73  -1.03 │  2398714644320   2429465945747   -1.27 │ 1581412  1426292   10.88 │
│               coq-engine-bench-lite │  124.72   126.00  -1.02 │   916993412857    938525068968   -2.29 │ 1008956  1097948   -8.11 │
│                           rocq-elpi │   16.63    16.78  -0.89 │   119079264093    119091626669   -0.01 │  461680   461896   -0.05 │
│                        coq-bedrock2 │  352.96   356.02  -0.86 │  2875581224207   2932901300452   -1.95 │  834952   875636   -4.65 │
│                         rocq-stdlib │  237.95   239.95  -0.83 │  1411935585904   1491817275559   -5.35 │  777312   759868    2.30 │
│                  rocq-mathcomp-boot │   39.41    39.74  -0.83 │   228202476205    233841202809   -2.41 │  655820   667360   -1.73 │
│                        rocq-runtime │   76.08    76.49  -0.54 │   555844655982    554955019578    0.16 │  498456   495904    0.51 │
│  rocq-mathcomp-group-representation │  103.54   103.83  -0.28 │   703650564975    726602875777   -3.16 │ 1685596  1715464   -1.74 │
│                    coq-fiat-parsers │  273.17   273.09   0.03 │  2086298318026   2085257052728    0.05 │ 2276632  2255880    0.92 │
│ coq-neural-net-interp-computed-lite │  236.96   236.64   0.14 │  2262241707178   2262173567312    0.00 │  882404   880900    0.17 │
│                 rocq-mathcomp-field │  212.17   211.84   0.16 │  1531860439371   1558368586062   -1.70 │ 2291036  2315088   -1.04 │
│         coq-rewriter-perf-SuperFast │  462.87   461.89   0.21 │  3534292914288   3533483259567    0.02 │ 1281192  1266380    1.17 │
│        coq-fiat-crypto-with-bedrock │ 7208.14  7188.69   0.27 │ 58696420641099  58866264322815   -0.29 │ 2826996  2827060   -0.00 │
│          rocq-mathcomp-finite-group │   26.68    26.57   0.41 │   169508018905    172552714462   -1.76 │  565280   573860   -1.50 │
│              coq-mathcomp-odd-order │  608.20   605.64   0.42 │  4178113700281   4262398130497   -1.98 │ 2804360  2662744    5.32 │
│                      coq-coquelicot │   38.84    38.67   0.44 │   234132083580    234042013084    0.04 │  834172   835840   -0.20 │
│                       coq-fiat-core │   56.33    56.02   0.55 │   337693270953    336556552868    0.34 │  481868   484732   -0.59 │
│               rocq-mathcomp-algebra │  402.83   400.58   0.56 │  2898777238972   2936378041697   -1.28 │ 1682280  1536332    9.50 │
│          coq-performance-tests-lite │  872.15   864.80   0.85 │  6958308812033   6955004452942    0.05 │ 1511980  1570632   -3.73 │
│                      rocq-equations │    7.99     7.91   1.01 │    55207257824     55126424701    0.15 │  400476   400372    0.03 │
│                 coq-category-theory │ 1126.96  1111.38   1.40 │  8188045444832   8188851285958   -0.01 │ 6004884  6747536  -11.01 │
│                            coq-corn │  654.67   644.98   1.50 │  4331395447703   4313148422890    0.42 │  703924   619624   13.61 │
│                 rocq-mathcomp-order │   82.64    80.96   2.08 │   595192009809    596682173724   -0.25 │ 1559576  1616504   -3.52 │
│                         coq-unimath │ 1995.12  1945.96   2.53 │ 16230131469549  15986154576664    1.53 │ 2142848  1710536   25.27 │
│                       coq-fourcolor │ 1391.60  1351.86   2.94 │ 12868490217414  12423870884905    3.58 │ 1616276  1025788   57.56 │
│                           rocq-core │    6.93     6.69   3.59 │    41580335353     41550382133    0.07 │  447504   449056   -0.35 │
│                           coq-color │  245.45   229.24   7.07 │  1499224305563   1441700926345    3.99 │ 1274148  1169404    8.96 │
│             rocq-mathcomp-ssreflect │    1.30     1.15  13.04 │     8181772548      7548778905    8.39 │  592036   593804   -0.30 │
└─────────────────────────────────────┴─────────────────────────┴────────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
coq-mathcomp-analysis (dependency install failed in NEW)
coq-compcert (dependency install failed in NEW)
rocq-metarocq-utils (dependency install failed in NEW)
coq-iris-examples (dependency install failed in NEW)

rocq-metarocq-common (dependency rocq-metarocq-utils failed)
rocq-metarocq-template (dependency rocq-metarocq-utils failed)
rocq-metarocq-pcuic (dependency rocq-metarocq-utils failed)
rocq-metarocq-safechecker (dependency rocq-metarocq-utils failed)
rocq-metarocq-erasure (dependency rocq-metarocq-utils failed)
rocq-metarocq-translations (dependency rocq-metarocq-utils failed)
coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                       TOP 25 SLOW DOWNS                                                        │
│                                                                                                                                │
│ OLD   NEW    DIFF   %DIFF   Ln                    FILE                                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 88.6  90.0  1.3923   1.57%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│ 14.6  15.7  1.1541   7.92%  833  coq-unimath/UniMath/CategoryTheory/ComprehensionCats/CwfFromCompCatWithUniv.v.html            │
│ 1.36  2.42  1.0663  78.59%  574  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│ 46.8  47.9  1.0653   2.28%  277  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│ 52.3  53.3  0.9575   1.83%  567  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│ 56.7  57.6  0.9339   1.65%  512  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│ 29.8  30.7  0.9287   3.12%   13  coq-fourcolor/theories/proof/job165to189.v.html                                               │
│ 88.8  89.7  0.8921   1.00%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│ 42.6  43.4  0.8663   2.04%  539  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│ 18.3  19.1  0.8462   4.63%   13  coq-fourcolor/theories/proof/job311to314.v.html                                               │
│ 44.9  45.7  0.8430   1.88%  256  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│ 30.9  31.7  0.8279   2.68%   13  coq-fourcolor/theories/proof/job254to270.v.html                                               │
│ 77.0  77.8  0.7969   1.03%   20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                   │
│ 16.5  17.3  0.7766   4.71%   13  coq-fourcolor/theories/proof/job235to238.v.html                                               │
│ 21.4  22.1  0.7486   3.51%  516  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                    │
│ 19.7  20.4  0.7435   3.78%   13  coq-fourcolor/theories/proof/job507to510.v.html                                               │
│ 24.0  24.8  0.7374   3.07%   13  coq-fourcolor/theories/proof/job486to489.v.html                                               │
│ 20.8  21.6  0.7195   3.45%   13  coq-fourcolor/theories/proof/job307to310.v.html                                               │
│  102   103  0.7164   0.70%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                        │
│ 22.3  23.0  0.7113   3.20%   13  coq-fourcolor/theories/proof/job303to306.v.html                                               │
│  201   202  0.6930   0.34%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│ 14.8  15.5  0.6925   4.67%   13  coq-fourcolor/theories/proof/job215to218.v.html                                               │
│ 23.6  24.2  0.6912   2.93%   13  coq-fourcolor/theories/proof/job554to562.v.html                                               │
│ 18.4  19.0  0.6843   3.73%   13  coq-fourcolor/theories/proof/job315to318.v.html                                               │
│ 1.58  2.25  0.6783  43.04%  176  coq-unimath/UniMath/ModelCategories/Examples.v.html                                           │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SPEED UPS                                                          │
│                                                                                                                                    │
│  OLD    NEW    DIFF     %DIFF   Ln                    FILE                                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  41.9   39.9  -2.0047   -4.78%  246  coq-category-theory/Construction/DecoratedCospan/Category.v.html                              │
│   238    237  -1.0920   -0.46%  141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                    │
│  8.19   7.32  -0.8678  -10.60%  571  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│  1.08  0.248  -0.8342  -77.06%  928  coq-unimath/UniMath/CategoryTheory/ComprehensionCats/CwfFromCompCatWithUniv.v.html            │
│  20.2   19.5  -0.7473   -3.69%  543  coq-unimath/UniMath/CategoryTheory/Presheaves/SigmaTypes.v.html                               │
│  4.00   3.31  -0.6905  -17.27%    6  coq-mathcomp-odd-order/theories/BGsection1.v.html                                             │
│  66.4   65.7  -0.6547   -0.99%  608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │
│  4.15   3.51  -0.6382  -15.40%    6  coq-mathcomp-odd-order/theories/BGsection2.v.html                                             │
│   134    133  -0.6255   -0.47%  155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                    │
│  3.60   2.98  -0.6176  -17.15%    6  coq-mathcomp-odd-order/theories/BGappendixAB.v.html                                           │
│  1.49  0.968  -0.5203  -34.95%   68  rocq-mathcomp-group-representation/group_representation/vcharacter.v.html                     │
│  39.4   38.9  -0.4804   -1.22%  236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                    │
│  4.32   3.86  -0.4623  -10.69%    8  coq-mathcomp-odd-order/theories/PFsection2.v.html                                             │
│  1.40  0.944  -0.4597  -32.76%  166  rocq-mathcomp-group-representation/group_representation/classfun.v.html                       │
│  1.62   1.16  -0.4558  -28.13%  115  rocq-mathcomp-group-representation/group_representation/character.v.html                      │
│  4.05   3.60  -0.4465  -11.03%    7  coq-mathcomp-odd-order/theories/BGsection3.v.html                                             │
│  1.57   1.13  -0.4373  -27.86%  120  rocq-mathcomp-group-representation/group_representation/inertia.v.html                        │
│  3.05   2.62  -0.4302  -14.11%   57  rocq-mathcomp-algebra/algebra/archimedean.v.html                                              │
│  1.31  0.894  -0.4195  -31.92%  180  rocq-mathcomp-field/field/finfield.v.html                                                     │
│ 0.919  0.503  -0.4160  -45.26%  173  rocq-mathcomp-field/field/algnum.v.html                                                       │
│ 0.856  0.458  -0.3980  -46.51%  393  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                            │
│  1.83   1.43  -0.3976  -21.78%   57  rocq-mathcomp-algebra/algebra/numeric_hierarchy/numdomain.v.html                              │
│  3.63   3.23  -0.3952  -10.90%    6  coq-mathcomp-odd-order/theories/BGsection4.v.html                                             │
│  29.3   28.9  -0.3912   -1.34%  145  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                  │
│ 0.979  0.590  -0.3887  -39.72%  175  rocq-mathcomp-field/field/galois.v.html                                                       │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[SkySkimmer]

The current interprocess communication is not designed for parallelism, this is probably what causes the errors in dependencies (since we run -j for dependencies in the bench)