Remove vernacstate cache by SkySkimmer · Pull Request #21975 · rocq-prover/rocq

SkySkimmer · 2026-04-29T11:15:27Z

Knowing when to call invalidate is tricky so if bench agrees it's
better to remove this.

Indeed in master the cache is handled unsoundly (skips unfreeze of a state which isn't the currently installed state) which hides some bugs:

STM restore_root_state would overwrite Flags.quiet set in init_extra (but unsound cache makes it a noop)
rocqide would overwrite user printing options with the default (but unsound cache prevents the overwrite)

Overlays:

SkySkimmer · 2026-04-29T11:21:34Z

@coqbot bench

SkySkimmer · 2026-04-29T13:54:42Z

rocqide bug (also in master):

Lemma foo : Set.
Proof.
exact Type.
Qed.

step to after Proof, set printing universes in IDE interface, go to end: the error message does not print universes
(it does print universes if you only stepped to before Proof before setting the option AFAICT)

coqbot-app · 2026-04-29T21:22:47Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                            coq-core │    2.69     2.74  -1.82 │    18289363886     18288014450   0.01 │   90384    90500  -0.13 │
│                         coq-coqutil │   47.55    47.84  -0.61 │   293581639125    293573464336   0.00 │  569900   569588   0.05 │
│               coq-engine-bench-lite │  129.48   129.76  -0.22 │   961453238421    960881960344   0.06 │ 1007792  1005460   0.23 │
│                rocq-metarocq-common │   41.50    41.56  -0.14 │   266720953858    266197758690   0.20 │  927124   922704   0.48 │
│              rocq-metarocq-template │   85.16    85.27  -0.13 │   581438597221    581941908147  -0.09 │ 1094876  1109020  -1.28 │
│                        coq-rewriter │  334.21   334.62  -0.12 │  2475483309870   2474112329370   0.06 │ 1571108  1542604   1.85 │
│                    coq-math-classes │   84.02    84.11  -0.11 │   507495541018    507822414920  -0.06 │  517264   513708   0.69 │
│                 rocq-metarocq-utils │   24.80    24.82  -0.08 │   159776582468    158892961484   0.56 │  588612   589164  -0.09 │
│                    coq-fiat-parsers │  280.09   280.26  -0.06 │  2136348959948   2136130032872   0.01 │ 2327248  2331168  -0.17 │
│        coq-fiat-crypto-with-bedrock │ 7348.03  7350.89  -0.04 │ 60265262729055  60274815968337  -0.02 │ 3099644  3100004  -0.01 │
│                   coq-iris-examples │  371.68   371.48   0.05 │  2421334270585   2422193120413  -0.04 │ 1086684  1124964  -3.40 │
│                      rocq-equations │    8.64     8.63   0.12 │    58430294180     58225258439   0.35 │  401036   402112  -0.27 │
│                        rocq-runtime │   75.64    75.52   0.16 │   548693748114    548609767489   0.02 │  504316   506252  -0.38 │
│                 rocq-metarocq-pcuic │  659.46   658.28   0.18 │  4174311412496   4167593220080   0.16 │ 2304460  2327976  -1.01 │
│                        coq-bedrock2 │  362.46   361.61   0.24 │  3002462841436   3000775886346   0.06 │  888848   879708   1.04 │
│                 coq-category-theory │  560.52   558.86   0.30 │  4066468640567   4062315494494   0.10 │  875384   875556  -0.02 │
│               rocq-metarocq-erasure │  485.68   484.05   0.34 │  3303905872055   3299339987236   0.14 │ 1811604  1817684  -0.33 │
│           rocq-metarocq-safechecker │  348.14   346.87   0.37 │  2525456883982   2523790123483   0.07 │ 1873552  1868676   0.26 │
│          coq-performance-tests-lite │  911.38   907.96   0.38 │  7252352004168   7243705295848   0.12 │ 1268504  1267960   0.04 │
│                       coq-fiat-core │   56.61    56.35   0.46 │   342210077235    341504874439   0.21 │  482464   484564  -0.43 │
│                         coq-unimath │ 1856.99  1845.45   0.63 │ 15281545069128  15252389989957   0.19 │ 1085992  1061924   2.27 │
│                      coq-verdi-raft │  502.07   498.61   0.69 │  3452779831622   3445745754195   0.20 │  822656   819580   0.38 │
│                           coq-verdi │   44.41    44.07   0.77 │   292594439653    293361543336  -0.26 │  526356   527992  -0.31 │
│         coq-rewriter-perf-SuperFast │  481.88   478.02   0.81 │  3732457035692   3731163295526   0.03 │ 1284456  1238880   3.68 │
│                           coq-color │  236.79   234.43   1.01 │  1489673178477   1479613391605   0.68 │ 1179600  1181340  -0.15 │
│                        rocq-bignums │   25.93    25.67   1.01 │   162734206151    162597318259   0.08 │  458592   463424  -1.04 │
│                         rocq-stdlib │  443.83   439.05   1.09 │  1576872221949   1560924355020   1.02 │  644816   645856  -0.16 │
│ coq-neural-net-interp-computed-lite │  241.82   239.04   1.16 │  2268450074317   2267655382292   0.04 │  899424   893348   0.68 │
│                            coq-hott │  160.53   157.75   1.76 │  1070935476378   1064354298836   0.62 │  458716   462280  -0.77 │
│                        coq-coqprime │   54.76    53.67   2.03 │   368774140241    365327395475   0.94 │  823788   821888   0.23 │
│                           rocq-core │    6.98     6.83   2.20 │    41812928802     41428071562   0.93 │  448780   448296   0.11 │
│          rocq-metarocq-translations │   16.91    16.20   4.38 │   118785418110    115004700262   3.29 │  779000   782052  -0.39 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-elpi (in NEW)
coq-compcert (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-corn (dependency rocq-elpi failed)
coq-coquelicot (dependency rocq-elpi failed)
coq-fourcolor (dependency rocq-elpi failed)
coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SLOW DOWNS                                                             │
│                                                                                                                                           │
│  OLD    NEW    DIFF    %DIFF   Ln                      FILE                                                                               │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   203    206  3.0066    1.48%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html         │
│  94.3   96.5  2.1806    2.31%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                       │
│  94.9   96.5  1.6773    1.77%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                       │
│  21.7   22.5  0.8106    3.74%   49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                               │
│  41.9   42.7  0.7804    1.86%  221  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                          │
│  36.1   36.9  0.7441    2.06%  222  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                          │
│  22.9   23.5  0.6337    2.77%  776  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                  │
│  26.8   27.5  0.6294    2.35%  794  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                  │
│ 0.944   1.54  0.5970   63.25%  572  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                             │
│  21.4   22.0  0.5613    2.62%  242  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                          │
│  30.5   31.1  0.5588    1.83%  223  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                          │
│  24.3   24.8  0.4968    2.05%  782  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                  │
│  31.0   31.5  0.4896    1.58%  255  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                            │
│  25.0   25.4  0.4548    1.82%  224  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                          │
│  18.0   18.4  0.4447    2.47%   32  coq-performance-tests-lite/src/pattern.v.html                                                         │
│  38.4   38.8  0.4441    1.16%  224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                        │
│  44.6   45.0  0.4305    0.97%  257  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                         │
│ 0.346  0.775  0.4292  124.16%  682  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                                                      │
│  3.81   4.23  0.4244   11.14%  492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                  │
│  20.3   20.7  0.4138    2.04%  233  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                          │
│  36.6   37.0  0.4106    1.12%  139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                          │
│  17.0   17.4  0.3990    2.34%  762  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                  │
│  25.1   25.5  0.3918    1.56%  550  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html     │
│  16.9   17.2  0.3697    2.19%    6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.v.html │
│  3.40   3.75  0.3513   10.34%  233  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/RecodeProofs.v.html                                     │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                             │
│                                                                                                                                         │
│  OLD    NEW     DIFF     %DIFF    Ln                     FILE                                                                           │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  40.3    39.1  -1.2355   -3.07%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│  44.4    43.5  -0.9513   -2.14%   578  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                 │
│  84.0    83.2  -0.8161   -0.97%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                          │
│  12.2    11.5  -0.6939   -5.69%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                         │
│  2.76    2.14  -0.6281  -22.72%   212  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                               │
│   108     108  -0.6070   -0.56%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                           │
│  12.9    12.3  -0.5689   -4.41%  1628  coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html                                      │
│  30.4    29.8  -0.5555   -1.83%   305  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                               │
│ 0.773   0.230  -0.5430  -70.24%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                   │
│  54.8    54.3  -0.5328   -0.97%   296  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                               │
│ 0.776   0.271  -0.5050  -65.04%   484  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html                                             │
│  4.15    3.66  -0.4889  -11.78%   196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                                    │
│  21.1    20.7  -0.4089   -1.94%   479  rocq-metarocq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksFixLambdaInd.v.html                 │
│ 0.800   0.398  -0.4015  -50.20%  1604  rocq-stdlib/theories/micromega/Tauto.v.html                                                      │
│ 0.905   0.507  -0.3983  -44.01%   586  rocq-stdlib/theories/Strings/Byte.v.html                                                         │
│  42.3    41.9  -0.3967   -0.94%   543  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│  59.6    59.2  -0.3921   -0.66%   659  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                            │
│  10.0    9.66  -0.3662   -3.65%  2852  coq-fiat-crypto-with-bedrock/src/Assembly/EquivalenceProofs.v.html                               │
│  34.7    34.3  -0.3649   -1.05%   898  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                             │
│  1.43    1.07  -0.3590  -25.05%   733  coq-category-theory/Construction/Comma/Adjunction.v.html                                         │
│  16.2    15.8  -0.3380   -2.09%   632  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html          │
│  22.2    21.9  -0.3318   -1.50%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                        │
│  37.4    37.1  -0.3317   -0.89%   276  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html                                       │
│ 0.395  0.0686  -0.3266  -82.64%   373  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                   │
│  31.7    31.4  -0.3211   -1.01%   198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

gares · 2026-05-04T13:02:04Z

Removing the cache seems ok to me.

At the same time the disable_summary API for RocqIDE seems very ugly. IMO it is better to remove from RocqIDE the "printing options" and have the user write Set Pring bla in the text. Or properly implement these printing options passing them functionally to the code, but that is clearly a lot of work for a very simple feature, IMO.

The root state was bugged in a way countered by a cache bug: - init_core / register_root_state would save the initial state, with Flags.quiet = false - init_extra would set Flags.quiet := true - restore_root_state would think the cache is still valid and so not touch Flags.quiet (NB: Flags.quiet is in the summary as goption "Silent") If we remove the cache (or invalidate after setting Flags.quiet) restore_root_state would restore Flags.quiet := false. Instead of trying to change the init flow to stop setting Flags.quiet between register and restore, we just remove the root state and the first saved state is the one saved by new_doc. This means there is no way to return to before new_doc, so STM can't handle more than 1 doc. AFAICT this is fine (in particular compile mode rejects multiple .v arguments, rocqide starts 1 idetop per document).

Otherwise setting the state to execute a command will overwrite the IDE options. (it works in master because of some unsound cache handling)

Knowing when to call invalidate is tricky so if bench agrees it's better to remove this.

SkySkimmer requested review from a team as code owners April 29, 2026 11:15

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2026

SkySkimmer requested a review from a team as a code owner April 29, 2026 11:15

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 29, 2026

ppedrot self-assigned this Apr 29, 2026

SkySkimmer added needs: overlay This is breaking external developments we track in CI. part: functional scheme The Functional Scheme vernac command. and removed part: functional scheme The Functional Scheme vernac command. labels Apr 30, 2026

SkySkimmer added 2 commits May 5, 2026 17:55

Disable summary for options set through XML in idetop

5d58c19

Otherwise setting the state to execute a command will overwrite the IDE options. (it works in master because of some unsound cache handling)

SkySkimmer added a commit to SkySkimmer/vsrocq that referenced this pull request May 5, 2026

Adapt to rocq-prover/rocq#21975 (rm vernacstate cache)

ef8fb2e

SkySkimmer added needs: progress Work in progress: awaiting action from the author. request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels May 5, 2026

SkySkimmer added a commit to SkySkimmer/rocq-lsp that referenced this pull request May 5, 2026

Adapt to rocq-prover/rocq#21975 (removed vernacstate cache)

affb07f

Remove vernacstate cache

203131d

Knowing when to call invalidate is tricky so if bench agrees it's better to remove this.

SkySkimmer force-pushed the no-cache branch from 9893ece to 203131d Compare May 5, 2026 16:07

coqbot-app Bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 5, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Remove vernacstate cache#21975

Remove vernacstate cache#21975
SkySkimmer wants to merge 3 commits into
rocq-prover:masterfrom
SkySkimmer:no-cache

SkySkimmer commented Apr 29, 2026 •

edited

Loading

Uh oh!

SkySkimmer commented Apr 29, 2026

Uh oh!

SkySkimmer commented Apr 29, 2026

Uh oh!

coqbot-app Bot commented Apr 29, 2026

Uh oh!

gares commented May 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

SkySkimmer commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

SkySkimmer commented Apr 29, 2026

Uh oh!

SkySkimmer commented Apr 29, 2026

Uh oh!

coqbot-app Bot commented Apr 29, 2026

Uh oh!

gares commented May 4, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

SkySkimmer commented Apr 29, 2026 •

edited

Loading