Support TIMED=1 in test suite + some preliminary cleanups

[SkySkimmer]

coqwc, coqdoc and tools tests don't use it due to low
expected value but would be trivial to add.

[SkySkimmer]

@coqbot run ci

[SkySkimmer]

@coqbot run full ci

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[coqbot-app]

🏁 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 │ 372.03  375.41  -0.90 │ 1566040725954  1577061390426  -0.70 │ 1347021548966  1347009293836   0.00 │  720828   717548   0.46 │
│ coq-equations │   6.20    6.23  -0.48 │   26231409146    26229932419   0.01 │   42465432271    42469177929  -0.01 │  387624   387272   0.09 │
│      coq-core │ 119.58  119.67  -0.08 │  464451363622   464088255321   0.08 │  499237087330   499065278745   0.03 │  370780   370732   0.01 │
│           coq │ 705.11  696.52   1.23 │ 3015487558333  2995587283279   0.66 │ 5638466237315  5620232983200   0.32 │ 1887376  1876580   0.58 │
└───────────────┴───────────────────────┴─────────────────────────────────────┴─────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                         TOP 25 SLOW DOWNS                                         │
│                                                                                                   │
│  OLD     NEW     DIFF    %DIFF    Ln             FILE                                             │
├───────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 1.7570  2.2720  0.5150   29.31%   209  coq-stdlib/setoid_ring/Ncring_tac.v.html                   │
│ 3.1210  3.3650  0.2440    7.82%   122  coq-stdlib/setoid_ring/Ncring_initial.v.html               │
│ 0.2220  0.3780  0.1560   70.27%    17  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │
│ 0.8100  0.9580  0.1480   18.27%   170  coq-stdlib/Numbers/HexadecimalNat.v.html                   │
│ 0.5940  0.7310  0.1370   23.06%   211  coq-stdlib/setoid_ring/Ncring_tac.v.html                   │
│ 0.1330  0.2670  0.1340  100.75%   160  coq-stdlib/MSets/MSetProperties.v.html                     │
│ 0.4030  0.5320  0.1290   32.01%   387  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html        │
│ 0.2910  0.4150  0.1240   42.61%   138  coq-stdlib/setoid_ring/Ncring_initial.v.html               │
│ 0.1590  0.2660  0.1070   67.30%   914  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html     │
│ 0.2420  0.3390  0.0970   40.08%    11  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html        │
│ 0.1020  0.1990  0.0970   95.10%   314  coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html           │
│ 0.2420  0.3380  0.0960   39.67%   301  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html        │
│ 0.7700  0.8650  0.0950   12.34%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                   │
│ 0.1720  0.2640  0.0920   53.49%    16  coq-stdlib/Numbers/HexadecimalQ.v.html                     │
│ 0.4470  0.5380  0.0910   20.36%   870  coq-stdlib/MSets/MSetRBT.v.html                            │
│ 0.1950  0.2830  0.0880   45.13%   315  coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html           │
│ 0.3480  0.4350  0.0870   25.00%   634  coq-stdlib/setoid_ring/Field_theory.v.html                 │
│ 0.1730  0.2600  0.0870   50.29%  1981  coq-stdlib/FSets/FMapFacts.v.html                          │
│ 0.3640  0.4460  0.0820   22.53%  1045  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html         │
│ 0.2020  0.2840  0.0820   40.59%    11  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html           │
│ 0.3160  0.3940  0.0780   24.68%   443  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html        │
│ 0.1960  0.2700  0.0740   37.76%    19  coq-stdlib/Reals/Abstract/ConstructiveLUB.v.html           │
│ 0.5160  0.5850  0.0690   13.37%  2222  coq-stdlib/FSets/FMapAVL.v.html                            │
│ 0.1590  0.2270  0.0680   42.77%    12  coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html        │
│ 0.0600  0.1260  0.0660  110.00%   788  coq-stdlib/MSets/MSetDecide.v.html                         │
└───────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                        TOP 25 SPEED UPS                                        │
│                                                                                                │
│  OLD     NEW     DIFF     %DIFF    Ln             FILE                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 1.5510  1.1380  -0.4130  -26.63%   853  coq-stdlib/FSets/FMapAVL.v.html                        │
│ 2.3350  1.9330  -0.4020  -17.22%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │
│ 0.4010  0.1760  -0.2250  -56.11%   219  coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html    │
│ 0.3950  0.1880  -0.2070  -52.41%   637  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html       │
│ 0.3350  0.1400  -0.1950  -58.21%   637  coq-stdlib/Reals/Abstract/ConstructiveSum.v.html       │
│ 0.3350  0.2200  -0.1150  -34.33%    16  coq-stdlib/Numbers/HexadecimalN.v.html                 │
│ 0.7700  0.6570  -0.1130  -14.68%   422  coq-stdlib/MSets/MSetList.v.html                       │
│ 0.4040  0.2930  -0.1110  -27.48%   652  coq-stdlib/ZArith/Znumtheory.v.html                    │
│ 0.4030  0.2950  -0.1080  -26.80%  1363  coq-stdlib/FSets/FMapAVL.v.html                        │
│ 0.3230  0.2160  -0.1070  -33.13%    57  coq-stdlib/Strings/Byte.v.html                         │
│ 0.2370  0.1350  -0.1020  -43.04%  1235  coq-stdlib/Logic/ChoiceFacts.v.html                    │
│ 0.1840  0.0830  -0.1010  -54.89%   320  coq-stdlib/Reals/Abstract/ConstructiveAbs.v.html       │
│ 0.1430  0.0540  -0.0890  -62.24%  1574  coq-stdlib/micromega/Tauto.v.html                      │
│ 0.7550  0.6660  -0.0890  -11.79%    75  coq-stdlib/Numbers/HexadecimalString.v.html            │
│ 0.1890  0.1010  -0.0880  -46.56%   790  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │
│ 0.2540  0.1690  -0.0850  -33.46%    18  coq-stdlib/FSets/FMapFacts.v.html                      │
│ 0.1370  0.0540  -0.0830  -60.58%   221  coq-stdlib/Reals/Abstract/ConstructiveMinMax.v.html    │
│ 1.3680  1.2860  -0.0820   -5.99%    73  coq-stdlib/Numbers/HexadecimalString.v.html            │
│ 0.1870  0.1050  -0.0820  -43.85%   742  coq-stdlib/micromega/EnvRing.v.html                    │
│ 1.0210  0.9390  -0.0820   -8.03%   467  coq-stdlib/Numbers/DecimalFacts.v.html                 │
│ 0.1850  0.1040  -0.0810  -43.78%   758  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │
│ 0.3890  0.3100  -0.0790  -20.31%   198  coq-stdlib/setoid_ring/Ncring_initial.v.html           │
│ 0.1400  0.0620  -0.0780  -55.71%   160  coq-stdlib/FSets/FSetProperties.v.html                 │
│ 1.5730  1.4950  -0.0780   -4.96%   596  coq-stdlib/Strings/Byte.v.html                         │
│ 1.1230  1.0460  -0.0770   -6.86%   316  coq-stdlib/Strings/Byte.v.html                         │
└────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[SkySkimmer]

ping @coq/test-suite-maintainers

[JasonGross]

Do you want to also add support for TIMING=1 while you're at it, so we can get per-line diffs?

[SkySkimmer]

Maybe someday but not in this PR

[SkySkimmer]

@coq/test-suite-maintainers can this get an assignee (and merge?)?

[herbelin]

If @JasonGross and @ejgallego do not object, I'll merge tomorrow (I'm not familiar myself with timing).

[JasonGross]

I don't have time to review right now, but the implementation looked okay at a quick glance, and I strongly support this change

[ejgallego]

I don't objec to this; however I think we should stop updating test-suite/Makefile and focus / decide on a an alternative system. The more things we add to test-suite/Makefile the more we waste time doubly, on the addition to it, and having to port to whatever next systems succeeds the current gargantuan Makefile (so in a sense, this PR add technical debt)

As of today the experience of running the test suite is very very poor, to the point that a few people have been discouraged of even trying to contribute to Coq when they had to face it.

The main leading alternative is Ali's work on porting the test-suite to Dune; that work is IMHO netly superior to what we have now, and adding features like the ones in this PR tends to be both easy and maintenable (note that I didn't try to look at this concrete PR, so here I'm just guessing)

[herbelin]

I then propose to postpone to Monday when we'll be able to talk live.

[SkySkimmer]

I think this should still be merged even if we plan to eventually replace the makefile. It is not that complex a change IMO, and anyway it's for devs not users so if the port requires dropping the feature we can do it (unless the feature is considered important, but if it's important then we should merge).

[herbelin]

It looks like a good argument. Emilio, I propose to merge which will not mean that it cannot change in the future.

[ejgallego]

Sure, as noted I don't oppose this PR at all, ln the other hand I'm afraid I can't help a lot with the make side.

[herbelin]

See discussion

[herbelin]

OK. @coqbot merge now

[herbelin]

@coqbot merge now