Turn on Proof Using Clear Unused by default

[SkySkimmer]

Depends:

• Restore "Proof Using Clear Unused" #22107

Overlays:

• Adapt to rocq-prover/rocq#22113 (Proof Using Clear Unused) stdlib#276
• More accurate clears after proof using MetaRocq/metarocq#1278
• https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1237

[SkySkimmer]

Quite small stdlib overlay.
It does show a pattern we may want to provide some backward compat for of doing Proof using stuff. clear rest..
The clear core (Tactics.clear_gen) already warns instead of error when the id is unknown, but the ltac1 binding uses hyp_list and hyp errors.
Changing to something like id_list is a bit more work than it seems because the ltac1 runtime has special support for hyp_list (Tacinterp.interp_hyp_list & co)

[SkySkimmer]

@coqbot bench

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│             rocq-mathcomp-ssreflect │    1.13     1.17  -3.42 │     7693679554      7688353920   0.07 │  594056   592180   0.32 │
│                      coq-verdi-raft │  474.60   490.70  -3.28 │  3293400747318   3396261293512  -3.03 │  810728   814428  -0.45 │
│                            coq-core │    2.71     2.76  -1.81 │    18617839512     18624265678  -0.03 │   90960    90824   0.15 │
│                      rocq-equations │    8.51     8.63  -1.39 │    59116682699     59099053380   0.03 │  399712   399476   0.06 │
│                           coq-verdi │   42.49    43.04  -1.28 │   283490294823    287174513165  -1.28 │  526996   526396   0.11 │
│                         rocq-stdlib │  416.01   419.35  -0.80 │  1508935798508   1508647543166   0.02 │  763676   757420   0.83 │
│                        coq-compcert │  304.12   306.13  -0.66 │  1998221079390   1998377126941  -0.01 │ 1201908  1200776   0.09 │
│                        rocq-bignums │   25.09    25.24  -0.59 │   160443169280    160468900105  -0.02 │  460248   463024  -0.60 │
│ coq-neural-net-interp-computed-lite │  236.62   237.57  -0.40 │  2262475747063   2262374993881   0.00 │  883288   881496   0.20 │
│                    coq-math-classes │   82.16    82.26  -0.12 │   498346042444    498300020249   0.01 │  513700   515204  -0.29 │
│                        rocq-runtime │   76.08    76.17  -0.12 │   551104363225    551336534298  -0.04 │  495596   495360   0.05 │
│                         coq-coqutil │   47.11    47.15  -0.08 │   292586205814    292289260979   0.10 │  565732   565448   0.05 │
│                      coq-coquelicot │   38.73    38.76  -0.08 │   234595327220    234463291655   0.06 │  825208   826012  -0.10 │
│                    coq-fiat-parsers │  271.67   271.63   0.01 │  2090229830108   2089611204582   0.03 │ 2036556  2036544   0.00 │
│                   coq-iris-examples │  364.53   364.41   0.03 │  2377875046770   2381468110311  -0.15 │ 1061820  1071960  -0.95 │
│                           coq-color │  229.47   229.37   0.04 │  1456760831204   1456031866190   0.05 │ 1160076  1159956   0.01 │
│                         coq-unimath │ 1885.11  1884.27   0.04 │ 15707735952519  15705089631887   0.02 │ 1708408  1706700   0.10 │
│                 rocq-mathcomp-order │   81.19    81.14   0.06 │   601547370496    601523332695   0.00 │ 1618308  1618296   0.00 │
│                 rocq-mathcomp-field │  193.08   192.95   0.07 │  1453029911254   1453217072743  -0.01 │ 2309772  2315272  -0.24 │
│          rocq-mathcomp-finite-group │   26.44    26.42   0.08 │   172590476419    172645773414  -0.03 │  568564   570568  -0.35 │
│                             coq-vst │  834.02   832.49   0.18 │  6322033914074   6321120985536   0.01 │ 2161004  2161320  -0.01 │
│          coq-performance-tests-lite │  886.58   884.22   0.27 │  7118234034150   7119181653621  -0.01 │ 1570800  1513356   3.80 │
│               coq-engine-bench-lite │  128.17   127.79   0.30 │   951754691782    951268826249   0.05 │ 1004804  1004568   0.02 │
│  rocq-mathcomp-group-representation │  103.89   103.58   0.30 │   729518885535    729561247371  -0.01 │ 1707688  1707700  -0.00 │
│                       coq-fourcolor │ 1352.92  1348.78   0.31 │ 12427483053473  12427166042174   0.00 │ 1020124  1020364  -0.02 │
│               rocq-mathcomp-algebra │  392.09   390.71   0.35 │  2894920485532   2894849250007   0.00 │ 1594716  1596668  -0.12 │
│                            coq-hott │  157.48   156.88   0.38 │  1058452972046   1058329354574   0.01 │  460220   459952   0.06 │
│                        coq-coqprime │   56.79    56.55   0.42 │   393727487612    393820491135  -0.02 │  821804   821832  -0.00 │
│                       coq-fiat-core │   55.47    55.23   0.43 │   335245254264    334827438013   0.12 │  483228   482776   0.09 │
│              coq-mathcomp-odd-order │  606.83   604.18   0.44 │  4283941551400   4284128518636  -0.00 │ 2655124  2653904   0.05 │
│              rocq-mathcomp-solvable │   98.72    98.26   0.47 │   666451059730    666453969213  -0.00 │ 1094740  1094732   0.00 │
│                           rocq-elpi │   16.27    16.17   0.62 │   116211268615    116203883338   0.01 │  450940   450988  -0.01 │
│                            coq-corn │  640.84   636.69   0.65 │  4329520307146   4329534532062  -0.00 │  619396   619496  -0.02 │
│               coq-mathcomp-analysis │ 1232.88  1224.02   0.72 │  9010950765969   9010512521280   0.00 │ 2114200  2114496  -0.01 │
│                           rocq-core │    6.82     6.77   0.74 │    41373872045     41370102080   0.01 │  447588   448100  -0.11 │
│                  rocq-mathcomp-boot │   39.73    39.30   1.09 │   233345303934    233297909447   0.02 │  663616   662320   0.20 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-metarocq-utils (in NEW)
coq-bedrock2 (in NEW)
coq-rewriter (in NEW)
coq-category-theory (in NEW)

rocq-metarocq-common (dependency rocq-metarocq-utils failed)
rocq-metarocq-template (dependency rocq-metarocq-utils failed)
rocq-metarocq-pcuic (dependency rocq-metarocq-utils failed)
rocq-metarocq-safechecker (dependency rocq-metarocq-utils failed)
rocq-metarocq-erasure (dependency rocq-metarocq-utils failed)
rocq-metarocq-translations (dependency rocq-metarocq-utils failed)
coq-fiat-crypto-with-bedrock (dependency coq-rewriter failed)
coq-rewriter-perf-SuperFast (dependency coq-rewriter failed)

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SLOW DOWNS                                                            │
│                                                                                                                                        │
│   OLD     NEW    DIFF    %DIFF     Ln                     FILE                                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    38.4   39.1  0.6977     1.82%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                 │
│    48.4   49.1  0.6755     1.40%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                    │
│    18.2   18.7  0.4386     2.40%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                      │
│  38.806  39.23  0.4240     1.09%   834  coq-vst/veric/binop_lemmas4.v.html                                                             │
│   0.299  0.704  0.4046   135.17%    15  rocq-stdlib/theories/ZArith/Zeuclid.v.html                                                     │
│   0.328  0.718  0.3897   118.85%    18  rocq-stdlib/theories/micromega/VarMap.v.html                                                   │
│   0.523  0.894  0.3716    71.09%   597  rocq-stdlib/theories/Strings/Byte.v.html                                                       │
│   0.780   1.15  0.3692    47.34%   408  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                      │
│   0.789   1.16  0.3677    46.61%   200  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                             │
│    26.1   26.4  0.3595     1.38%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                    │
│   0.304  0.644  0.3401   111.98%    18  rocq-stdlib/theories/ZArith/Zeven.v.html                                                       │
│   0.280  0.613  0.3333   119.03%   596  rocq-stdlib/theories/Strings/Byte.v.html                                                       │
│    30.9   31.2  0.3221     1.04%    13  coq-fourcolor/theories/proof/job254to270.v.html                                                │
│ 0.00769  0.308  0.2999  3899.67%    97  coq-mathcomp-analysis/theories/topology_theory/compact.v.html                                  │
│    26.1   26.4  0.2992     1.15%   374  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                    │
│    20.8   21.1  0.2783     1.34%   338  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                    │
│   0.124  0.393  0.2692   217.55%    14  rocq-stdlib/theories/setoid_ring/Ncring.v.html                                                 │
│    24.7   25.0  0.2614     1.06%    13  coq-fourcolor/theories/proof/job503to506.v.html                                                │
│    8.13   8.38  0.2482     3.05%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                                              │
│    25.1   25.3  0.2381     0.95%    13  coq-fourcolor/theories/proof/job279to282.v.html                                                │
│    7.43   7.65  0.2269     3.06%   602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │
│    88.7   88.9  0.2197     0.25%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                │
│   3.661  3.879  0.2180     5.95%   534  coq-vst/floyd/local2ptree_typecheck.v.html                                                     │
│    25.0   25.2  0.2102     0.84%    13  coq-fourcolor/theories/proof/job299to302.v.html                                                │
│ 0.00870  0.215  0.2068  2377.32%    97  coq-mathcomp-analysis/theories/lebesgue_integral_theory/lebesgue_integral_definition.v.html    │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SPEED UPS                                                             │
│                                                                                                                                          │
│  OLD      NEW      DIFF     %DIFF    Ln                     FILE                                                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    202       202  -0.6898   -0.34%      8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│   18.4      17.8  -0.5328   -2.90%     32  coq-performance-tests-lite/src/pattern.v.html                                                 │
│   11.0      10.6  -0.4528   -4.10%    410  coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html                          │
│  0.614     0.189  -0.4249  -69.16%    682  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                                              │
│  0.382  0.000426  -0.3813  -99.89%     36  coq-mathcomp-analysis/theories/probability_theory/exponential_distribution.v.html             │
│  0.602     0.239  -0.3628  -60.31%    374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                │
│  0.344   0.00485  -0.3394  -98.59%    112  coq-mathcomp-analysis/theories/esum.v.html                                                    │
│  0.551     0.212  -0.3384  -61.46%    484  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html                                          │
│  0.608     0.275  -0.3326  -54.70%    586  rocq-stdlib/theories/Strings/Byte.v.html                                                      │
│  0.619     0.305  -0.3137  -50.67%     14  rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html                                          │
│  0.302  0.000771  -0.3013  -99.74%     96  coq-mathcomp-analysis/theories/topology_theory/compact.v.html                                 │
│   4.40      4.11  -0.2921   -6.64%    204  coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html                                   │
│  0.871     0.590  -0.2809  -32.25%   1834  coq-verdi-raft/theories/RaftProofs/StateMachineSafetyProof.v.html                             │
│  0.363    0.0821  -0.2805  -77.35%    585  rocq-stdlib/theories/Strings/Byte.v.html                                                      │
│   3.48      3.21  -0.2642   -7.60%    492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                          │
│ 34.327    34.074  -0.2530   -0.74%     97  coq-vst/veric/binop_lemmas5.v.html                                                            │
│   1.07     0.817  -0.2512  -23.51%    816  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                     │
│  0.245  0.000160  -0.2447  -99.93%     94  coq-mathcomp-analysis/theories/independence.v.html                                            │
│   27.1      26.8  -0.2403   -0.89%     13  coq-fourcolor/theories/proof/job531to534.v.html                                               │
│  0.417     0.188  -0.2292  -54.91%     16  rocq-stdlib/theories/Numbers/HexadecimalPos.v.html                                            │
│  0.555     0.328  -0.2272  -40.95%    141  rocq-stdlib/theories/Strings/Ascii.v.html                                                     │
│  0.223  0.000616  -0.2229  -99.72%  19268  coq-coqprime/src/Coqprime/examples/BasePrimes.v.html                                          │
│   9.51      9.29  -0.2229   -2.34%    978  coq-verdi-raft/theories/Raft/Linearizability.v.html                                           │
│   18.5      18.3  -0.2213   -1.19%     13  coq-fourcolor/theories/proof/job311to314.v.html                                               │
│  0.632     0.412  -0.2204  -34.85%      1  rocq-stdlib/theories/btauto/Algebra.v.html                                                    │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[SkySkimmer]

@coqbot bench

[SkySkimmer]

allowing unbound variables in clear args is also not going to work, cf https://gitlab.inria.fr/coq/coq/-/jobs/7483897

[SkySkimmer]

see also #883