Skip to content
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

Produce profiles in google trace format #17702

Merged
merged 11 commits into from Sep 16, 2023
Merged

Produce profiles in google trace format #17702

merged 11 commits into from Sep 16, 2023

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Jun 7, 2023 •
edited

(trace format doc: https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/edit)

display using https://profiler.firefox.com/
or https://ui.perfetto.dev/
(or in chrome's builtin display but I didn't test it)

Example visualization (in perfetto):

  • peano_naturals from HoTT (1MB gzipped)
    peano_nats

  • hurkens from stdlib (3MB uncompressed, 170KB gzipped)
    hurkens

  • example from uconstr: for Ltac2? #13977 (120MB uncompressed, 4MB gzipped)
    bad

@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 Jun 7, 2023
@SkySkimmer
Copy link
Contributor Author

@coqbot bench

@SkySkimmer
Copy link
Contributor Author

Bench failed to upload artifacts (too large)
I sshd into the machine, opam.NEW is 32GB, opam.OLD 21GB
Full list of trace files sorted by size https://gist.github.com/SkySkimmer/32721edc5ad8c70ed3fa49961e5f38b9

There are some approaches we could use to limit artifact size

  • remove the files bigger than some size limit
  • remove entries which takes less than some time limit (in the current streaming model this is inconvenient as we don't know how long it will take when we're printing the start event, and BTW "complete events" don't display as nicely IMO, but we could probably deal with it by delaying the printing) (they would still appear in the summary of subcalls for the surrounding events, and BTW we should add the number of calls next to the current sum of time spent)

Probably the second is more reasonable.

@SkySkimmer
Copy link
Contributor Author

(that last fiat_crypto_via_setoid_rewrite_standalone is 19GB uncompressed BTW)

@Alizter
Copy link
Contributor

Alizter commented Jun 8, 2023

Is .gz the best compression we can do?

@ejgallego
Copy link
Member

As written in Zulip also note:

@SkySkimmer
Copy link
Contributor Author

I put some numbers in the "coq_makefile ..." commit
TLDR xz is somewhat better but not enough to compensate for being unable to give the compressed file directly to the visualizer IMO
Instead of 11GB we might have 8GB ish

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 8, 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-stdlib │  410.93  414.82   -0.94 │ 1763852538060  1779497716248   -0.88 │  1450962382080  1448973846854    0.14 │  659112   649516   1.48 │
│                   coq-core │  113.21  112.33    0.78 │  475116936872   474201702481    0.19 │   479015935445   478476718627    0.11 │  291188   291428  -0.08 │
│ coq-performance-tests-lite │ 1538.93  751.75  104.71 │ 7024474957991  3408417412912  106.09 │ 13067722654339  6033755252446  116.58 │ 1668044  1667728   0.02 │
└────────────────────────────┴─────────────────────────┴──────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘
🐢 Top 25 slow downs 
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                       TOP 25 SLOW DOWNS                                                       │
│                                                                                                                               │
│   OLD       NEW       DIFF     %DIFF     Ln                  FILE                                                             │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 128.4610  397.8810  269.4200   209.73%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 128.2650  397.5770  269.3120   209.97%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│  16.6800   70.3260   53.6460   321.62%    32  coq-performance-tests-lite/src/pattern.v.html                                   │
│   7.2500   34.3630   27.1130   373.97%    31  coq-performance-tests-lite/src/pattern.v.html                                   │
│   3.2990   16.9060   13.6070   412.46%    30  coq-performance-tests-lite/src/pattern.v.html                                   │
│   3.6040   12.2950    8.6910   241.15%   652  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   3.8660   12.4840    8.6180   222.92%   623  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   1.5300    8.3470    6.8170   445.56%    29  coq-performance-tests-lite/src/pattern.v.html                                   │
│   0.7530    4.1390    3.3860   449.67%    28  coq-performance-tests-lite/src/pattern.v.html                                   │
│  40.2010   42.2840    2.0830     5.18%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html  │
│   3.1320    4.0530    0.9210    29.41%    32  coq-performance-tests-lite/src/n_polymorphic_universes.v.html                   │
│   0.1270    0.5630    0.4360   343.31%   133  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   0.1260    0.5170    0.3910   310.32%   190  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   2.4680    2.7840    0.3160    12.80%  1001  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   0.0570    0.3010    0.2440   428.07%   162  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   1.3240    1.5670    0.2430    18.35%   566  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                    │
│   1.2680    1.4820    0.2140    16.88%   853  coq-stdlib/FSets/FMapAVL.v.html                                                 │
│   2.1660    2.3390    0.1730     7.99%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                          │
│   0.0630    0.2360    0.1730   274.60%   219  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   0.0050    0.1610    0.1560  3120.00%   730  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                          │
│   0.1890    0.3330    0.1440    76.19%   905  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                          │
│   0.0030    0.1470    0.1440  4800.00%   878  coq-stdlib/Reals/Abstract/ConstructiveRealsMorphisms.v.html                     │
│   0.3850    0.5240    0.1390    36.10%   301  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html                             │
│   0.2680    0.4030    0.1350    50.37%   198  coq-stdlib/setoid_ring/Ncring_initial.v.html                                    │
│   0.0000    0.1330    0.1330      inf%  1901  coq-stdlib/FSets/FMapFacts.v.html                                               │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                           TOP 25 SPEED UPS                                           │
│                                                                                                      │
│  OLD     NEW     DIFF     %DIFF     Ln              FILE                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 3.5990  2.7840  -0.8150   -22.65%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                  │
│ 3.1640  2.5100  -0.6540   -20.67%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html  │
│ 1.9620  1.4700  -0.4920   -25.08%   209  coq-stdlib/setoid_ring/Ncring_tac.v.html                    │
│ 1.1030  0.8410  -0.2620   -23.75%   384  coq-stdlib/MSets/MSetAVL.v.html                             │
│ 1.3870  1.1900  -0.1970   -14.20%   316  coq-stdlib/Strings/Byte.v.html                              │
│ 1.0770  0.8810  -0.1960   -18.20%   170  coq-stdlib/Numbers/HexadecimalNat.v.html                    │
│ 0.8640  0.6810  -0.1830   -21.18%   203  coq-stdlib/setoid_ring/Ncring_tac.v.html                    │
│ 1.4020  1.2280  -0.1740   -12.41%   374  coq-stdlib/setoid_ring/Ncring_polynom.v.html                │
│ 0.7140  0.5460  -0.1680   -23.53%   343  coq-stdlib/setoid_ring/Ncring_polynom.v.html                │
│ 0.3690  0.2070  -0.1620   -43.90%   637  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html            │
│ 0.8930  0.7320  -0.1610   -18.03%   160  coq-stdlib/Numbers/HexadecimalNat.v.html                    │
│ 0.1780  0.0200  -0.1580   -88.76%  1307  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html             │
│ 0.1520  0.0010  -0.1510   -99.34%  1903  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html             │
│ 0.3530  0.2040  -0.1490   -42.21%   204  coq-stdlib/setoid_ring/Ncring_tac.v.html                    │
│ 0.3710  0.2240  -0.1470   -39.62%   637  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html            │
│ 0.1610  0.0140  -0.1470   -91.30%  1201  coq-stdlib/Reals/Abstract/ConstructiveRealsMorphisms.v.html │
│ 0.1470  0.0000  -0.1470  -100.00%  1910  coq-stdlib/FSets/FMapFacts.v.html                           │
│ 0.4810  0.3350  -0.1460   -30.35%   705  coq-stdlib/Numbers/HexadecimalFacts.v.html                  │
│ 1.0090  0.8680  -0.1410   -13.97%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                    │
│ 0.2500  0.1100  -0.1400   -56.00%   351  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html  │
│ 0.3010  0.1640  -0.1370   -45.51%  2037  coq-stdlib/FSets/FMapAVL.v.html                             │
│ 0.2730  0.1380  -0.1350   -49.45%  1845  coq-stdlib/FSets/FMapAVL.v.html                             │
│ 0.1340  0.0020  -0.1320   -98.51%   679  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html             │
│ 0.1460  0.0150  -0.1310   -89.73%   396  coq-stdlib/MSets/MSetAVL.v.html                             │
│ 0.1230  0.0000  -0.1230  -100.00%   768  coq-stdlib/QArith/QArith_base.v.html                        │
└──────────────────────────────────────────────────────────────────────────────────────────────────────┘

@SkySkimmer
Copy link
Contributor Author

Summary of fiat_crypto_via_setoid_rewrite_standalone.v:

{
  "args": {
    "subtimes": {
      "Conversion": "5.33E+07 us, 12974960 calls",
      "Typeops.infer": "6.27E+04 us, 269 calls",
      "check-wf-univs": "3.45E+03 us, 269 calls",
      "close_proof": "3.47E+03 us, 76 calls",
      "command": "8.24E+08 us, 509 calls",
      "init": "5.45E+03 us, 1 call",
      "intern": "1.79E+05 us, 806 calls",
      "interp": "8.24E+08 us, 433 calls",
      "interp-delayed-qed": "2.63E+04 us, 76 calls",
      "kernel": "1.2E+05 us, 1377 calls",
      "parse_command": "2.87E+04 us, 510 calls",
      "pretyping": "1.43E+07 us, 3083964 calls",
      "synterp": "5.78E+04 us, 433 calls",
      "typeclass search": "1.2E+08 us, 2677 calls",
      "unfreeze_full_state": "1.01E+04 us, 736 calls",
      "unification": "2.45E+08 us, 67171072 calls",
      "universes_of_constr": "2.33E+03 us, 422 calls"
    },
    "major": "4.65E+08 w",
    "minor": "3.12E+11 w"
  },
  "name": "process",
  "ph": "E",
  "ts": 1686235869987325,
  "pid": 30626,
  "tid": 30626
}

@Janno
Copy link
Contributor

Janno commented Jun 9, 2023

This looks very interesting. I could see this becoming a less noisy alternative to perf when trying to answer high-level performance questions.

Do you know that printing directly won't lead to skewed results? When I implemented profiling in Mtac2 I had no choice but to collect everything into a list because the printing alone would distort nested events to the point of being unusable for any kind of microbenchmarks. It can be especially annoying when events have very different durations because the smallest events would be most affected by printing happening within them whereas for larger events it would almost make no difference, relatively speaking.

One thing that would improve the usefulness of this change for me would be to use mtime's to_uint64_ns function (https://erratique.ch/software/mtime/doc/Mtime/index.html#val-to_uint64_ns) for timestamps. It corresponds to MONOTONIC_CLOCK on linux (which can be selected in perf with perf record -k MONOTONIC_CLOCK) and using it everywhere allows aligning traces across different profiling methods when they are collected simultaneously. We use it to align perf traces with our own internal automation traces and it works great. It gives us very fine-grained insight into which OCaml functions end up running during specific steps in our tactics.

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 9, 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-stdlib │  409.68  416.98  -1.75 │ 1739277622914  1762413796492  -1.31 │  1450793348282  1449495996903   0.09 │  659472   649356   1.56 │
│                   coq-core │  115.75  116.20  -0.39 │  451589474129   450629996090   0.21 │   479064161283   478342177849   0.15 │  291384   290300   0.37 │
│ coq-performance-tests-lite │ 1352.22  762.53  77.33 │ 6110961123188  3401466570946  79.66 │ 11235158549559  6035318300720  86.16 │ 1669716  1667768   0.12 │
└────────────────────────────┴────────────────────────┴─────────────────────────────────────┴──────────────────────────────────────┴─────────────────────────┘
🐢 Top 25 slow downs 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                      TOP 25 SLOW DOWNS                                                       │
│                                                                                                                              │
│   OLD       NEW       DIFF     %DIFF    Ln                  FILE                                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 130.9890  343.7220  212.7330   162.41%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 130.7900  342.2090  211.4190   161.65%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│  16.1390   59.6230   43.4840   269.43%   32  coq-performance-tests-lite/src/pattern.v.html                                   │
│   7.1610   29.5620   22.4010   312.82%   31  coq-performance-tests-lite/src/pattern.v.html                                   │
│   3.2100   14.4190   11.2090   349.19%   30  coq-performance-tests-lite/src/pattern.v.html                                   │
│   3.6430   10.4640    6.8210   187.24%  652  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   3.9110   10.6390    6.7280   172.03%  623  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   1.5010    7.0500    5.5490   369.69%   29  coq-performance-tests-lite/src/pattern.v.html                                   │
│   0.7500    3.5040    2.7540   367.20%   28  coq-performance-tests-lite/src/pattern.v.html                                   │
│  40.4680   42.3610    1.8930     4.68%  224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html  │
│   2.3530    3.1510    0.7980    33.91%  736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                          │
│   3.1540    3.8680    0.7140    22.64%   32  coq-performance-tests-lite/src/n_polymorphic_universes.v.html                   │
│   0.8750    1.3820    0.5070    57.94%  382  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                    │
│   2.8470    3.3100    0.4630    16.26%  487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                      │
│   0.1300    0.4800    0.3500   269.23%  133  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   0.1290    0.4430    0.3140   243.41%  190  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   1.4340    1.7060    0.2720    18.97%  316  coq-stdlib/Strings/Byte.v.html                                                  │
│   0.2450    0.4920    0.2470   100.82%   12  coq-stdlib/MSets/MSets.v.html                                                   │
│   0.0640    0.2630    0.1990   310.94%  219  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   0.1280    0.3180    0.1900   148.44%  579  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                    │
│   0.3710    0.5560    0.1850    49.87%  301  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html                             │
│   0.1550    0.3230    0.1680   108.39%  811  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html                              │
│   0.4420    0.6050    0.1630    36.88%  353  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                    │
│   0.1600    0.3110    0.1510    94.38%  431  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                          │
│   0.0050    0.1540    0.1490  2980.00%  730  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                          │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                           TOP 25 SPEED UPS                                           │
│                                                                                                      │
│  OLD     NEW     DIFF     %DIFF     Ln              FILE                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 1.9730  1.5280  -0.4450   -22.55%   209  coq-stdlib/setoid_ring/Ncring_tac.v.html                    │
│ 1.1280  0.7890  -0.3390   -30.05%   813  coq-stdlib/MSets/MSetRBT.v.html                             │
│ 1.1060  0.7920  -0.3140   -28.39%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                    │
│ 1.3430  1.0510  -0.2920   -21.74%   467  coq-stdlib/Numbers/DecimalFacts.v.html                      │
│ 0.6360  0.3680  -0.2680   -42.14%   868  coq-stdlib/MSets/MSetRBT.v.html                             │
│ 1.1480  0.9000  -0.2480   -21.60%   170  coq-stdlib/Numbers/HexadecimalNat.v.html                    │
│ 0.9730  0.7470  -0.2260   -23.23%   203  coq-stdlib/setoid_ring/Ncring_tac.v.html                    │
│ 2.7260  2.5130  -0.2130    -7.81%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html  │
│ 0.5060  0.2970  -0.2090   -41.30%   313  coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html            │
│ 0.9860  0.7880  -0.1980   -20.08%   160  coq-stdlib/Numbers/HexadecimalNat.v.html                    │
│ 0.6750  0.4780  -0.1970   -29.19%   564  coq-stdlib/setoid_ring/Ncring_polynom.v.html                │
│ 0.1770  0.0200  -0.1570   -88.70%  1307  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html             │
│ 0.3200  0.1670  -0.1530   -47.81%   315  coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html            │
│ 0.5840  0.4310  -0.1530   -26.20%   387  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html         │
│ 0.1530  0.0010  -0.1520   -99.35%  1903  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html             │
│ 0.1800  0.0350  -0.1450   -80.56%   880  coq-stdlib/Reals/Abstract/ConstructiveRealsMorphisms.v.html │
│ 0.1380  0.0000  -0.1380  -100.00%  1426  coq-stdlib/FSets/FMapFacts.v.html                           │
│ 0.1280  0.0000  -0.1280  -100.00%  1910  coq-stdlib/FSets/FMapFacts.v.html                           │
│ 0.1320  0.0070  -0.1250   -94.70%  1008  coq-stdlib/setoid_ring/Field_theory.v.html                  │
│ 0.1430  0.0180  -0.1250   -87.41%   214  coq-stdlib/MSets/MSetProperties.v.html                      │
│ 0.1250  0.0020  -0.1230   -98.40%   679  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html             │
│ 0.1360  0.0180  -0.1180   -86.76%  1201  coq-stdlib/Reals/Abstract/ConstructiveRealsMorphisms.v.html │
│ 0.2550  0.1370  -0.1180   -46.27%    12  coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html         │
│ 0.3480  0.2300  -0.1180   -33.91%    14  coq-stdlib/Numbers/Cyclic/Int63/Ring63.v.html               │
│ 0.2530  0.1360  -0.1170   -46.25%  1845  coq-stdlib/FSets/FMapAVL.v.html                             │
└──────────────────────────────────────────────────────────────────────────────────────────────────────┘

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 9, 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-stdlib │  408.17  411.76  -0.87 │ 1752168497494  1763756774243  -0.66 │  1450807392087  1449450495416   0.09 │  663844   651116    1.95 │
│                   coq-core │  114.41  113.15   1.11 │  470051564243   467299067519   0.59 │   478926771775   477940694438   0.21 │  291768   291360    0.14 │
│ coq-performance-tests-lite │ 1345.59  756.62  77.84 │ 6137145885783  3430758427880  78.89 │ 11242480150890  6040334578306  86.12 │ 1670096  1872988  -10.83 │
└────────────────────────────┴────────────────────────┴─────────────────────────────────────┴──────────────────────────────────────┴──────────────────────────┘
🐢 Top 25 slow downs 
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                       TOP 25 SLOW DOWNS                                                       │
│                                                                                                                               │
│   OLD       NEW       DIFF     %DIFF     Ln                  FILE                                                             │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 129.2910  341.9850  212.6940   164.51%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 129.0450  340.8540  211.8090   164.14%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│  16.1140   58.3800   42.2660   262.29%    32  coq-performance-tests-lite/src/pattern.v.html                                   │
│   7.1720   28.7550   21.5830   300.93%    31  coq-performance-tests-lite/src/pattern.v.html                                   │
│   3.2110   14.0170   10.8060   336.53%    30  coq-performance-tests-lite/src/pattern.v.html                                   │
│   3.6120   10.4900    6.8780   190.42%   652  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   3.8230   10.6710    6.8480   179.13%   623  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   1.4990    6.8820    5.3830   359.11%    29  coq-performance-tests-lite/src/pattern.v.html                                   │
│   0.7410    3.4190    2.6780   361.40%    28  coq-performance-tests-lite/src/pattern.v.html                                   │
│   3.1420    3.8480    0.7060    22.47%    32  coq-performance-tests-lite/src/n_polymorphic_universes.v.html                   │
│   0.1290    0.4870    0.3580   277.52%   133  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   1.1540    1.4730    0.3190    27.64%   853  coq-stdlib/FSets/FMapAVL.v.html                                                 │
│   0.1250    0.3760    0.2510   200.80%   190  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   0.3420    0.5760    0.2340    68.42%   870  coq-stdlib/MSets/MSetRBT.v.html                                                 │
│   1.2780    1.4940    0.2160    16.90%   372  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                    │
│   1.1570    1.3680    0.2110    18.24%   374  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                    │
│   0.6140    0.8180    0.2040    33.22%   203  coq-stdlib/setoid_ring/Ncring_tac.v.html                                        │
│   0.0950    0.2820    0.1870   196.84%   312  coq-stdlib/Reals/Abstract/ConstructiveAbs.v.html                                │
│   0.1780    0.3470    0.1690    94.94%   385  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                    │
│   0.6440    0.8130    0.1690    26.24%   813  coq-stdlib/MSets/MSetRBT.v.html                                                 │
│   0.0030    0.1590    0.1560  5200.00%  1303  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html                                 │
│   0.0580    0.2090    0.1510   260.34%   162  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
│   0.0030    0.1510    0.1480  4933.33%  1190  coq-stdlib/Reals/Abstract/ConstructiveRealsMorphisms.v.html                     │
│   0.0520    0.1950    0.1430   275.00%  1885  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html                                 │
│   0.0630    0.2030    0.1400   222.22%   219  coq-performance-tests-lite/PerformanceExperiments/Harness.v.html                │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                      TOP 25 SPEED UPS                                                      │
│                                                                                                                            │
│   OLD      NEW     DIFF     %DIFF     Ln                  FILE                                                             │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 41.0630  40.5630  -0.5000    -1.22%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html  │
│  1.5740   1.1670  -0.4070   -25.86%   566  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                    │
│  2.8060   2.4730  -0.3330   -11.87%  1001  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│  0.8390   0.5570  -0.2820   -33.61%   211  coq-stdlib/setoid_ring/Ncring_tac.v.html                                        │
│  3.6010   3.3790  -0.2220    -6.16%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                      │
│  3.0620   2.8720  -0.1900    -6.21%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                          │
│  1.9360   1.7540  -0.1820    -9.40%   583  coq-stdlib/Strings/Byte.v.html                                                  │
│  0.1480   0.0010  -0.1470   -99.32%  1903  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html                                 │
│  0.1770   0.0350  -0.1420   -80.23%  1307  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html                                 │
│  0.1460   0.0080  -0.1380   -94.52%   214  coq-stdlib/MSets/MSetProperties.v.html                                          │
│  0.2880   0.1550  -0.1330   -46.18%  1845  coq-stdlib/FSets/FMapAVL.v.html                                                 │
│  0.1550   0.0230  -0.1320   -85.16%  1201  coq-stdlib/Reals/Abstract/ConstructiveRealsMorphisms.v.html                     │
│  0.1630   0.0320  -0.1310   -80.37%   880  coq-stdlib/Reals/Abstract/ConstructiveRealsMorphisms.v.html                     │
│  0.1390   0.0080  -0.1310   -94.24%  1008  coq-stdlib/setoid_ring/Field_theory.v.html                                      │
│  0.1310   0.0030  -0.1280   -97.71%   679  coq-stdlib/Numbers/Cyclic/Int31/Cyclic31.v.html                                 │
│  0.1270   0.0000  -0.1270  -100.00%   768  coq-stdlib/QArith/QArith_base.v.html                                            │
│  0.3470   0.2330  -0.1140   -32.85%   719  coq-stdlib/MSets/MSetRBT.v.html                                                 │
│  0.1170   0.0090  -0.1080   -92.31%   644  coq-stdlib/ZArith/Znumtheory.v.html                                             │
│  0.2560   0.1490  -0.1070   -41.80%  1097  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html                              │
│  0.1320   0.0270  -0.1050   -79.55%   396  coq-stdlib/MSets/MSetAVL.v.html                                                 │
│  0.3170   0.2150  -0.1020   -32.18%    11  coq-stdlib/Reals/Alembert.v.html                                                │
│  0.3040   0.2030  -0.1010   -33.22%    11  coq-stdlib/setoid_ring/Rings_Q.v.html                                           │
│  0.3370   0.2410  -0.0960   -28.49%   637  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html                                │
│  0.1070   0.0110  -0.0960   -89.72%   136  coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html                             │
│  0.3400   0.2450  -0.0950   -27.94%    14  coq-stdlib/Numbers/Cyclic/Abstract/NZCyclic.v.html                              │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@ejgallego
Copy link
Member

IMHO a useful thing to have in a performance metric summary is a way to identify which calls are most costly, that is to say, "anomalous". For example it could be the case that the typechecking of some file is dominated by conversion or unification, but the interesting bit there is to try to know which calls are taking more time than they should.

@SkySkimmer SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Jun 16, 2023
@SkySkimmer
Copy link
Contributor Author

@coqbot bench

@SkySkimmer SkySkimmer mentioned this pull request Jun 16, 2023
Merged
3 tasks
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 17, 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-stdlib │  413.39   413.92  -0.13 │  1754125028175   1753923734878   0.01 │  1451104867333   1449440701849   0.11 │  663724   651376    1.90 │
│                     coq-core │  116.57   116.37   0.17 │   460671916863    453378381039   1.61 │   479068355125    478223996727   0.18 │  291368   292028   -0.23 │
│                coq-perennial │ 5908.16  5897.10   0.19 │ 26734657671604  26668608259086   0.25 │ 44743799767269  44748486394607  -0.01 │ 2114744  2132296   -0.82 │
│                 coq-compcert │  288.78   287.66   0.39 │  1289491367906   1285965635285   0.27 │  1967993443266   1967354774178   0.03 │ 1133232  1133348   -0.01 │
│               coq-coquelicot │   38.82    38.65   0.44 │   172090761005    170179675426   1.12 │   239366527102    239697680114  -0.14 │  786192   811624   -3.13 │
│       coq-mathcomp-character │  167.26   165.72   0.93 │   759020898590    751344785257   1.02 │  1185020457870   1172181597886   1.10 │ 1752612  1732252    1.18 │
│  coq-rewriter-perf-SuperFast │  753.24   746.15   0.95 │  3361266503669   3329011259253   0.97 │  5833515756818   5791348313386   0.73 │ 1309728  1433696   -8.65 │
│                coq-fourcolor │ 1577.48  1558.34   1.23 │  6971155977318   6894024388226   1.12 │ 12518332473393  12510775373012   0.06 │ 2283940  2290072   -0.27 │
│                  coq-unimath │ 1523.55  1504.98   1.23 │  6890739681447   6804935363930   1.26 │ 12923635776953  12844497414072   0.62 │ 1288852  1332172   -3.25 │
│                      coq-vst │  865.99   853.88   1.42 │  3899494393449   3841433052310   1.51 │  6387227290580   6381726151221   0.09 │ 2262144  2113936    7.01 │
│       coq-mathcomp-odd-order │  878.03   865.03   1.50 │  4005521218962   3942448978703   1.60 │  6688628487032   6633179939382   0.84 │ 1619284  1593096    1.64 │
│   coq-performance-tests-lite │  779.67   766.65   1.70 │  3476361698504   3421351234391   1.61 │  6152689875972   6044242410397   1.79 │ 1871708  1669168   12.13 │
│ coq-fiat-crypto-with-bedrock │ 6237.22  6126.54   1.81 │ 28086060563071  27554719033263   1.93 │ 51529639547290  51032510502458   0.97 │ 2414540  2410748    0.16 │
│       coq-mathcomp-ssreflect │  253.10   248.60   1.81 │  1144011016624   1123543977618   1.82 │  1993701918939   1985923342781   0.39 │ 4863780  4821216    0.88 │
│            coq-iris-examples │  491.51   482.46   1.88 │  2214970404240   2174065265234   1.88 │  3370028127276   3339789126588   0.91 │ 1087756  1079132    0.80 │
│      coq-metacoq-safechecker │  381.28   373.94   1.96 │  1735307121597   1700648035437   2.04 │  2890353424063   2852433935512   1.33 │ 2007292  2050772   -2.12 │
│           coq-mathcomp-field │  252.51   247.51   2.02 │  1141142934812   1117228521137   2.14 │  1940126940235   1927832276517   0.64 │ 1570068  1560312    0.63 │
│                 coq-rewriter │  357.04   349.83   2.06 │  1607765692725   1575449838120   2.05 │  2674563415231   2627225771156   1.80 │ 1212696  1211852    0.07 │
│         coq-mathcomp-algebra │  683.20   669.31   2.08 │  3084926906696   3019156309330   2.18 │  5367872920989   5351498597787   0.31 │ 3759836  4184484  -10.15 │
│             coq-fiat-parsers │  336.23   329.03   2.19 │  1482283908598   1449317935017   2.27 │  2462184886526   2439729739386   0.92 │ 2394568  2421112   -1.10 │
│                     coq-corn │  801.89   781.72   2.58 │  3614999209026   3521905685502   2.64 │  5579721327175   5509262002685   1.28 │  812196   742184    9.43 │
│          coq-category-theory │  737.82   719.13   2.60 │  3349290478623   3263536058368   2.63 │  5701855566133   5621342376163   1.43 │  884380   895776   -1.27 │
│        coq-mathcomp-solvable │  152.72   148.70   2.70 │   691883773773    673676296024   2.70 │  1102998551317   1087158009937   1.46 │ 1732664  1727292    0.31 │
│             coq-math-classes │   87.36    85.05   2.72 │   390734665974    379986341522   2.83 │   545379832281    538625909124   1.25 │  519216   520608   -0.27 │
│          coq-metacoq-erasure │  314.77   306.18   2.81 │  1415398250993   1376000970937   2.86 │  2228592565275   2195976316640   1.49 │ 2038828  2047144   -0.41 │
│        coq-engine-bench-lite │  160.97   156.41   2.92 │   685237273778    665904004315   2.90 │  1280883054103   1253022348669   2.22 │ 1325892  1324340    0.12 │
│            coq-metacoq-pcuic │  640.23   621.94   2.94 │  2880254675193   2794640096940   3.06 │  4230206062428   4156179619664   1.78 │ 1901988  2091800   -9.07 │
│         coq-metacoq-template │  168.28   163.26   3.07 │   743369449812    719936193312   3.25 │  1175892107652   1157912656202   1.55 │ 1299008  1260252    3.08 │
│                 coq-bedrock2 │  323.80   314.03   3.11 │  1460178120890   1416340193804   3.10 │  2830659361793   2807382354104   0.83 │  841600   838836    0.33 │
│                     coq-hott │  153.18   148.55   3.12 │   685569556182    664339416409   3.20 │  1076608181021   1059724607554   1.59 │  626932   620976    0.96 │
│        coq-mathcomp-fingroup │   39.08    37.77   3.47 │   177430838360    171475904521   3.47 │   268234181253    262739182124   2.09 │  570044   569868    0.03 │
│     coq-metacoq-translations │   18.47    17.85   3.47 │    80797516798     78120093812   3.43 │   130839024655    128336397300   1.95 │  907184   905868    0.15 │
│                  coq-bignums │   28.99    27.91   3.87 │   130385159757    125377673335   3.99 │   185841928405    180893016314   2.74 │  486712   486764   -0.01 │
│                coq-fiat-core │   61.92    59.28   4.45 │   260824280719    251477969936   3.72 │   380132292612    374817528126   1.42 │  492856   491744    0.23 │
│                  coq-coqutil │   40.86    38.96   4.88 │   181274186653    172262102424   5.23 │   259312933568    251843898323   2.97 │  560820   560552    0.05 │
│                    coq-color │  235.04   223.60   5.12 │  1048856489631    997678656250   5.13 │  1511212430206   1470390174151   2.78 │ 1155152  1168740   -1.16 │
│                coq-equations │   11.19    10.64   5.17 │    47722127143     45982107901   3.78 │    74886814367     73222905730   2.27 │  421168   415236    1.43 │
│                 coq-coqprime │   47.84    45.47   5.21 │   214121822993    202387066201   5.80 │   323114083641    312095485056   3.53 │  779908   776768    0.40 │
│                    coq-verdi │   49.42    46.88   5.42 │   220528932759    209548897151   5.24 │   336795321818    323289900779   4.18 │  529376   531124   -0.33 │
│               coq-verdi-raft │  588.27   556.80   5.65 │  2666932145493   2521641658601   5.76 │  4126127335361   3974700277697   3.81 │  821500   818944    0.31 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
coq-geocoq

🐢 Top 25 slow downs 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                         TOP 25 SLOW DOWNS                                                          │
│                                                                                                                                    │
│   OLD       NEW      DIFF   %DIFF    Ln                   FILE                                                                     │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 131.7620  136.0200  4.2580   3.23%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html          │
│ 131.9730  136.2060  4.2330   3.21%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html          │
│  64.9830   68.6370  3.6540   5.62%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                      │
│ 124.0760  126.6460  2.5700   2.07%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                   │
│  15.8240   17.8800  2.0560  12.99%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                │
│  15.4360   17.2610  1.8250  11.82%  3158  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                      │
│  80.4790   82.2730  1.7940   2.23%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                              │
│  38.2010   39.7540  1.5530   4.07%   835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                   │
│  80.8610   82.3750  1.5140   1.87%   618  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                              │
│ 111.4520  112.8850  1.4330   1.29%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                  │
│   8.5960    9.9800  1.3840  16.10%   496  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                             │
│   8.4830    9.8480  1.3650  16.09%   496  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html                              │
│  14.7030   16.0080  1.3050   8.88%   417  coq-verdi-raft/raft-proofs/LeaderLogsLogMatchingProof.v.html                             │
│  16.0880   17.2880  1.2000   7.46%    32  coq-performance-tests-lite/src/pattern.v.html                                            │
│   9.9570   11.1280  1.1710  11.76%   827  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                │
│  20.6660   21.6550  0.9890   4.79%  1495  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/UnivalentKleisliEnriched.v.html │
│   8.1280    9.0990  0.9710  11.95%   828  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                │
│  13.0690   14.0390  0.9700   7.42%  3090  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                      │
│   9.3870   10.3020  0.9150   9.75%  1271  coq-verdi-raft/raft/CommonTheorems.v.html                                                │
│   7.5740    8.4750  0.9010  11.90%   829  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                │
│   5.5160    6.3900  0.8740  15.84%  1391  coq-perennial/src/program_proof/aof/proof.v.html                                         │
│   6.8840    7.7110  0.8270  12.01%   830  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                │
│  26.9860   27.8030  0.8170   3.03%    12  coq-fourcolor/theories/job486to489.v.html                                                │
│   8.6800    9.4730  0.7930   9.14%   914  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                │
│  14.0140   14.8000  0.7860   5.61%   317  coq-fiat-crypto-with-bedrock/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v.html        │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                     │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  42.4280   40.5370  -1.8910   -4.46%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                          │
│  20.2850   18.5320  -1.7530   -8.64%   808  coq-perennial/src/program_proof/wal/logger_proof.v.html                                                 │
│  43.2500   41.6700  -1.5800   -3.65%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html               │
│  42.8190   41.2620  -1.5570   -3.64%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                              │
│  50.0490   48.6430  -1.4060   -2.81%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                       │
│  41.2960   39.9590  -1.3370   -3.24%   368  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                       │
│  35.2910   34.3720  -0.9190   -2.60%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│  32.6550   31.7870  -0.8680   -2.66%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│  25.1750   24.3400  -0.8350   -3.32%    20  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  25.1650   24.3680  -0.7970   -3.17%    25  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│   8.6360    7.9260  -0.7100   -8.22%   723  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                                         │
│  19.7390   19.0580  -0.6810   -3.45%    28  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│   7.3330    6.7080  -0.6250   -8.52%   860  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                  │
│  47.1310   46.5530  -0.5780   -1.23%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│   1.4750    0.9200  -0.5550  -37.63%   382  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                                            │
│ 159.1880  158.6410  -0.5470   -0.34%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│   5.3000    4.8840  -0.4160   -7.85%   747  coq-perennial/src/program_proof/fencing/frontend_proof.v.html                                           │
│  13.1140   12.7050  -0.4090   -3.12%    15  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│   1.0650    0.6750  -0.3900  -36.62%   816  coq-stdlib/MSets/MSetRBT.v.html                                                                         │
│   4.9100    4.5260  -0.3840   -7.82%   620  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/FunctorCategory.v.html                         │
│   4.5690    4.2040  -0.3650   -7.99%  2764  coq-iris-examples/theories/logatom/herlihy_wing_queue/hwq.v.html                                        │
│  25.8880   25.5330  -0.3550   -1.37%  2293  coq-perennial/src/goose_lang/logical_reln_fund.v.html                                                   │
│  80.9240   80.5830  -0.3410   -0.42%   618  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│  52.4290   52.0900  -0.3390   -0.65%    50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│   0.3810    0.0470  -0.3340  -87.66%  1447  coq-perennial/src/program_proof/aof/proof.v.html                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@SkySkimmer
Copy link
Contributor Author

Unrelated bench https://gitlab.com/coq/coq/-/jobs/4488727880: 126MB artifacts
This bench https://gitlab.com/coq/coq/-/jobs/4488304313: 193MB artifacts

@SkySkimmer
Copy link
Contributor Author

Removed the minimum time based skip

@coqbot bench

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 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-stdlib │  409.43   415.66  -1.50 │  1740513277308   1766532821065  -1.47 │  1447482073393   1446376896508   0.08 │  657032   646488   1.63 │
│                coq-perennial │ 5880.35  5898.85  -0.31 │ 26593497510827  26683153059213  -0.34 │ 44733862196640  44754198602153  -0.05 │ 2219836  2219324   0.02 │
│                     coq-core │  115.03   115.35  -0.28 │   461167961411    459011369194   0.47 │   479149228203    478591932822   0.12 │  291748   292268  -0.18 │
│                      coq-vst │  860.16   858.47   0.20 │  3870077985423   3862632321218   0.19 │  6377613740378   6371283225265   0.10 │ 1947940  2113816  -7.85 │
│                coq-fourcolor │ 1557.05  1550.58   0.42 │  6883507832034   6858458933534   0.37 │ 12523074214042  12501706629301   0.17 │ 2282124  2289788  -0.33 │
│               coq-coquelicot │   38.50    38.26   0.63 │   170545819214    169296994904   0.74 │   239162808207    239451576755  -0.12 │  784192   810124  -3.20 │
│                 coq-compcert │  285.47   283.58   0.67 │  1276160151837   1269560603621   0.52 │  1963162100677   1961337087987   0.09 │ 1133696  1132300   0.12 │
│       coq-mathcomp-odd-order │  878.09   871.72   0.73 │  4001819590796   3972402650513   0.74 │  6690616759634   6627982248712   0.95 │ 1607320  1471232   9.25 │
│           coq-mathcomp-field │  251.40   249.50   0.76 │  1135629568746   1127933514984   0.68 │  1939791634561   1928113484346   0.61 │ 1432788  1431440   0.09 │
│        coq-mathcomp-solvable │  150.52   149.26   0.84 │   682398161620    676200063678   0.92 │  1103430240363   1085665649771   1.64 │ 1723680  1715216   0.49 │
│            coq-iris-examples │  483.19   478.20   1.04 │  2179797923110   2156390444095   1.09 │  3362852247472   3322195613218   1.22 │ 1074000  1051636   2.13 │
│       coq-mathcomp-character │  168.01   166.08   1.16 │   763401964378    754162858157   1.23 │  1184828253313   1170837556503   1.19 │ 1597448  1597004   0.03 │
│                  coq-unimath │ 1523.11  1505.34   1.18 │  6888414248559   6807216834512   1.19 │ 12929730397065  12825186294312   0.82 │ 1273116  1325696  -3.97 │
│                 coq-bedrock2 │  320.24   315.95   1.36 │  1445540976171   1425640518395   1.40 │  2828689407097   2803429586457   0.90 │  845840   831548   1.72 │
│  coq-rewriter-perf-SuperFast │  752.98   742.73   1.38 │  3362247649414   3315464163512   1.41 │  5828570323820   5783355015101   0.78 │ 1310724  1309000   0.13 │
│             coq-fiat-parsers │  334.05   329.17   1.48 │  1473040482171   1450440747676   1.56 │  2459715250147   2433976276287   1.06 │ 2401104  2422288  -0.87 │
│        coq-engine-bench-lite │  160.76   158.31   1.55 │   683597639326    673170816868   1.55 │  1280834203526   1260753212663   1.59 │ 1207216  1209324  -0.17 │
│         coq-mathcomp-algebra │  675.98   665.03   1.65 │  3057724209621   3004862014421   1.76 │  5369756408769   5348659844401   0.39 │ 2060160  2056280   0.19 │
│ coq-fiat-crypto-with-bedrock │ 6224.28  6111.12   1.85 │ 28013246126865  27496106471457   1.88 │ 51517502689305  50984245234740   1.05 │ 2321000  2307800   0.57 │
│                     coq-corn │  791.58   774.85   2.16 │  3570645938775   3493234973983   2.22 │  5574725912310   5489945428888   1.54 │  812284   742364   9.42 │
│          coq-metacoq-erasure │  311.72   304.53   2.36 │  1401318695139   1368249961445   2.42 │  2228562445867   2190760687368   1.73 │ 2028248  2045524  -0.84 │
│          coq-category-theory │  737.30   720.18   2.38 │  3346901913554   3265288885915   2.50 │  5708289058198   5620154152874   1.57 │  868044   893092  -2.80 │
│                coq-fiat-core │   60.63    59.21   2.40 │   257818266030    251166159814   2.65 │   380942149872    374048030087   1.84 │  490168   489200   0.20 │
│                coq-equations │   11.04    10.78   2.41 │    47726842902     46030915518   3.68 │    75280216741     73123593594   2.95 │  412240   411404   0.20 │
│             coq-math-classes │   86.83    84.78   2.42 │   388402023608    378610779327   2.59 │   546766191368    538784643641   1.48 │  519256   517280   0.38 │
│        coq-mathcomp-fingroup │   38.80    37.84   2.54 │   176197796707    171761638230   2.58 │   268866060684    262205982439   2.54 │  555688   556572  -0.16 │
│      coq-metacoq-safechecker │  384.29   374.38   2.65 │  1749550070580   1703399504756   2.71 │  2892661610524   2851044206893   1.46 │ 2000716  2049472  -2.38 │
│                 coq-rewriter │  358.83   349.30   2.73 │  1617162352765   1574150448098   2.73 │  2672106150615   2621710561994   1.92 │ 1215412  1211872   0.29 │
│         coq-metacoq-template │  167.14   162.70   2.73 │   738790290890    717897877108   2.91 │  1176488758701   1152894701206   2.05 │ 1283676  1259460   1.92 │
│            coq-metacoq-pcuic │  637.29   620.31   2.74 │  2867962980031   2787360249075   2.89 │  4236072602688   4147347859907   2.14 │ 1897692  2095524  -9.44 │
│       coq-mathcomp-ssreflect │  254.67   247.70   2.81 │  1149834266433   1119633194092   2.70 │  1993762183663   1980144194678   0.69 │ 2915836  2631736  10.80 │
│     coq-metacoq-translations │   18.30    17.79   2.87 │    80289000829     77798685197   3.20 │   131154135529    128192647115   2.31 │  906256   908524  -0.25 │
│                     coq-hott │  153.42   149.14   2.87 │   685676316381    665926343160   2.97 │  1080968916957   1058113217228   2.16 │  627044   621296   0.93 │
│                  coq-coqutil │   40.35    39.22   2.88 │   179881288293    172672692919   4.17 │   260076521346    251461791289   3.43 │  559096   558680   0.07 │
│   coq-performance-tests-lite │  787.02   763.37   3.10 │  3511378585123   3401488910244   3.23 │  6157126956584   6041849675505   1.91 │ 1873372  1667804  12.33 │
│                  coq-bignums │   28.86    27.78   3.89 │   130188086597    124680789684   4.42 │   186286991267    180423011892   3.25 │  482980   482152   0.17 │
│                    coq-color │  232.19   222.79   4.22 │  1037032201167    993951159769   4.33 │  1517572345826   1466156881574   3.51 │ 1126108  1166744  -3.48 │
│               coq-verdi-raft │  584.85   555.77   5.23 │  2654042588997   2518213962926   5.39 │  4125113078201   3971240062715   3.87 │  809580   812916  -0.41 │
│                 coq-coqprime │   47.61    45.21   5.31 │   212974632592    201698859359   5.59 │   325268477554    311136917973   4.54 │  774904   775804  -0.12 │
│                    coq-verdi │   49.42    46.79   5.62 │   221636909544    208948832642   6.07 │   337785497900    322915980579   4.60 │  523256   526172  -0.55 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-geocoq

🐢 Top 25 slow downs 
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                         TOP 25 SLOW DOWNS                                                         │
│                                                                                                                                   │
│   OLD       NEW      DIFF   %DIFF    Ln                   FILE                                                                    │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 129.7760  137.9340  8.1580   6.29%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html         │
│ 130.1090  138.0960  7.9870   6.14%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html         │
│  65.3640   68.3280  2.9640   4.53%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                     │
│ 123.7510  126.4160  2.6650   2.15%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                  │
│ 112.5270  114.5930  2.0660   1.84%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                 │
│  15.9230   17.7890  1.8660  11.72%    32  coq-performance-tests-lite/src/pattern.v.html                                           │
│  51.8080   53.5420  1.7340   3.35%   915  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html               │
│  15.3370   17.0670  1.7300  11.28%  3158  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                     │
│ 212.1770  213.8190  1.6420   0.77%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html              │
│   8.4590   10.0370  1.5780  18.65%   496  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html                             │
│  16.2480   17.8260  1.5780   9.71%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                               │
│  38.1720   39.6450  1.4730   3.86%   835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                  │
│   8.4020    9.8750  1.4730  17.53%   496  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                            │
│  14.5390   15.7420  1.2030   8.27%   417  coq-verdi-raft/raft-proofs/LeaderLogsLogMatchingProof.v.html                            │
│  80.2860   81.3220  1.0360   1.29%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                             │
│   8.6630    9.6580  0.9950  11.49%   192  coq-vst/veric/binop_lemmas5.v.html                                                      │
│ 122.2010  123.1870  0.9860   0.81%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html              │
│  13.7030   14.6450  0.9420   6.87%   615  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html │
│  13.0590   13.9590  0.9000   6.89%  3090  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                     │
│  10.0010   10.8660  0.8650   8.65%   827  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html               │
│  13.7710   14.6300  0.8590   6.24%   613  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html │
│  59.2910   60.1360  0.8450   1.43%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                │
│   9.4840   10.3100  0.8260   8.71%  1271  coq-verdi-raft/raft/CommonTheorems.v.html                                               │
│   5.2650    6.0730  0.8080  15.35%   172  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html    │
│   8.5640    9.3560  0.7920   9.25%  1078  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                          │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                     │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  33.9990   31.4090  -2.5900   -7.62%  1730  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                                         │
│  22.8720   20.6170  -2.2550   -9.86%  1357  coq-perennial/src/program_proof/wal/installer_proof.v.html                                              │
│  81.9990   80.4350  -1.5640   -1.91%   618  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│  82.6760   81.2620  -1.4140   -1.71%   618  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│  47.0140   46.1810  -0.8330   -1.77%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                         │
│  36.7740   35.9690  -0.8050   -2.19%   522  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html                                    │
│   7.9460    7.1430  -0.8030  -10.11%   881  coq-vst/veric/binop_lemmas4.v.html                                                                      │
│  46.9620   46.1820  -0.7800   -1.66%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│ 158.0850  157.3090  -0.7760   -0.49%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│   2.7970    2.1020  -0.6950  -24.85%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                                                  │
│   8.6660    8.0410  -0.6250   -7.21%   723  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                                         │
│   9.9220    9.3910  -0.5310   -5.35%    40  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html            │
│   4.6420    4.1230  -0.5190  -11.18%   130  coq-category-theory/Functor/Strong/Product.v.html                                                       │
│   1.3740    0.8550  -0.5190  -37.77%   382  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                                            │
│  28.2490   27.7600  -0.4890   -1.73%   194  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│  13.8180   13.3590  -0.4590   -3.32%   187  coq-perennial/src/goose_lang/interpreter/disk_interpreter.v.html                                        │
│  52.6490   52.1920  -0.4570   -0.87%    50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  30.2440   29.8040  -0.4400   -1.45%    12  coq-fourcolor/theories/job190to206.v.html                                                               │
│   5.7600    5.3460  -0.4140   -7.19%   429  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                                          │
│   1.0660    0.6660  -0.4000  -37.52%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                                                                │
│   1.5820    1.2540  -0.3280  -20.73%  1874  coq-perennial/src/program_proof/wal/recovery_proof.v.html                                               │
│   1.5000    1.1760  -0.3240  -21.60%   372  coq-stdlib/setoid_ring/Ncring_polynom.v.html                                                            │
│   3.2520    2.9300  -0.3220   -9.90%  1409  coq-perennial/src/program_proof/wal/installer_proof.v.html                                              │
│   4.3010    3.9880  -0.3130   -7.28%   128  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│  29.0360   28.7290  -0.3070   -1.06%   147  coq-vst/veric/expr_lemmas4.v.html                                                                       │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@SkySkimmer
Copy link
Contributor Author

Unrelated bench gitlab.com/coq/coq/-/jobs/4488727880: 126MB artifacts
This bench gitlab.com/coq/coq/-/jobs/4488304313: 193MB artifacts

https://gitlab.com/coq/coq/-/jobs/4498167930: 240MB artifacts

@SkySkimmer
Copy link
Contributor Author

The largest is for https://github.com/thery/coqprime/blob/master/src/Coqprime/examples/BasePrimes.v which is a file with 25k commands. The .gz is 1.3MiB.

@SkySkimmer SkySkimmer marked this pull request as ready for review June 20, 2023 10:31
@SkySkimmer SkySkimmer requested review from a team as code owners June 20, 2023 10:31
SkySkimmer and others added 7 commits September 15, 2023 13:46
@SkySkimmer
coq_makefile produces profile info when PROFILING set, bench sets it
f167000 
profiles seem to compress well, for instance from profiling Hurkens:

- .vo: 48KB (for reference)
- .prof.json: 2.6MB
- .prof.json.gz: 144KB (compression level 6 (default))
- .prof.json.gz: 124KB (compression level 9 (best))
- .prof.json.xz: 108KB (compression level 6 (default); also 9)
- .prof.json.7z: 116KB
- .prof.json.zip: 124KB (compression level 9)

The chrome displayer supports importing straight from gzip so we use that.
@SkySkimmer
newprofile: include sum of times and call counts of subcategories in …
6c72e50 
…args

although this could be computed afterwards this makes it easier to
display

nb because we sum floats accuracy may be shit
@SkySkimmer
newprofile: filter components to print events for using COQ_PROFILE_C…
67a44fd 
…OMPONENTS

This interacts a bit weirdly with the minimum duration based skip, but
maybe I'll remove the skip if this works well enough.
@SkySkimmer
newprofile: include line number for "command" component extra data
306cdb7
@SkySkimmer
Doc for newprofile
187b82c
@SkySkimmer @jfehrle
Apply suggestions from code review
695d1f7 
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
@SkySkimmer
Changed NewProfile.MiniJson.t to polymorphic variants matching yojson
664ec4d
ejgallego
ejgallego approved these changes Sep 15, 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.

We will address the API tweaks in a further PR.

The issue of what JSON library Coq should use is referred to the next call.

@SkySkimmer
Copy link
Contributor Author

I considered printing to a buffer originally but using Printf.fprintf in the subprints forces out_channel which confused me.
I guess it should be fine to use Format instead, then we can do of_out_channel of_buffer etc.

@ejgallego
Copy link
Member

I considered printing to a buffer originally but using Printf.fprintf in the subprints forces out_channel which confused me. I guess it should be fine to use Format instead, then we can do of_out_channel of_buffer etc.

Yes. IMHO the current default is good for coqc, it is better to flush directly to disk than to take valious RAM. Finer printing is only needed when you want to recheck only a part of the document.

@SkySkimmer
Copy link
Contributor Author

I think I understand better what you want after thinking about this printf / format stuff, cf new commits

@ejgallego
Copy link
Member

I think I understand better what you want after thinking about this printf / format stuff, cf new commits

Thanks Gaëtan, this will be a good basis to start implementing the incremental support.

I'm happy to merge now, not sure if we want to run the full CI tho? Gonna do it "just in case"

I'd be nice to have the dune build @check for all plugins in the light pipeline, that would help quite a bit in PRs like this.

@ejgallego
Copy link
Member

@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 Sep 15, 2023
@SkySkimmer SkySkimmer mentioned this pull request Sep 15, 2023
Open
ejgallego
ejgallego reviewed Sep 15, 2023
View reviewed changes
lib/newProfile.ml

let f fmt = match !accu with
| None -> assert false
| Some { ch } -> Format.fprintf ch fmt
Copy link
Member

Choose a reason for hiding this comment

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

@SkySkimmer you may want to add a flush here if you want to have fully synchonous semantics, Format can buffer aggresively some times.

This can also be done using the specifier %! , or via the kprintf family of functions.

@ejgallego
Copy link
Member

@coqbot: merge now

@coqbot-app coqbot-app bot merged commit a99e6ec into coq:master Sep 16, 2023
8 checks passed
@ejgallego
Copy link
Member

Still note the comments about flush, that could need a tweak in a further PR.

@SkySkimmer SkySkimmer deleted the trace branch September 18, 2023 10:42
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 10, 2023
@coqbot-app @ejgallego @rlepigre
Merge PR coq#17702: Produce profiles in google trace format
f5035a5 
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: rlepigre
Co-authored-by: ejgallego <ejgallego@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 10, 2023
@coqbot-app @ejgallego @rlepigre
Merge PR coq#17702: Produce profiles in google trace format
9dc7f65 
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: rlepigre
Co-authored-by: ejgallego <ejgallego@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 16, 2023
@coqbot-app @ejgallego @rlepigre
Merge PR coq#17702: Produce profiles in google trace format
79525a2 
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: rlepigre
Co-authored-by: ejgallego <ejgallego@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 16, 2023
@coqbot-app @ejgallego @rlepigre
Merge PR coq#17702: Produce profiles in google trace format
b727607 
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: rlepigre
Co-authored-by: ejgallego <ejgallego@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 25, 2023
@coqbot-app @ejgallego @rlepigre
Merge PR coq#17702: Produce profiles in google trace format
4c5c1ae 
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: rlepigre
Co-authored-by: ejgallego <ejgallego@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Oct 30, 2023
@coqbot-app @ejgallego @rlepigre
Merge PR coq#17702: Produce profiles in google trace format
a65eec9 
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: rlepigre
Co-authored-by: ejgallego <ejgallego@users.noreply.github.com>
@rlepigre rlepigre mentioned this pull request Dec 1, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jfehrle jfehrle jfehrle left review comments

@rlepigre rlepigre rlepigre left review comments

@ejgallego ejgallego ejgallego approved these changes

@gares gares gares approved these changes

Assignees

@ejgallego ejgallego

Labels
kind: feature New user-facing feature request or implementation. kind: infrastructure CI, build tools, development tools.
Projects
None yet
Milestone
8.19+rc1
Development

Successfully merging this pull request may close these issues.

None yet
7 participants
@SkySkimmer @Alizter @ejgallego @Janno @jfehrle @gares @rlepigre