WIP statically control access to summary

[SkySkimmer]

No description provided.

[SkySkimmer]

New version with less overdesigned (IMO) API
This time I pushed it until it passes the corelib + most of the test suite
Failing tests should be just:

• Anomaly: Universe undefined #4603 (fails with invalid argument index out of bounds, involves adding a Definition in the middle of a proof)
• some fake_ide tests (ie STM is bugged somehow)

There are also lurking bugs when going back and forth over commands which load plugins. We need to somehow add new summary states to the "active" state (cf code in mltop, but the code is not robust to backtracking).
May also be buggy if plugins get statically linked? not sure

I'll try to explain the design later (not today)

[SkySkimmer]

@coqbot bench

[coqbot-app]

No check suite 31373 for head commit dc3e9af.

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

@coqbot bench

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

All plugins need overlays and the mltop new summary capture probably needs improvement but otherwise this seems to work (!)

The declare hooks are currently a bit footgunny though, it works like

let some_function summary args =
  (* immediately declare some constant *)
  let _ : globref = Declare.declare_constant summary ... in
  (* then open an interactive proof *)
  let info = Declare.Info.make ~hook:(Declare.Hook.make @@ fun summary s -> Declare.declare_constant summary ...) ... in
  ...
  Declare.Proof.start_definition ~info ...

the problem is the shadowing (at the same type) of summary in the hook. Reusing the surrounding summary is a bug.
Not sure if there's any way to make this less footgunny while keeping the imperative summary handle (instead of full immutable style returning the updated summary). And while we still have global imperative state trying to treat the state as immutable seems like its own footgun.

EDIT added a dynamic check that "mut" handles are not outdated

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬──────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]   │
│                                     │                         │                                       │                          │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF  │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼──────────────────────────┤
│               coq-engine-bench-lite │  126.83   127.28  -0.35 │   946865784598    949034654174  -0.23 │ 1085048  1084820    0.02 │
│ coq-neural-net-interp-computed-lite │  237.50   237.28   0.09 │  2262920327316   2261510001421   0.06 │  844408   916372   -7.85 │
│                             coq-vst │  830.54   828.15   0.29 │  6292799772383   6276078732188   0.27 │ 2178060  2182732   -0.21 │
│                   coq-iris-examples │  365.91   364.69   0.33 │  2411066063440   2398372707236   0.53 │ 1130660  1121792    0.79 │
│                            coq-core │    2.89     2.88   0.35 │    19704925320     19681264612   0.12 │  106584   106740   -0.15 │
│                         coq-unimath │ 1787.10  1778.08   0.51 │ 14832339940830  14779735002014   0.36 │ 1125588  1090012    3.26 │
│                        coq-bedrock2 │  352.87   351.01   0.53 │  2918199858796   2911152751026   0.24 │  847812   829064    2.26 │
│                        coq-compcert │  301.37   299.52   0.62 │  1965630563009   1952130594117   0.69 │ 1252868  1295444   -3.29 │
│                        rocq-runtime │   74.70    74.22   0.65 │   542635919173    539359618463   0.61 │  516436   516180    0.05 │
│          coq-performance-tests-lite │  910.59   904.16   0.71 │  7284638592590   7264233251905   0.28 │ 2204544  2204624   -0.00 │
│                         coq-coqutil │   46.37    46.04   0.72 │   288496662795    285992613970   0.88 │  564480   562456    0.36 │
│                    coq-fiat-parsers │  275.24   273.12   0.78 │  2106514596566   2101152952059   0.26 │ 2038384  2350208  -13.27 │
│                      coq-verdi-raft │  496.96   492.33   0.94 │  3417776507049   3410536844051   0.21 │  820260   823052   -0.34 │
│                            coq-hott │  161.21   159.03   1.37 │  1100787807300   1092044907930   0.80 │  470912   470220    0.15 │
│                           coq-verdi │   42.96    42.37   1.39 │   284017140669    282681779084   0.47 │  527596   527104    0.09 │
│                         rocq-stdlib │  457.39   445.53   2.66 │  1557517002027   1539452265035   1.17 │  626800   626364    0.07 │
│                           rocq-core │    6.86     6.67   2.85 │    41786765303     40980815905   1.97 │  461772   457948    0.84 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
rocq-bignums (in NEW)
rocq-elpi (in NEW)
rocq-equations (in NEW)
coq-rewriter (in NEW)
coq-fiat-core (in NEW)

rocq-mathcomp-boot (dependency rocq-elpi failed)
rocq-mathcomp-order (dependency rocq-elpi failed)
rocq-mathcomp-ssreflect (dependency rocq-elpi failed)
rocq-mathcomp-fingroup (dependency rocq-elpi failed)
rocq-mathcomp-algebra (dependency rocq-elpi failed)
rocq-mathcomp-solvable (dependency rocq-elpi failed)
rocq-mathcomp-field (dependency rocq-elpi failed)
rocq-mathcomp-character (dependency rocq-elpi failed)
coq-mathcomp-odd-order (dependency rocq-elpi failed)
coq-mathcomp-analysis (dependency rocq-elpi failed)
coq-math-classes (dependency rocq-bignums failed)
coq-corn (dependency rocq-bignums failed)
rocq-metarocq-utils (dependency rocq-equations failed)
rocq-metarocq-common (dependency rocq-equations failed)
rocq-metarocq-template (dependency rocq-equations failed)
rocq-metarocq-pcuic (dependency rocq-equations failed)
rocq-metarocq-safechecker (dependency rocq-equations failed)
rocq-metarocq-erasure (dependency rocq-equations failed)
rocq-metarocq-translations (dependency rocq-equations failed)
coq-color (dependency rocq-bignums failed)
coq-coqprime (dependency rocq-bignums failed)
coq-fiat-crypto-with-bedrock (dependency coq-rewriter failed)
coq-coquelicot (dependency rocq-elpi failed)
coq-fourcolor (dependency rocq-elpi failed)
coq-rewriter-perf-SuperFast (dependency coq-rewriter failed)
coq-category-theory (dependency rocq-equations failed)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                       TOP 25 SLOW DOWNS                                                       │
│                                                                                                                               │
│  OLD    NEW    DIFF    %DIFF   Ln                    FILE                                                                     │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  94.3   97.0  2.6812    2.84%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html           │
│  94.5   97.1  2.5785    2.73%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html           │
│  64.4   65.6  1.1792    1.83%  608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                               │
│  38.0   38.6  0.5814    1.53%  224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html            │
│  1.18   1.72  0.5385   45.70%  813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                 │
│ 0.278  0.815  0.5377  193.71%   12  rocq-stdlib/theories/MSets/MSets.v.html                                                   │
│  1.49   1.98  0.4868   32.59%  313  rocq-stdlib/theories/Strings/Byte.v.html                                                  │
│  36.6   37.1  0.4676    1.28%  139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                              │
│  1.28   1.72  0.4351   33.94%   75  rocq-stdlib/theories/Numbers/HexadecimalString.v.html                                     │
│ 0.814   1.23  0.4115   50.53%  816  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                 │
│  21.6   22.0  0.3639    1.68%  651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                 │
│ 0.432  0.795  0.3625   83.83%  249  rocq-stdlib/theories/Structures/OrdersEx.v.html                                           │
│ 0.273  0.602  0.3281  120.00%   11  rocq-stdlib/theories/QArith/Qring.v.html                                                  │
│  2.80   3.08  0.2826   10.11%  597  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/SetGroupoidComprehension.v.html │
│  1.14   1.39  0.2452   21.47%  408  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                 │
│ 0.263  0.502  0.2396   91.21%   14  rocq-stdlib/theories/Logic/Epsilon.v.html                                                 │
│ 0.394  0.622  0.2280   57.81%  422  rocq-stdlib/theories/MSets/MSetList.v.html                                                │
│  18.7   18.9  0.2226    1.19%  481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                         │
│ 0.301  0.505  0.2042   67.92%   18  rocq-stdlib/theories/FSets/FMapFacts.v.html                                               │
│ 0.431  0.632  0.2018   46.86%   16  rocq-stdlib/theories/Structures/OrdersEx.v.html                                           │
│ 0.518  0.708  0.1893   36.53%   13  rocq-stdlib/theories/QArith/Qreduction.v.html                                             │
│ 0.401  0.582  0.1812   45.21%   59  rocq-stdlib/theories/ZArith/Zeuclid.v.html                                                │
│ 0.362  0.540  0.1778   49.12%    1  rocq-stdlib/theories/btauto/Algebra.v.html                                                │
│ 0.425  0.601  0.1757   41.30%  705  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html                                      │
│ 0.365  0.539  0.1739   47.67%   16  rocq-stdlib/theories/extraction/ExtrOcamlIntConv.v.html                                   │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                         TOP 25 SPEED UPS                                                          │
│                                                                                                                                   │
│  OLD      NEW     DIFF     %DIFF    Ln                   FILE                                                                     │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   3.17     2.54  -0.6344  -20.02%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                │
│ 33.802   33.355  -0.4470   -1.32%   194  coq-vst/veric/expr_lemmas4.v.html                                                        │
│  34.75   34.321  -0.4290   -1.23%   147  coq-vst/veric/expr_lemmas4.v.html                                                        │
│ 32.173   31.795  -0.3780   -1.17%    97  coq-vst/veric/binop_lemmas5.v.html                                                       │
│   46.8     46.5  -0.3233   -0.69%   115  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                               │
│   12.0     11.7  -0.3209   -2.68%   388  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│  6.376    6.094  -0.2820   -4.42%   192  coq-vst/veric/binop_lemmas5.v.html                                                       │
│   7.84     7.57  -0.2654   -3.39%   633  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│   1.14    0.872  -0.2651  -23.32%   690  rocq-stdlib/theories/setoid_ring/Field_theory.v.html                                     │
│   12.1     11.8  -0.2570   -2.13%   324  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│   12.3     12.1  -0.2286   -1.86%   930  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html    │
│  0.703    0.494  -0.2095  -29.80%   200  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                       │
│  0.509    0.304  -0.2049  -40.23%   719  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                │
│  0.552    0.348  -0.2040  -36.95%    11  rocq-stdlib/theories/setoid_ring/Rings_Z.v.html                                          │
│   7.76     7.55  -0.2023   -2.61%    30  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                │
│   3.48     3.28  -0.2007   -5.77%   196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                            │
│  0.189  0.00496  -0.1838  -97.37%   449  rocq-stdlib/theories/FSets/FMapAVL.v.html                                                │
│  0.676    0.500  -0.1762  -26.06%  1290  rocq-stdlib/theories/Logic/ChoiceFacts.v.html                                            │
│  0.512    0.337  -0.1753  -34.25%   609  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                │
│  0.498    0.325  -0.1723  -34.62%   650  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                │
│  0.394    0.223  -0.1714  -43.45%    28  rocq-stdlib/theories/Structures/OrdersEx.v.html                                          │
│  0.171  0.00486  -0.1659  -97.15%    38  rocq-stdlib/theories/Zmod/ZstarDef.v.html                                                │
│  0.403    0.239  -0.1644  -40.79%   759  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                │
│   4.61     4.45  -0.1633   -3.54%   646  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │
│  0.281    0.123  -0.1577  -56.09%    25  rocq-stdlib/theories/Logic/ClassicalChoice.v.html                                        │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job