Separate unsynchronized and synchronized grammar states in procq

[SkySkimmer]

The unsynchronized part is shared over the whole process, but in
principle we could have multiple synchronized parsing states (eg with
multicore, or a more functional style summary)

[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 │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│                            coq-core │    2.85     2.91  -2.06 │    19730503279     19687897219   0.22 │  106484   106340   0.14 │
│                           coq-verdi │   42.45    42.82  -0.86 │   284518265719    283852611516   0.23 │  536952   524596   2.36 │
│                         coq-coqutil │   45.97    46.25  -0.61 │   287461016612    286381345192   0.38 │  560860   560528   0.06 │
│                       coq-fiat-core │   54.43    54.76  -0.60 │   333311736975    331650537887   0.50 │  480076   481252  -0.24 │
│                         rocq-stdlib │  443.34   445.18  -0.41 │  1538426969138   1534516094207   0.25 │  625552   632840  -1.15 │
│                        coq-compcert │  298.40   299.07  -0.22 │  1955049817464   1950017827764   0.26 │ 1181832  1294152  -8.68 │
│                        coq-bedrock2 │  350.26   351.04  -0.22 │  2911027735451   2908124634881   0.10 │  837500   822976   1.76 │
│          coq-performance-tests-lite │  903.61   905.27  -0.18 │  7263589216344   7259253387635   0.06 │ 2000016  2203960  -9.25 │
│                        rocq-bignums │   24.74    24.77  -0.12 │   157409547326    156877569591   0.34 │  455676   456244  -0.12 │
│               coq-engine-bench-lite │  128.31   128.45  -0.11 │   949286360598    949715295604  -0.05 │ 1062180  1084168  -2.03 │
│                    coq-math-classes │   82.95    82.98  -0.04 │   502893308832    501377720176   0.30 │  520968   515888   0.98 │
│                             coq-vst │  827.59   827.75  -0.02 │  6278963130573   6274797836487   0.07 │ 2165400  2173608  -0.38 │
│         coq-rewriter-perf-SuperFast │  480.37   480.31   0.01 │  3729857906161   3727605666705   0.06 │ 1279400  1254404   1.99 │
│                           coq-color │  228.65   228.58   0.03 │  1449332298503   1445458669737   0.27 │ 1120448  1134748  -1.26 │
│        coq-fiat-crypto-with-bedrock │ 7190.37  7183.07   0.10 │ 59523688588991  59492380288331   0.05 │ 3191132  3169080   0.70 │
│ coq-neural-net-interp-computed-lite │  236.90   236.62   0.12 │  2263281445938   2263214540252   0.00 │  914176   878812   4.02 │
│                         coq-unimath │ 1784.23  1780.94   0.18 │ 14807048751322  14796267702140   0.07 │ 1070376  1095168  -2.26 │
│                      coq-verdi-raft │  495.19   494.10   0.22 │  3418185432930   3416355231344   0.05 │  825588   819296   0.77 │
│                        coq-rewriter │  331.61   330.83   0.24 │  2475271392413   2475018619235   0.01 │ 1440824  1505408  -4.29 │
│                   coq-iris-examples │  365.31   364.16   0.32 │  2407158781176   2400707812987   0.27 │ 1131472  1129120   0.21 │
│                            coq-hott │  158.54   157.86   0.43 │  1094022181428   1088956045702   0.47 │  462836   471212  -1.78 │
│                    coq-fiat-parsers │  275.30   273.98   0.48 │  2111962367317   2105811320600   0.29 │ 2148496  2348168  -8.50 │
│                        rocq-runtime │   74.17    73.79   0.51 │   536844159247    536948903993  -0.02 │  510080   508772   0.26 │
│                           rocq-core │    6.74     6.70   0.60 │    41357077302     41022385969   0.82 │  456936   455100   0.40 │
│                        coq-coqprime │   52.89    52.25   1.22 │   358329367460    357632569576   0.19 │  819800   820308  -0.06 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
rocq-elpi (dependency install failed in NEW)
rocq-equations (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)
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-coquelicot (dependency rocq-elpi failed)
coq-fourcolor (dependency rocq-elpi failed)
coq-category-theory (dependency rocq-equations failed)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                             │
│  OLD    NEW    DIFF    %DIFF   Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  82.2   83.4  1.2698    1.55%   48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  1.36   2.54  1.1795   86.69%  549  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                           │
│   236    237  0.9202    0.39%  141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  2.48   3.31  0.8298   33.43%   34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  3.86   4.59  0.7278   18.85%  128  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│ 0.287  0.892  0.6051  210.73%   12  rocq-stdlib/theories/MSets/MSets.v.html                                                                 │
│  1.90   2.47  0.5673   29.83%   32  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│   133    134  0.5229    0.39%  155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│   201    202  0.5216    0.26%    8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│  26.2   26.7  0.4986    1.90%   62  coq-fiat-crypto-with-bedrock/src/Assembly/Parse/TestAsm.v.html                                          │
│  21.5   21.9  0.4755    2.22%   49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  19.8   20.3  0.4727    2.39%  708  coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html                                            │
│  64.4   64.9  0.4491    0.70%  716  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                                   │
│   173    174  0.4325    0.25%  233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  18.6   18.9  0.3278    1.76%   77  coq-fiat-crypto-with-bedrock/src/Assembly/Parse/TestAsm.v.html                                          │
│ 0.260  0.554  0.2946  113.48%   19  rocq-stdlib/theories/FSets/FSetFacts.v.html                                                             │
│  20.8   21.0  0.2851    1.37%   23  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/Arith.v.html                                           │
│  26.4   26.7  0.2758    1.05%  374  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                             │
│ 0.270  0.544  0.2744  101.79%   12  rocq-stdlib/theories/ZArith/Znumtheory.v.html                                                           │
│ 0.163  0.428  0.2652  162.67%  596  rocq-stdlib/theories/Strings/Byte.v.html                                                                │
│  1.15   1.41  0.2621   22.79%  207  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                                      │
│  26.4   26.6  0.2611    0.99%  375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                             │
│ 0.278  0.537  0.2590   93.06%   11  rocq-stdlib/theories/Strings/HexString.v.html                                                           │
│  34.4   34.6  0.2525    0.73%  174  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                           │
│  18.7   18.9  0.2524    1.35%   31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                               │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SPEED UPS                                                              │
│                                                                                                                                            │
│  OLD     NEW     DIFF     %DIFF    Ln                     FILE                                                                             │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   64.7    63.6  -1.0715   -1.66%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                        │
│   95.5    94.5  -0.9190   -0.96%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│    118     118  -0.8925   -0.75%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                             │
│   93.2    92.5  -0.7328   -0.79%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                        │
│   95.3    94.6  -0.6894   -0.72%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│   45.6    45.0  -0.5781   -1.27%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                │
│   3.85    3.32  -0.5228  -13.60%   557  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                      │
│   2.05    1.53  -0.5221  -25.43%   313  rocq-stdlib/theories/Strings/Byte.v.html                                                           │
│   27.5    27.0  -0.5029   -1.83%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │
│   3.21    2.71  -0.4988  -15.54%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                          │
│  0.895   0.474  -0.4208  -47.03%   249  rocq-stdlib/theories/Structures/OrdersEx.v.html                                                    │
│   43.3    42.9  -0.3742   -0.86%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                            │
│   30.6    30.3  -0.3256   -1.06%   225  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                       │
│  0.568   0.248  -0.3192  -56.23%     1  rocq-stdlib/theories/micromega/ZifyPow.v.html                                                      │
│  0.551   0.242  -0.3098  -56.19%    11  rocq-stdlib/theories/Strings/OctalString.v.html                                                    │
│  0.576   0.270  -0.3053  -53.03%    36  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                          │
│ 32.279  31.983  -0.2960   -0.92%    97  coq-vst/veric/binop_lemmas5.v.html                                                                 │
│  0.467   0.172  -0.2944  -63.10%    13  rocq-stdlib/theories/micromega/ZCoeff.v.html                                                       │
│  0.594   0.303  -0.2913  -49.00%    17  rocq-stdlib/theories/Logic/IndefiniteDescription.v.html                                            │
│   2.76    2.47  -0.2812  -10.20%  1001  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│  0.615   0.339  -0.2758  -44.83%  1161  rocq-stdlib/theories/Strings/Byte.v.html                                                           │
│   8.19    7.92  -0.2709   -3.31%  1831  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html   │
│  0.492   0.228  -0.2643  -53.68%    14  rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html                                               │
│  0.504   0.241  -0.2631  -52.17%    11  rocq-stdlib/theories/ZArith/Zminmax.v.html                                                         │
│   14.1    13.8  -0.2567   -1.82%   216  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                           │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job