Evarconv: save keys #19611

Tragicus · 2024-09-27T11:31:37Z

Saves the head constant of a term before delta-reducing it, to be used during canonical structure resolution and to find matching heads.
Also prevents trying to solve canonical structure problems of the form S.proj s ~ t when s reduces to an applied constructor.

Fixes / closes #????

Added / updated test-suite.

Added changelog.
Added / updated documentation.
- Documented any new / changed user messages.
- Updated documented syntax by running make doc_gram_rsts.

Overlays (to be merged before the current PR)

mathcomp-analysis: adapt to coq#19611 math-comp/analysis#1377
odd-order: annotate card_vspace1 math-comp/odd-order#60
hott: Adapt to Coq#19611 HoTT/Coq-HoTT#2127
fcsl-pcm: Adapt to coq#pr19611 imdea-software/fcsl-pcm#45

SkySkimmer · 2024-09-27T11:50:33Z

@coqbot run full ci

SkySkimmer · 2024-09-27T11:52:46Z

started a bench manually to have the mathcomp overlay

pi8027 · 2024-09-27T12:25:34Z

FYI, I started porting lemma-overloading to recent versions of Coq and MathComp. I think this is a good stress test for this PR. (I don't think I will finish it quickly though.)

coqbot-app · 2024-09-28T02:31:12Z

🏁 Bench results:

┌─────────────────────────────────────┬──────────────────────────┬────────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]       │            CPU instructions            │  max resident mem [KB]  │
│                                     │                          │                                        │                         │
│            package_name             │   NEW      OLD    PDIFF  │      NEW             OLD        PDIFF  │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼──────────────────────────┼────────────────────────────────────────┼─────────────────────────┤
│              coq-mathcomp-ssreflect │   89.55   105.71  -15.29 │   593765703433    675097586725  -12.05 │ 1708612  1601036   6.72 │
│                  coq-mathcomp-field │   86.00    89.71   -4.14 │   600885944213    624864974808   -3.84 │ 1216220  1222288  -0.50 │
│                coq-mathcomp-algebra │  140.03   145.09   -3.49 │   943208861313    974396403803   -3.20 │ 1246296  1217864   2.33 │
│                            coq-core │  131.88   133.17   -0.97 │   538775747363    537923375867    0.16 │  464636   463612   0.22 │
│                      coq-coquelicot │   36.21    36.38   -0.47 │   219058827535    219457366312   -0.18 │  806192   797560   1.08 │
│                         coq-bignums │   29.15    29.27   -0.41 │   187620597553    187670802631   -0.03 │  466892   466732   0.03 │
│                    coq-math-classes │   82.89    83.12   -0.28 │   510039285588    509907834273    0.03 │  503612   505028  -0.28 │
│            coq-metacoq-translations │   16.24    16.28   -0.25 │   116717921642    116650628876    0.06 │  774664   776028  -0.18 │
│         coq-rewriter-perf-SuperFast │  760.00   761.82   -0.24 │  5897070818265   5893652429846    0.06 │ 1417276  1405464   0.84 │
│                        coq-bedrock2 │  324.48   325.18   -0.22 │  2759798121663   2758721757276    0.04 │  854256   855004  -0.09 │
│                        coq-compcert │  296.59   296.93   -0.11 │  1969076554753   1968900609438    0.01 │ 1043524  1099004  -5.05 │
│                           coq-color │  242.15   242.38   -0.09 │  1530532602613   1530169927014    0.02 │ 1134936  1141108  -0.54 │
│                        coq-rewriter │  336.93   336.99   -0.02 │  2522840750122   2520893274970    0.08 │ 1320152  1312212   0.61 │
│                 coq-metacoq-erasure │  518.64   518.51    0.03 │  3629447415427   3617390942937    0.33 │ 1910368  1880440   1.59 │
│                coq-metacoq-template │  144.95   144.88    0.05 │   981092236486    980571017599    0.05 │ 1229632  1229996  -0.03 │
│                      coq-verdi-raft │  532.82   532.40    0.08 │  3715589182606   3713463475553    0.06 │  822568   830628  -0.97 │
│                         coq-coqutil │   42.04    42.00    0.10 │   264395161626    264198201368    0.07 │  681692   679424   0.33 │
│        coq-fiat-crypto-with-bedrock │ 5272.64  5263.86    0.17 │ 42756185125487  42735126349101    0.05 │ 3245484  3245524  -0.00 │
│                 coq-category-theory │  612.11   610.71    0.23 │  4547269133461   4531510158951    0.35 │  982504   983308  -0.08 │
│                   coq-metacoq-pcuic │  689.23   687.59    0.24 │  4500597644567   4493354574677    0.16 │ 3023924  2963848   2.03 │
│                             coq-vst │  856.79   854.64    0.25 │  6454103927081   6451604288675    0.04 │ 1670044  1686824  -0.99 │
│             coq-metacoq-safechecker │  357.04   355.93    0.31 │  2704889680353   2706916488112   -0.07 │ 1880316  1884324  -0.21 │
│                   coq-metacoq-utils │   22.44    22.36    0.36 │   147802784250    147541387752    0.18 │  582812   583552  -0.13 │
│                       coq-fiat-core │   55.28    55.06    0.40 │   335277567151    334910529400    0.11 │  470636   469568   0.23 │
│                          coq-stdlib │  349.16   347.13    0.58 │  1211878544222   1211032327532    0.07 │  641680   640348   0.21 │
│               coq-mathcomp-fingroup │   26.14    25.97    0.65 │   171920258169    172842808336   -0.53 │  566396   562276   0.73 │
│                           coq-verdi │   44.23    43.89    0.77 │   295099698361    294621171347    0.16 │  526468   520572   1.13 │
│                    coq-fiat-parsers │  275.28   273.07    0.81 │  2127610473729   2127052320493    0.03 │ 2288972  2290104  -0.05 │
│                  coq-metacoq-common │   65.89    65.26    0.97 │   428603066947    428243840959    0.08 │ 1228060  1228380  -0.03 │
│ coq-neural-net-interp-computed-lite │  234.92   232.48    1.05 │  2253470067051   2253200986106    0.01 │  846080   847384  -0.15 │
│               coq-mathcomp-solvable │   95.23    94.23    1.06 │   672666146553    654105986926    2.84 │  879408   877048   0.27 │
│               coq-engine-bench-lite │  130.58   129.12    1.13 │   971452409059    967934679775    0.36 │ 1058672  1059056  -0.04 │
│                       coq-equations │    7.12     7.02    1.42 │    47725746624     47670990230    0.11 │  384604   385920  -0.34 │
│                        coq-coqprime │   51.70    50.92    1.53 │   354921498383    354810409244    0.03 │  783148   781192   0.25 │
│                            coq-corn │  678.23   664.91    2.00 │  4724824917108   4630759298817    2.03 │  750888   723772   3.75 │
│                   coq-iris-examples │  524.52   389.09   34.81 │  3663492067555   2614036103434   40.15 │ 1075552  1147496  -6.27 │
│                       coq-fourcolor │ 1996.50  1351.68   47.71 │ 16544608430012  12512926816404   32.22 │  818408   828496  -1.22 │
└─────────────────────────────────────┴──────────────────────────┴────────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-hott
coq-performance-tests-lite
coq-mathcomp-character
coq-mathcomp-analysis (dependency install failed in NEW)
coq-unimath

coq-mathcomp-odd-order (dependency coq-mathcomp-character failed)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                    TOP 25 SLOW DOWNS                                                                    │
│                                                                                                                                                         │
│   OLD       NEW       DIFF      %DIFF      Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   0.4110  534.9490  534.5380  130057.91%   193  coq-fourcolor/theories/hypermap.v.html                                                                  │
│   0.6130   70.7650   70.1520   11444.05%   670  coq-fourcolor/theories/matte.v.html                                                                     │
│   8.0820   52.1460   44.0640     545.21%   581  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html                               │
│   8.0880   52.1000   44.0120     544.16%   591  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html                               │
│   7.9890   51.7230   43.7340     547.43%   580  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html                               │
│   0.4160   42.2550   41.8390   10057.45%   621  coq-fourcolor/theories/matte.v.html                                                                     │
│   0.2430    3.7030    3.4600    1423.87%  1156  coq-fourcolor/theories/cfmap.v.html                                                                     │
│  62.3500   65.1640    2.8140       4.51%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│ 198.3720  200.5560    2.1840       1.10%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│ 181.0750  182.6620    1.5870       0.88%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│ 120.1750  121.2370    1.0620       0.88%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  94.1270   95.0840    0.9570       1.02%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│   3.0240    3.9220    0.8980      29.70%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                                   │
│   3.0920    3.9450    0.8530      27.59%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  36.9020   37.7500    0.8480       2.30%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                        │
│  23.9940   24.8180    0.8240       3.43%   129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                                   │
│   0.4760    1.2870    0.8110     170.38%   330  coq-metacoq-erasure/erasure/theories/Typed/ExtractionCorrectness.v.html                                 │
│   0.0110    0.8140    0.8030    7300.00%   165  coq-fourcolor/theories/revsnip.v.html                                                                   │
│  36.5750   37.3540    0.7790       2.13%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│  35.5480   36.1710    0.6230       1.75%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│  37.2650   37.8230    0.5580       1.50%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                     │
│  18.3720   18.8810    0.5090       2.77%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                               │
│   6.3770    6.8650    0.4880       7.65%   192  coq-vst/veric/binop_lemmas5.v.html                                                                      │
│   1.6460    2.0690    0.4230      25.70%    42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│   1.0130    1.4200    0.4070      40.18%  1142  coq-stdlib/FSets/FMapAVL.v.html                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SPEED UPS                                                           │
│                                                                                                                                      │
│   OLD      NEW      DIFF     %DIFF    Ln                    FILE                                                                     │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 11.2360   0.2140  -11.0220  -98.10%  2103  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                    │
│  4.8790   0.4880   -4.3910  -90.00%  2089  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                    │
│ 63.6750  62.4490   -1.2260   -1.93%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                               │
│  1.1970   0.0010   -1.1960  -99.92%  3118  coq-mathcomp-algebra/mathcomp/algebra/poly.v.html                                         │
│  4.9420   3.8210   -1.1210  -22.68%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                    │
│  1.0040   0.0070   -0.9970  -99.30%   202  coq-mathcomp-field/mathcomp/field/separable.v.html                                        │
│ 25.6430  24.7880   -0.8550   -3.33%   345  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                        │
│  0.8560   0.0080   -0.8480  -99.07%  1595  coq-mathcomp-solvable/mathcomp/solvable/maximal.v.html                                    │
│  5.0150   4.2040   -0.8110  -16.17%  1827  coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                       │
│  3.2780   2.5500   -0.7280  -22.21%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                    │
│ 25.4450  24.8220   -0.6230   -2.45%    12  coq-fourcolor/theories/job279to282.v.html                                                 │
│ 25.4840  24.8890   -0.5950   -2.33%    12  coq-fourcolor/theories/job299to302.v.html                                                 │
│ 62.1100  61.5380   -0.5720   -0.92%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                  │
│  2.5080   1.9570   -0.5510  -21.97%    32  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                               │
│  0.5310   0.0060   -0.5250  -98.87%   177  coq-mathcomp-solvable/mathcomp/solvable/alt.v.html                                        │
│ 12.4480  11.9460   -0.5020   -4.03%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                  │
│ 19.9150  19.4660   -0.4490   -2.25%    12  coq-fourcolor/theories/job507to510.v.html                                                 │
│ 39.1870  38.7410   -0.4460   -1.14%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                │
│  0.4400   0.0030   -0.4370  -99.32%   363  coq-mathcomp-solvable/mathcomp/solvable/cyclic.v.html                                     │
│  2.0160   1.5830   -0.4330  -21.48%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                               │
│ 39.1230  38.6930   -0.4300   -1.10%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │
│  0.4680   0.0410   -0.4270  -91.24%   464  coq-mathcomp-field/mathcomp/field/separable.v.html                                        │
│  0.4050   0.0040   -0.4010  -99.01%   170  coq-mathcomp-solvable/mathcomp/solvable/alt.v.html                                        │
│  0.3760   0.0030   -0.3730  -99.20%  1556  coq-mathcomp-solvable/mathcomp/solvable/abelian.v.html                                    │
│  0.3710   0.0020   -0.3690  -99.46%   187  coq-mathcomp-solvable/mathcomp/solvable/jordanholder.v.html                               │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

coqbot-app · 2024-09-28T02:31:16Z

🔴 CI failures at commit d1e2548 without any failure in the test-suite

✔️ Corresponding jobs for the base commit 241e2fa succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-hott, ci-unimath

You can also pass me a specific list of targets to minimize as arguments.

SkySkimmer · 2024-09-28T05:59:22Z

performance-tests-lite timedout in the bench, in Reify/CanonicalStructures/_2_SuperFast.v AFAICT (the bench runs each package with a 3h timeout)
mathcomp-character failed producing a 3.7GiB log full of Debug [unification] messages, the end of the log says

- File "./inertia.v", line 933, characters 2-6:
- Error: The reference STOP was not found in the current environment.
- 
- Command exited with non-zero status 1
- inertia.vo (real: 3995.19, user: 3961.49, sys: 33.47, mem: 1484984 ko)

it seems the only files tried where

- mxrepresentation.vo (real: 17.75, user: 17.56, sys: 0.19, mem: 922884 ko)
- classfun.vo (real: 12.10, user: 11.92, sys: 0.17, mem: 949400 ko)
- character.vo (real: 14.61, user: 14.44, sys: 0.16, mem: 916728 ko)
- inertia.vo (real: 3995.19, user: 3961.49, sys: 33.47, mem: 1484984 ko)

Tragicus · 2024-09-28T09:40:04Z

Oh, sorry, fixed, and thank you. There is no need to restart the bench, there are several issues to investigate already.

Tragicus · 2024-10-15T07:37:17Z

This should be ready for the CI, and if everything goes well a bench.

ppedrot · 2024-10-15T08:34:31Z

@coqbot run full ci

Tragicus · 2024-10-15T09:42:52Z

It looks like my overlay is wrong. What name should I give instead of odd-order?

ppedrot · 2024-10-15T09:50:27Z

Did you use the script to generate the overlays or did you copy-paste this from other files? Otherwise the projects are oddorder and hott respectively.

Tragicus · 2024-10-15T10:07:53Z

I did not know about the script, which actually appears at least twice in the documentation, so thank you.

gares · 2024-10-16T11:51:00Z

@coqbot bench

coqbot-app · 2024-10-16T17:02:08Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                       coq-fiat-core │   55.49    56.18  -1.23 │   336470944098    336408576927   0.02 │  468236   468456  -0.05 │
│                         coq-coqutil │   41.54    41.84  -0.72 │   263581420058    263544639916   0.01 │  555004   554620   0.07 │
│                    coq-math-classes │   83.86    84.04  -0.21 │   516216257731    516253848517  -0.01 │  504560   505056  -0.10 │
│               coq-engine-bench-lite │  127.93   128.20  -0.21 │   965498238639    965692417118  -0.02 │ 1058400  1058564  -0.02 │
│                            coq-corn │  673.40   674.74  -0.20 │  4662357327308   4656448720325   0.13 │  691104   738600  -6.43 │
│                    coq-fiat-parsers │  273.79   274.25  -0.17 │  2129620274030   2129243214611   0.02 │ 2273188  2276860  -0.16 │
│                          coq-stdlib │  347.80   348.18  -0.11 │  1214703125301   1214564500899   0.01 │  625036   624444   0.09 │
│ coq-neural-net-interp-computed-lite │  233.77   233.95  -0.08 │  2251728299380   2251675158522   0.00 │  852620   851792   0.10 │
│                            coq-core │  133.34   133.42  -0.06 │   540339460167    539727016820   0.11 │  479180   480336  -0.24 │
│                             coq-vst │  855.65   855.56   0.01 │  6465110946260   6464865820756   0.00 │ 1687360  1680276   0.42 │
│                        coq-compcert │  301.01   300.97   0.01 │  1990019888399   1990565348138  -0.03 │ 1091544  1089884   0.15 │
│          coq-performance-tests-lite │  905.47   904.96   0.06 │  7310034933726   7303419246523   0.09 │ 2439296  2439140   0.01 │
│                           coq-verdi │   43.94    43.85   0.21 │   295723523267    295652893961   0.02 │  523464   524284  -0.16 │
│                           coq-color │  242.77   242.09   0.28 │  1536791883831   1537160565668  -0.02 │ 1136596  1136940  -0.03 │
│                         coq-bignums │   29.76    29.66   0.34 │   189873776339    189875375233  -0.00 │  468228   469012  -0.17 │
│                   coq-iris-examples │  395.87   394.33   0.39 │  2653758511765   2650846764347   0.11 │ 1083968  1071904   1.13 │
│                      coq-verdi-raft │  537.91   534.66   0.61 │  3746880976043   3746610588691   0.01 │  830988   830972   0.00 │
│                        coq-bedrock2 │  326.10   324.05   0.63 │  2766383093518   2766375143020   0.00 │  862696   862732  -0.00 │
│                        coq-coqprime │   51.97    51.55   0.81 │   357264460808    357282524467  -0.01 │  781044   781188  -0.02 │
│                         coq-unimath │ 1474.45  1460.32   0.97 │ 12186602565391  12106387491320   0.66 │ 1107280  1112588  -0.48 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-hott
coq-mathcomp-ssreflect (dependency install failed in NEW)
coq-equations
coq-rewriter

coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-algebra (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-solvable (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-field (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-character (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-odd-order (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-analysis (dependency coq-mathcomp-ssreflect failed)
coq-metacoq-utils (dependency coq-equations failed)
coq-metacoq-common (dependency coq-equations failed)
coq-metacoq-template (dependency coq-equations failed)
coq-metacoq-pcuic (dependency coq-equations failed)
coq-metacoq-safechecker (dependency coq-equations failed)
coq-metacoq-erasure (dependency coq-equations failed)
coq-metacoq-translations (dependency coq-equations failed)
coq-fiat-crypto-with-bedrock (dependency coq-rewriter failed)
coq-coquelicot (dependency coq-mathcomp-ssreflect failed)
coq-fourcolor (dependency coq-mathcomp-ssreflect failed)
coq-rewriter-perf-SuperFast (dependency coq-rewriter failed)
coq-category-theory (dependency coq-equations failed)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                      TOP 25 SLOW DOWNS                                                      │
│                                                                                                                             │
│   OLD      NEW      DIFF     %DIFF     Ln                  FILE                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  0.0030    1.3140  1.3110  43700.00%   238  coq-unimath/UniMath/CategoryTheory/Limits/Filtered.v.html                       │
│ 62.2290   63.0790  0.8500      1.37%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                     │
│ 46.5520   47.2550  0.7030      1.51%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html     │
│ 36.1370   36.8060  0.6690      1.85%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                    │
│  0.0850    0.7340  0.6490    763.53%   556  coq-unimath/UniMath/AlgebraicTheories/RepresentationTheorem.v.html              │
│  0.0010    0.6100  0.6090  60900.00%   110  coq-unimath/UniMath/CategoryTheory/Limits/StandardDiagrams.v.html               │
│  0.0010    0.6090  0.6080  60800.00%   107  coq-unimath/UniMath/CategoryTheory/Limits/StandardDiagrams.v.html               │
│ 99.4830  100.0170  0.5340      0.54%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 25.0900   25.5490  0.4590      1.83%   374  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html     │
│ 99.5570  100.0110  0.4540      0.46%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 25.0300   25.4820  0.4520      1.81%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html     │
│ 32.9050   33.3340  0.4290      1.30%   147  coq-vst/veric/expr_lemmas4.v.html                                               │
│ 46.2480   46.6700  0.4220      0.91%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                      │
│  0.1950    0.5940  0.3990    204.62%   934  coq-unimath/UniMath/AlgebraicTheories/CategoryOfRetracts.v.html                 │
│ 11.1820   11.5470  0.3650      3.26%   410  coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html            │
│ 31.9390   32.2650  0.3260      1.02%   194  coq-vst/veric/expr_lemmas4.v.html                                               │
│  0.2910    0.6070  0.3160    108.59%   199  coq-unimath/UniMath/CategoryTheory/Categories/StandardCategories.v.html         │
│ 16.8740   17.1840  0.3100      1.84%    32  coq-performance-tests-lite/src/pattern.v.html                                   │
│  4.5180    4.8230  0.3050      6.75%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html   │
│ 20.0080   20.2940  0.2860      1.43%   338  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html     │
│ 18.5320   18.8110  0.2790      1.51%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html               │
│  0.1450    0.4120  0.2670    184.14%   290  coq-unimath/UniMath/AlgebraicTheories/Examples/EndomorphismTheory.v.html        │
│ 14.9250   15.1830  0.2580      1.73%  1505  coq-vst/floyd/VSU.v.html                                                        │
│ 17.3450   17.5890  0.2440      1.41%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                       │
│  0.3810    0.6240  0.2430     63.78%   870  coq-stdlib/MSets/MSetRBT.v.html                                                 │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SPEED UPS                                                              │
│                                                                                                                                           │
│   OLD       NEW      DIFF     %DIFF    Ln                    FILE                                                                         │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  43.0820   42.1710  -0.9110    -2.11%  834  coq-vst/veric/binop_lemmas4.v.html                                                            │
│   0.7080    0.3180  -0.3900   -55.08%  868  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   0.9120    0.6900  -0.2220   -24.34%  205  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                      │
│   1.9950    1.7760  -0.2190   -10.98%   25  coq-engine-bench-lite/coq/PerformanceDemos/app_n.v.html                                       │
│   5.3150    5.1080  -0.2070    -3.89%  198  coq-compcert/x86/Op.v.html                                                                    │
│   1.6970    1.5010  -0.1960   -11.55%  313  coq-stdlib/Strings/Byte.v.html                                                                │
│ 199.9390  199.7440  -0.1950    -0.10%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│   0.8300    0.6700  -0.1600   -19.28%  813  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   7.9220    7.7640  -0.1580    -1.99%   31  coq-performance-tests-lite/src/pattern.v.html                                                 │
│   0.4060    0.2710  -0.1350   -33.25%  650  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   0.4240    0.2910  -0.1330   -31.37%  637  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   4.3540    4.2230  -0.1310    -3.01%  428  coq-compcert/lib/Heaps.v.html                                                                 │
│   0.3500    0.2190  -0.1310   -37.43%  445  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html                                           │
│   4.3420    4.2180  -0.1240    -2.86%  623  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│   1.2250    1.1020  -0.1230   -10.04%   21  coq-engine-bench-lite/coq/PerformanceDemos/app_n.v.html                                       │
│   0.2950    0.1770  -0.1180   -40.00%   16  coq-stdlib/Numbers/HexadecimalZ.v.html                                                        │
│   3.5620    3.4440  -0.1180    -3.31%  490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                    │
│   1.3810    1.2670  -0.1140    -8.25%  839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                 │
│   0.4380    0.3260  -0.1120   -25.57%  624  coq-stdlib/MSets/MSetRBT.v.html                                                               │
│   0.1080    0.0000  -0.1080  -100.00%  301  coq-vst/concurrency/conclib.v.html                                                            │
│   0.1190    0.0120  -0.1070   -89.92%   72  coq-unimath/UniMath/CategoryTheory/Categories/HSET/SliceFamEquiv.v.html                       │
│   0.1750    0.0700  -0.1050   -60.00%  230  coq-iris-examples/theories/logatom/snapshot/atomic_snapshot.v.html                            │
│   0.1590    0.0560  -0.1030   -64.78%  616  coq-vst/floyd/go_lower.v.html                                                                 │
│   0.6940    0.5920  -0.1020   -14.70%  820  coq-unimath/UniMath/CategoryTheory/Limits/Examples/IsoCommaLimits.v.html                      │
│   0.1010    0.0000  -0.1010  -100.00%   61  coq-iris-examples/theories/spanning_tree/proof.v.html                                         │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

gares · 2024-10-17T13:50:53Z

@coqbot run full ci

Tragicus · 2024-10-29T10:22:10Z

I mean that losing 10 hours of compilation is a bit sad, so I hope there is a way to restart the bench at coq-mathcomp-classical where it stopped.

SkySkimmer · 2024-10-29T10:32:24Z

I started a bench with just the failing jobs as targets, that's the best we can do.

coqbot-app · 2024-10-29T11:12:33Z

🏁 Bench results:

┌────────────────────────┬────────────────────────┬──────────────────────────────────────┬─────────────────────────┐
│                        │     user time [s]      │           CPU instructions           │  max resident mem [KB]  │
│                        │                        │                                      │                         │
│      package_name      │  NEW     OLD    PDIFF  │      NEW            OLD       PDIFF  │   NEW      OLD    PDIFF │
├────────────────────────┼────────────────────────┼──────────────────────────────────────┼─────────────────────────┤
│ coq-mathcomp-classical │  56.19   67.15  -16.32 │  380386314956   459312881201  -17.18 │ 1444300  1476316  -2.17 │
│               coq-core │ 130.65  131.00   -0.27 │  540915566449   540764953397    0.03 │  481732   480740   0.21 │
│             coq-stdlib │ 351.43  349.54    0.54 │ 1209941892996  1209865585682    0.01 │  625576   621244   0.70 │
└────────────────────────┴────────────────────────┴──────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-mathcomp-analysis

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                       TOP 25 SLOW DOWNS                                        │
│                                                                                                │
│  OLD     NEW     DIFF    %DIFF     Ln             FILE                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 0.5970  0.8280  0.2310    38.69%  2108  coq-stdlib/FSets/FMapFacts.v.html                      │
│ 0.1020  0.2610  0.1590   155.88%   853  coq-stdlib/MSets/MSetRBT.v.html                        │
│ 0.0020  0.1530  0.1510  7550.00%   130  coq-mathcomp-classical/classical/fsbigop.v.html        │
│ 1.5590  1.6930  0.1340     8.60%   313  coq-stdlib/Strings/Byte.v.html                         │
│ 0.6870  0.8180  0.1310    19.07%   813  coq-stdlib/MSets/MSetRBT.v.html                        │
│ 0.3130  0.4360  0.1230    39.30%    14  coq-stdlib/MSets/MSetToFiniteSet.v.html                │
│ 0.2250  0.3450  0.1200    53.33%    12  coq-stdlib/MSets/MSets.v.html                          │
│ 0.3200  0.4390  0.1190    37.19%   624  coq-stdlib/MSets/MSetRBT.v.html                        │
│ 0.2300  0.3490  0.1190    51.74%    11  coq-stdlib/Floats/FloatOps.v.html                      │
│ 0.1580  0.2730  0.1150    72.78%    31  coq-stdlib/FSets/FMapFullAVL.v.html                    │
│ 0.1450  0.2590  0.1140    78.62%   262  coq-stdlib/FSets/FSetProperties.v.html                 │
│ 0.3170  0.4290  0.1120    35.33%   637  coq-stdlib/MSets/MSetRBT.v.html                        │
│ 0.1940  0.3060  0.1120    57.73%    19  coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html       │
│ 0.2260  0.3370  0.1110    49.12%   443  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html    │
│ 0.4460  0.5530  0.1070    23.99%   870  coq-stdlib/MSets/MSetRBT.v.html                        │
│ 0.4640  0.5650  0.1010    21.77%    82  coq-stdlib/Numbers/Cyclic/Int63/Sint63.v.html          │
│ 0.1600  0.2550  0.0950    59.38%   445  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html    │
│ 0.1870  0.2810  0.0940    50.27%     1  coq-stdlib/Reals/Cauchy/QExtra.v.html                  │
│ 0.1950  0.2890  0.0940    48.21%  1603  coq-stdlib/micromega/Tauto.v.html                      │
│ 0.1700  0.2630  0.0930    54.71%   444  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html    │
│ 0.1860  0.2780  0.0920    49.46%    16  coq-stdlib/Numbers/HexadecimalN.v.html                 │
│ 0.1790  0.2700  0.0910    50.84%    13  coq-stdlib/extraction/ExtrOCamlPArray.v.html           │
│ 0.1650  0.2530  0.0880    53.33%    12  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │
│ 0.1720  0.2570  0.0850    49.42%    16  coq-stdlib/Numbers/DecimalNat.v.html                   │
│ 0.1770  0.2610  0.0840    47.46%    14  coq-stdlib/Numbers/Cyclic/Int63/Ring63.v.html          │
└────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                          TOP 25 SPEED UPS                                           │
│                                                                                                     │
│  OLD     NEW     DIFF     %DIFF     Ln             FILE                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 1.3140  1.0240  -0.2900   -22.07%  1142  coq-stdlib/FSets/FMapAVL.v.html                            │
│ 0.9860  0.7120  -0.2740   -27.79%   205  coq-stdlib/setoid_ring/Ncring_tac.v.html                   │
│ 0.3270  0.1420  -0.1850   -56.57%    11  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html        │
│ 0.3160  0.1400  -0.1760   -55.70%   226  coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html        │
│ 2.4230  2.2550  -0.1680    -6.93%   203  coq-stdlib/setoid_ring/Ncring_tac.v.html                   │
│ 1.1600  0.9970  -0.1630   -14.05%   408  coq-stdlib/MSets/MSetAVL.v.html                            │
│ 0.1730  0.0220  -0.1510   -87.28%   121  coq-mathcomp-classical/classical/fsbigop.v.html            │
│ 0.9750  0.8330  -0.1420   -14.56%   572  coq-stdlib/MSets/MSetAVL.v.html                            │
│ 3.5690  3.4340  -0.1350    -3.78%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │
│ 0.2240  0.1040  -0.1200   -53.57%   268  coq-mathcomp-classical/classical/fsbigop.v.html            │
│ 0.2830  0.1660  -0.1170   -41.34%    11  coq-stdlib/Reals/Abstract/ConstructivePower.v.html         │
│ 0.4310  0.3150  -0.1160   -26.91%   140  coq-stdlib/Strings/Ascii.v.html                            │
│ 0.6010  0.4900  -0.1110   -18.47%   816  coq-stdlib/MSets/MSetRBT.v.html                            │
│ 0.1890  0.0830  -0.1060   -56.08%   225  coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html        │
│ 0.3000  0.1950  -0.1050   -35.00%   637  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html           │
│ 0.2490  0.1580  -0.0910   -36.55%   731  coq-stdlib/MSets/MSetRBT.v.html                            │
│ 0.2490  0.1640  -0.0850   -34.14%  1121  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html         │
│ 0.7340  0.6500  -0.0840   -11.44%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                   │
│ 0.2120  0.1320  -0.0800   -37.74%   637  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html           │
│ 0.6350  0.5580  -0.0770   -12.13%   868  coq-stdlib/MSets/MSetRBT.v.html                            │
│ 0.2640  0.1910  -0.0730   -27.65%  1630  coq-stdlib/Numbers/Cyclic/Int63/Uint63.v.html              │
│ 0.0720  0.0000  -0.0720  -100.00%   598  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html           │
│ 0.0690  0.0000  -0.0690  -100.00%   591  coq-stdlib/micromega/ZifyInst.v.html                       │
│ 0.3230  0.2560  -0.0670   -20.74%   719  coq-stdlib/MSets/MSetRBT.v.html                            │
│ 0.0870  0.0200  -0.0670   -77.01%   139  coq-mathcomp-classical/classical/fsbigop.v.html            │
└─────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

SkySkimmer · 2024-10-29T11:37:06Z

mathcomp analysis failed in OLD

- File "./topology_theory/pseudometric_structure.v", line 5, characters 29-35:
- Error: Cannot find a physical path bound to logical path
- signed with prefix mathcomp.

Tragicus · 2024-10-29T12:44:23Z

It looks like they changed the layout of analysis, there are new directories reals, reals_stdlib and analysis_stdlib that need to be compiled first. I rebased the overlay (so it should fail now too). Can we remove the -C theories from the make command?

SkySkimmer · 2024-10-29T12:51:47Z

I guess you mean the command in the analysis opam file. You can make a PR on the opam repo.

Tragicus · 2024-10-29T13:03:18Z

Done (in my branch), I hope recompiling classical will not be an issue, I could not find a way to compile all the directories except classical.

proux01 · 2024-10-29T13:11:37Z

Damn, I forgot the extra-dev opam repo, let me fix that.

Tragicus · 2024-10-29T13:19:16Z

Then I revert the changes ^^

proux01 · 2024-10-29T13:30:37Z

PR opened coq/opam#3192

proux01 · 2024-10-30T06:54:48Z

PR merged

proux01 · 2024-10-30T09:16:54Z

@coqbot bench

coqbot-app · 2024-10-30T09:45:22Z

🏁 Bench results:

┌────────────────────────┬───────────────────────┬─────────────────────────────────────┬─────────────────────────┐
│                        │     user time [s]     │          CPU instructions           │  max resident mem [KB]  │
│                        │                       │                                     │                         │
│      package_name      │  NEW     OLD    PDIFF │      NEW            OLD       PDIFF │   NEW      OLD    PDIFF │
├────────────────────────┼───────────────────────┼─────────────────────────────────────┼─────────────────────────┤
│ coq-mathcomp-classical │  67.10   67.47  -0.55 │  457434099443   459071276486  -0.36 │ 1456524  1474824  -1.24 │
│               coq-core │ 133.99  132.99   0.75 │  541199973162   540656996143   0.10 │  480084   480644  -0.12 │
│             coq-stdlib │ 351.16  347.21   1.14 │ 1210109835693  1209805380624   0.03 │  626936   621544   0.87 │
└────────────────────────┴───────────────────────┴─────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-mathcomp-analysis

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                          TOP 25 SLOW DOWNS                                          │
│                                                                                                     │
│  OLD     NEW     DIFF     %DIFF     Ln             FILE                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 1.0230  1.4070  0.3840     37.54%  1142  coq-stdlib/FSets/FMapAVL.v.html                            │
│ 0.8360  1.1500  0.3140     37.56%   572  coq-stdlib/MSets/MSetAVL.v.html                            │
│ 3.1880  3.4360  0.2480      7.78%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │
│ 0.3810  0.6220  0.2410     63.25%    14  coq-stdlib/MSets/MSetToFiniteSet.v.html                    │
│ 0.1810  0.3810  0.2000    110.50%   637  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html           │
│ 0.1760  0.3720  0.1960    111.36%   219  coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html        │
│ 0.7030  0.8890  0.1860     26.46%   205  coq-stdlib/setoid_ring/Ncring_tac.v.html                   │
│ 0.5250  0.6850  0.1600     30.48%   816  coq-stdlib/MSets/MSetRBT.v.html                            │
│ 0.6210  0.7720  0.1510     24.32%   160  coq-stdlib/Numbers/HexadecimalNat.v.html                   │
│ 0.0000  0.1490  0.1490       inf%   172  coq-mathcomp-classical/classical/set_interval.v.html       │
│ 0.0060  0.1500  0.1440   2400.00%   412  coq-mathcomp-classical/classical/cardinality.v.html        │
│ 0.0110  0.1540  0.1430   1300.00%   122  coq-mathcomp-classical/classical/fsbigop.v.html            │
│ 0.0010  0.1380  0.1370  13700.00%   171  coq-mathcomp-classical/classical/classical_orders.v.html   │
│ 0.9320  1.0680  0.1360     14.59%   408  coq-stdlib/MSets/MSetAVL.v.html                            │
│ 0.4180  0.5500  0.1320     31.58%   705  coq-stdlib/Numbers/HexadecimalFacts.v.html                 │
│ 0.2010  0.3290  0.1280     63.68%    16  coq-stdlib/Numbers/HexadecimalZ.v.html                     │
│ 0.3850  0.5070  0.1220     31.69%  1149  coq-stdlib/FSets/FMapAVL.v.html                            │
│ 0.1260  0.2480  0.1220     96.83%   637  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html           │
│ 0.0000  0.1210  0.1210       inf%   341  coq-mathcomp-classical/classical/classical_sets.v.html     │
│ 0.0000  0.1170  0.1170       inf%   308  coq-mathcomp-classical/classical/boolp.v.html              │
│ 0.3730  0.4880  0.1150     30.83%   474  coq-stdlib/MSets/MSetWeakList.v.html                       │
│ 0.0310  0.1450  0.1140    367.74%   354  coq-mathcomp-classical/classical/classical_orders.v.html   │
│ 0.1860  0.2940  0.1080     58.06%     1  coq-stdlib/Array/PArray.v.html                             │
│ 0.0090  0.1150  0.1060   1177.78%   153  coq-mathcomp-classical/classical/wochoice.v.html           │
│ 0.1260  0.2310  0.1050     83.33%   351  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │
└─────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                         TOP 25 SPEED UPS                                          │
│                                                                                                   │
│  OLD     NEW     DIFF     %DIFF     Ln             FILE                                           │
├───────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 0.6260  0.3040  -0.3220   -51.44%   870  coq-stdlib/MSets/MSetRBT.v.html                          │
│ 0.9420  0.6220  -0.3200   -33.97%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html   │
│ 0.3110  0.0080  -0.3030   -97.43%   405  coq-mathcomp-classical/classical/cardinality.v.html      │
│ 0.5200  0.3120  -0.2080   -40.00%   868  coq-stdlib/MSets/MSetRBT.v.html                          │
│ 1.7240  1.5220  -0.2020   -11.72%   313  coq-stdlib/Strings/Byte.v.html                           │
│ 0.1840  0.0220  -0.1620   -88.04%   121  coq-mathcomp-classical/classical/fsbigop.v.html          │
│ 0.1470  0.0000  -0.1470  -100.00%   178  coq-mathcomp-classical/classical/set_interval.v.html     │
│ 0.1430  0.0050  -0.1380   -96.50%   173  coq-mathcomp-classical/classical/classical_orders.v.html │
│ 0.2980  0.1610  -0.1370   -45.97%    11  coq-stdlib/Reals/Abstract/ConstructivePower.v.html       │
│ 0.3380  0.2030  -0.1350   -39.94%    11  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html      │
│ 0.4070  0.2730  -0.1340   -32.92%   650  coq-stdlib/MSets/MSetRBT.v.html                          │
│ 0.4150  0.2920  -0.1230   -29.64%  1165  coq-stdlib/FSets/FMapAVL.v.html                          │
│ 0.4330  0.3120  -0.1210   -27.94%   624  coq-stdlib/MSets/MSetRBT.v.html                          │
│ 0.1170  0.0000  -0.1170  -100.00%   344  coq-mathcomp-classical/classical/classical_sets.v.html   │
│ 0.1160  0.0000  -0.1160  -100.00%   309  coq-mathcomp-classical/classical/boolp.v.html            │
│ 0.1230  0.0100  -0.1130   -91.87%   152  coq-mathcomp-classical/classical/wochoice.v.html         │
│ 0.6910  0.5810  -0.1100   -15.92%   813  coq-stdlib/MSets/MSetRBT.v.html                          │
│ 0.4130  0.3030  -0.1100   -26.63%   637  coq-stdlib/MSets/MSetRBT.v.html                          │
│ 0.1060  0.0030  -0.1030   -97.17%   264  coq-mathcomp-classical/classical/wochoice.v.html         │
│ 0.6720  0.5700  -0.1020   -15.18%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                 │
│ 0.2080  0.1060  -0.1020   -49.04%   268  coq-mathcomp-classical/classical/fsbigop.v.html          │
│ 0.3930  0.2970  -0.0960   -24.43%   163  coq-stdlib/Numbers/HexadecimalPos.v.html                 │
│ 0.2580  0.1620  -0.0960   -37.21%  1121  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html       │
│ 0.2420  0.1520  -0.0900   -37.19%  1151  coq-stdlib/FSets/FMapAVL.v.html                          │
│ 0.3820  0.2930  -0.0890   -23.30%   138  coq-stdlib/Numbers/HexadecimalPos.v.html                 │
└───────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

Tragicus · 2024-10-30T09:56:30Z

I rebased my branch of opam_coq_archive.

proux01 · 2024-10-30T10:58:43Z

So
@coqbot bench
(but would probably be easier to remove the change to bench.sh in current PR for future runs)

coqbot-app · 2024-10-30T11:48:43Z

🏁 Bench results:

┌────────────────────────┬───────────────────────┬─────────────────────────────────────┬─────────────────────────┐
│                        │     user time [s]     │          CPU instructions           │  max resident mem [KB]  │
│                        │                       │                                     │                         │
│      package_name      │  NEW     OLD    PDIFF │      NEW            OLD       PDIFF │   NEW      OLD    PDIFF │
├────────────────────────┼───────────────────────┼─────────────────────────────────────┼─────────────────────────┤
│  coq-mathcomp-analysis │ 557.45  563.42  -1.06 │ 4166403947945  4204357186634  -0.90 │ 1747144  1729676   1.01 │
│ coq-mathcomp-classical │  67.25   67.89  -0.94 │  457381604396   459103971261  -0.38 │ 1456232  1475084  -1.28 │
│             coq-stdlib │ 352.13  353.77  -0.46 │ 1209942259255  1209962556465  -0.00 │  627488   622124   0.86 │
│               coq-core │ 133.90  133.47   0.32 │  540971890200   540725063435   0.05 │  481044   480260   0.16 │
└────────────────────────┴───────────────────────┴─────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                   TOP 25 SLOW DOWNS                                                    │
│                                                                                                                        │
│   OLD      NEW     DIFF    %DIFF     Ln                 FILE                                                           │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  0.3510   0.7090  0.3580   101.99%   870  coq-stdlib/MSets/MSetRBT.v.html                                              │
│  0.8060   1.1240  0.3180    39.45%   572  coq-stdlib/MSets/MSetAVL.v.html                                              │
│  1.8160   2.0770  0.2610    14.37%   203  coq-stdlib/setoid_ring/Ncring_tac.v.html                                     │
│  0.5480   0.8010  0.2530    46.17%   813  coq-stdlib/MSets/MSetRBT.v.html                                              │
│  0.4040   0.6560  0.2520    62.38%   622  coq-mathcomp-analysis/theories/lebesgue_measure.v.html                       │
│  0.6890   0.9160  0.2270    32.95%   205  coq-stdlib/setoid_ring/Ncring_tac.v.html                                     │
│  0.4130   0.6300  0.2170    52.54%   581  coq-mathcomp-analysis/theories/probability.v.html                            │
│  0.6440   0.8530  0.2090    32.45%   160  coq-stdlib/Numbers/HexadecimalNat.v.html                                     │
│  0.1280   0.3360  0.2080   162.50%    11  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html                          │
│  0.1350   0.3400  0.2050   151.85%  1045  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html                           │
│  0.9050   1.1070  0.2020    22.32%   408  coq-stdlib/MSets/MSetAVL.v.html                                              │
│  0.0020   0.1910  0.1890  9450.00%    79  coq-mathcomp-analysis/theories/ftc.v.html                                    │
│  0.0000   0.1840  0.1840      inf%    84  coq-mathcomp-analysis/theories/probability.v.html                            │
│  0.0080   0.1880  0.1800  2250.00%   103  coq-mathcomp-analysis/theories/convex.v.html                                 │
│ 10.8390  11.0150  0.1760     1.62%  3439  coq-mathcomp-analysis/theories/lebesgue_integral.v.html                      │
│  0.1140   0.2880  0.1740   152.63%   347  coq-mathcomp-analysis/theories/ereal.v.html                                  │
│  0.2540   0.4250  0.1710    67.32%   207  coq-mathcomp-analysis/theories/realfun.v.html                                │
│  0.1820   0.3480  0.1660    91.21%    16  coq-stdlib/Numbers/HexadecimalZ.v.html                                       │
│  0.0020   0.1630  0.1610  8050.00%   165  coq-mathcomp-analysis/theories/cantor.v.html                                 │
│  0.6610   0.8190  0.1580    23.90%   197  coq-stdlib/setoid_ring/Ncring_tac.v.html                                     │
│  0.1060   0.2580  0.1520   143.40%   116  coq-mathcomp-analysis/theories/topology_theory/pseudometric_structure.v.html │
│  0.0090   0.1610  0.1520  1688.89%   322  coq-mathcomp-analysis/theories/forms.v.html                                  │
│  0.1570   0.3070  0.1500    95.54%   144  coq-mathcomp-analysis/theories/realfun.v.html                                │
│  0.3460   0.4950  0.1490    43.06%     7  coq-mathcomp-analysis/theories/cantor.v.html                                 │
│  0.0000   0.1490  0.1490      inf%   172  coq-mathcomp-classical/classical/set_interval.v.html                         │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                   TOP 25 SPEED UPS                                                    │
│                                                                                                                       │
│  OLD     NEW     DIFF     %DIFF     Ln                 FILE                                                           │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 2.3700  0.0310  -2.3390   -98.69%   871  coq-mathcomp-analysis/theories/derive.v.html                                 │
│ 3.7350  2.9040  -0.8310   -22.25%  1281  coq-mathcomp-analysis/theories/derive.v.html                                 │
│ 0.3730  0.0080  -0.3650   -97.86%  1159  coq-mathcomp-analysis/theories/probability.v.html                            │
│ 0.3110  0.0080  -0.3030   -97.43%   405  coq-mathcomp-classical/classical/cardinality.v.html                          │
│ 0.3450  0.0620  -0.2830   -82.03%  2023  coq-mathcomp-analysis/theories/lebesgue_measure.v.html                       │
│ 0.4580  0.2260  -0.2320   -50.66%   747  coq-stdlib/MSets/MSetRBT.v.html                                              │
│ 3.0670  2.8370  -0.2300    -7.50%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                   │
│ 0.7730  0.5740  -0.1990   -25.74%   422  coq-stdlib/MSets/MSetList.v.html                                             │
│ 0.1990  0.0020  -0.1970   -98.99%    77  coq-mathcomp-analysis/theories/ftc.v.html                                    │
│ 0.2000  0.0040  -0.1960   -98.00%   318  coq-mathcomp-analysis/theories/ereal.v.html                                  │
│ 0.1870  0.0110  -0.1760   -94.12%   102  coq-mathcomp-analysis/theories/convex.v.html                                 │
│ 0.1790  0.0040  -0.1750   -97.77%   149  coq-mathcomp-analysis/theories/derive.v.html                                 │
│ 0.2900  0.1160  -0.1740   -60.00%   211  coq-mathcomp-analysis/theories/topology_theory/order_topology.v.html         │
│ 0.3650  0.1940  -0.1710   -46.85%    17  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                   │
│ 0.6330  0.4700  -0.1630   -25.75%    82  coq-stdlib/Numbers/Cyclic/Int63/Sint63.v.html                                │
│ 0.2850  0.1220  -0.1630   -57.19%   207  coq-mathcomp-analysis/theories/topology_theory/order_topology.v.html         │
│ 0.1840  0.0230  -0.1610   -87.50%   121  coq-mathcomp-classical/classical/fsbigop.v.html                              │
│ 0.1540  0.0020  -0.1520   -98.70%   273  coq-mathcomp-analysis/theories/forms.v.html                                  │
│ 0.1560  0.0040  -0.1520   -97.44%   141  coq-mathcomp-analysis/theories/realfun.v.html                                │
│ 0.2480  0.0970  -0.1510   -60.89%   119  coq-mathcomp-analysis/theories/topology_theory/pseudometric_structure.v.html │
│ 0.1470  0.0000  -0.1470  -100.00%   178  coq-mathcomp-classical/classical/set_interval.v.html                         │
│ 0.5230  0.3810  -0.1420   -27.15%   597  coq-stdlib/Strings/Byte.v.html                                               │
│ 0.1440  0.0050  -0.1390   -96.53%   173  coq-mathcomp-classical/classical/classical_orders.v.html                     │
│ 0.4090  0.2830  -0.1260   -30.81%   650  coq-stdlib/MSets/MSetRBT.v.html                                              │
│ 0.4230  0.2980  -0.1250   -29.55%   313  coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html                             │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

Tragicus · 2024-10-30T13:38:47Z

I am not sure how the performance gain in classical disappeared, I just compiled it again in less than a minute. Also, is there nothing after analysis?

SkySkimmer · 2024-10-30T14:14:18Z

The change in classical in #19611 (comment) seems to have been because some files weren't there in NEW
https://coq.gitlabpages.inria.fr/-/coq/-/jobs/4903968/artifacts/_bench/logs/coq-mathcomp-classical.BOTH.perfile_timings.1.log

   After |   Peak Mem | File Name             |   Before |   Peak Mem ||    Change || Change (mem) | % Change | % Change (mem)
------------------------------------------------------------------------------------------------------------------------------
0m56.93s | 1444300 ko | Total Time / Peak Mem | 1m08.04s | 1476316 ko || -0m11.11s ||    -32016 ko |  -16.32% |         -2.16%
------------------------------------------------------------------------------------------------------------------------------
  N/A    |     N/A    | filter.vo             | 0m06.73s |  915048 ko || -0m06.73s ||   -915048 ko | -100.00% |       -100.00%
  N/A    |     N/A    | classical_orders.vo   | 0m03.47s |  744932 ko || -0m03.47s ||   -744932 ko | -100.00% |       -100.00%
0m23.43s | 1444300 ko | functions.vo          | 0m23.43s | 1476316 ko || +0m00.00s ||    -32016 ko |   +0.00% |         -2.16%
0m07.93s |  896804 ko | classical_sets.vo     | 0m07.89s |  903360 ko || +0m00.04s ||     -6556 ko |   +0.50% |         -0.72%
0m06.17s |  790024 ko | cardinality.vo        | 0m06.24s |  794500 ko || -0m00.07s ||     -4476 ko |   -1.12% |         -0.56%
0m04.25s |  730652 ko | set_interval.vo       | 0m04.49s |  735508 ko || -0m00.24s ||     -4856 ko |   -5.34% |         -0.66%
0m03.95s |  719044 ko | fsbigop.vo            | 0m04.22s |  719684 ko || -0m00.27s ||      -640 ko |   -6.39% |         -0.08%
0m02.78s |  644952 ko | wochoice.vo           | 0m02.81s |  641748 ko || -0m00.03s ||      3204 ko |   -1.06% |         +0.49%
0m02.51s |  681004 ko | mathcomp_extra.vo     | 0m02.61s |  680940 ko || -0m00.10s ||        64 ko |   -3.83% |         +0.00%
0m02.43s |  683556 ko | boolp.vo              | 0m02.62s |  681612 ko || -0m00.19s ||      1944 ko |   -7.25% |         +0.28%
0m02.01s |  697752 ko | all_classical.vo      | 0m02.09s |  717904 ko || -0m00.08s ||    -20152 ko |   -3.82% |         -2.80%
0m01.47s |  643996 ko | contra.vo             | 0m01.44s |  641768 ko || +0m00.03s ||      2228 ko |   +2.08% |         +0.34%

proux01 · 2024-10-30T15:09:22Z

@coqbot run full ci

coqbot-app · 2024-10-30T17:29:19Z

🔴 CI failure at commit cbdc29f without any failure in the test-suite

✔️ Corresponding job for the base commit e9d68d2 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-fcsl_pcm

You can also pass me a specific list of targets to minimize as arguments.

⚠️ ⌛ You may want to wait until the pipeline for the base commit (e9d68d2) finishes.

gares · 2024-10-30T21:25:58Z

engine/evarutil.ml

+    | Evar _ | Meta _ -> raise NotInstantiatedEvar
+    | _ -> EConstr.iter evd has_ev t in
+  try let _ = has_ev t in false
+  with (Not_found | NotInstantiatedEvar) -> true


The Not_found is fishy, it would mean the term has an unknown evar.

I think I copy-pasted the code from has_undefined_evars, which changed in the meantime, and it is out of the scope of this PR to fix this. Also, catching the unknown evars here is not a trivial design choice (although I agree that if we want the invariant that no evar may ever not be declared in the evar_map then we should probably explode as soon as possible). Should I mirror the code of has_undefined_evars again and open another PR to propose the change?

gares · 2024-10-30T21:35:26Z

pretyping/evarconv.ml

            | None -> UnifFailure (evd,NotSameHead))

        | _, _ ->
+        let no_cs1 = ref false in


I see why you use a ref to make f2 and f3 pass extra data, and I see no better way. But it deserves a comment.

gares · 2024-10-30T21:35:29Z

pretyping/evarconv.ml

@@ -695,6 +702,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
        end

 and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
+    parents1 parents2 keys1 keys2 lastUnfolded


IMO, it would make more sense to define a type cs_keys_cache = { .... } and pass a single argument here.
The type should come with an empty : unit -> .. constructor and a flip function to exchange left with right.
It would also help to document what the last argument (the last unfolded thing) is.

gares · 2024-10-30T21:41:51Z

pretyping/evarconv.ml

+               (let x = try get_cs env i keys2 (match lastUnfolded with | Some true -> true | _ -> false) parents2 appr1 c2 appr2
+                 with No_cs b -> no_cs1 := b; None in
+               let x = match x with
+               | Some _ -> x


I think you should name the try...with No_cs ... code, maybe get_cs_opt and move out the assignment to no_cs1. This way you should be able to call it twice and the control flow should become a bit more clear as in

match get_cs_opt bla bla 2 with | Some x -> x | None -> match get_cs_opt bla bla 1 with | Some x -> x | None -> raise Not_found

gares · 2024-10-30T21:42:29Z

pretyping/evarconv.ml

-             else conv_record flags env (check_conv_record env i appr1 appr2)
+             else conv_record flags env (
+               let x =
+                 try get_cs env i keys2 false parents2 appr1 c2 appr2


gares · 2024-10-30T21:42:35Z

pretyping/evarconv.ml

-             else conv_record flags env (check_conv_record env i appr2 appr1)
+             else conv_record flags env (
+               let x =
+                 try get_cs env i keys1 false parents1 appr2 c1 appr1


gares · 2024-10-30T21:43:30Z

pretyping/evarconv.mli


+exception No_cs of bool


The only user of this function/exception ignores the bool.
I don't get the point of exposing the decompose_proj API. Could you please explain the choice?

decompose_proj is used in pretyping/unification.ml.

Tragicus requested review from a team as code owners September 27, 2024 11:31

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 Sep 27, 2024

Tragicus marked this pull request as draft September 27, 2024 11:31

Tragicus mentioned this pull request Sep 27, 2024

Add semi-modules, semi-algebras, and semilinear functions math-comp/math-comp#1125

Open

3 tasks

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 27, 2024

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 1, 2024

Tragicus force-pushed the cs-save-key branch from d302f7f to 74dc919 Compare October 10, 2024 10:21

coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Oct 10, 2024

Tragicus force-pushed the cs-save-key branch from 74dc919 to add9a9c Compare October 10, 2024 11:55

Tragicus marked this pull request as ready for review October 11, 2024 11:54

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 Oct 15, 2024

Tragicus force-pushed the cs-save-key branch from eeeedcc to 976e95f Compare October 15, 2024 10:02

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 Oct 15, 2024

gares self-assigned this Oct 29, 2024

gares added this to the 9.0+rc1 milestone Oct 29, 2024

This was referenced Oct 30, 2024

adapt to coq#19611 math-comp/analysis#1377

Merged

annotate card_vspace1 math-comp/odd-order#60

Merged

Adapt to Coq#19611 HoTT/Coq-HoTT#2127

Open

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 Oct 30, 2024

gares reviewed Oct 30, 2024

View reviewed changes

Tragicus mentioned this pull request Oct 31, 2024

Adapt to coq#pr19611 imdea-software/fcsl-pcm#45

Open

review

c974f3b

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 Oct 31, 2024

Evarconv: save keys #19611

Are you sure you want to change the base?

Evarconv: save keys #19611

Conversation

Tragicus commented Sep 27, 2024 • edited Loading

Overlays (to be merged before the current PR)

SkySkimmer commented Sep 27, 2024

SkySkimmer commented Sep 27, 2024

pi8027 commented Sep 27, 2024

coqbot-app bot commented Sep 28, 2024

coqbot-app bot commented Sep 28, 2024

SkySkimmer commented Sep 28, 2024

Tragicus commented Sep 28, 2024

Tragicus commented Oct 15, 2024

ppedrot commented Oct 15, 2024

Tragicus commented Oct 15, 2024

ppedrot commented Oct 15, 2024

Tragicus commented Oct 15, 2024

gares commented Oct 16, 2024

coqbot-app bot commented Oct 16, 2024

gares commented Oct 17, 2024

Tragicus commented Oct 29, 2024

SkySkimmer commented Oct 29, 2024

coqbot-app bot commented Oct 29, 2024

SkySkimmer commented Oct 29, 2024

Tragicus commented Oct 29, 2024 • edited Loading

SkySkimmer commented Oct 29, 2024

Tragicus commented Oct 29, 2024 • edited Loading

proux01 commented Oct 29, 2024

Tragicus commented Oct 29, 2024

proux01 commented Oct 29, 2024

proux01 commented Oct 30, 2024

proux01 commented Oct 30, 2024

coqbot-app bot commented Oct 30, 2024

Tragicus commented Oct 30, 2024

proux01 commented Oct 30, 2024

coqbot-app bot commented Oct 30, 2024

Tragicus commented Oct 30, 2024

SkySkimmer commented Oct 30, 2024

proux01 commented Oct 30, 2024

coqbot-app bot commented Oct 30, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gares Oct 30, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Tragicus commented Sep 27, 2024 •

edited

Loading

Tragicus commented Oct 29, 2024 •

edited

Loading

Tragicus commented Oct 29, 2024 •

edited

Loading

gares Oct 30, 2024 •

edited

Loading