[core] Improved state protection against memprof-limits interruptions by ejgallego · Pull Request #19177 · rocq-prover/rocq

ejgallego · 2024-06-07T16:27:30Z

This is a proof-of-concept (based on #19175), but could be merged as
is.

It should fix a few bugs we had when interrupting Coq:

Pcoq.unfreeze caused grammar state to go wrong (in a non
recoverable way)
Interrupting module dynlink was also leaving the system in a bad
state.

It is hard to review the codebase for potential problems like this.

ejgallego · 2024-06-07T17:12:47Z

I can still corrupt the parser state with this (on the other hand, interrupting the initial requires seems to behave much better).

I'll try to figure out next week what's missing (likely we need to protect some of the code that was added for 8.17 to enable backtracking of grammars?)

edit: protecting the summaries made my test-suite pass (in ultra interruption mode), tho I found a couple of anomalies (which can be recovered) "memprof limits, token is set"

But that is very good news.

ejgallego · 2024-06-10T19:22:31Z

Marking this 8.20 ; it is non-controversial IMHO, and would be a pity for UI users to have to keep patching Coq in order to get reliable interruptions.

gadmm · 2024-06-10T20:33:29Z

It is hard to review the codebase for potential problems like this.

With memprof-limits, the code to be audited for problems like this should first be strictly delineated by the memprof-limits tasks (e.g. one only need to look at the functions passed as arguments to the memprof-limits limits).

Then, those functions:

should be rewritten to avoid global state, i.e. non local to the task (by passing shared state as argument to/closure members of the task if necessary),
the arguments/closure members should be of types whose interface is designed to be interrupt-safe---all interrupt-unsafe functions in the interface should be replaced by interrupt-safe ones.

Note that local state (i.e. local to the task) is fine (e.g. no need to rewrite the whole program to pass state around).

Keeping global state can technically work but it makes things much more difficult for the monitor to keep track that nothing unwind-unsafe escapes.

Was it hard to locate all the global state used by the interruptible functions? Do you have a methodical way to do so?
How realistic is the idea to keep track of all shared state at the level of monitors, by avoiding global state inside tasks?

I had a quick glance at the changes and those are the questions that came to mind.

proux01 · 2024-06-17T08:17:35Z

Still draft, postponing.

SkySkimmer · 2024-06-17T16:04:04Z

@coqbot bench

ejgallego · 2024-06-17T16:45:56Z

@coqbot bench

Maybe I should rebase and re-run?

SkySkimmer · 2024-06-17T17:02:32Z

bench seems to be running fine, no need to do it on rebase

ejgallego · 2024-06-17T17:04:59Z

lib/util.mli

   Credit X.Leroy, D.Remy. *)
 val try_finally: ('a -> 'b) -> 'a -> ('c -> unit) -> 'c -> 'b

+val protect_ref : scope:(unit -> 'a) -> 'b ref -> 'a


Have a new version that documents all this, will upload after the bench completes.

no need to wait

👍

Ok, will do tomorrow. If we decide to ship this in 8.20 (hopefully) it shouldn't be too much of a PITA as it doesn't need overlays.

I mainly wanna be sure the version I push passes all my testing, which takes a little bit.

ejgallego · 2024-06-17T17:24:58Z

With memprof-limits, the code to be audited for problems like this should first be strictly delineated by the memprof-limits tasks (e.g. one only need to look at the functions passed as arguments to the memprof-limits limits).

Thanks @gadmm , indeed in coq-lsp we run under memprof-limits code that is below vernac, similarly to the approach you mentioned of handling Coq tasks as user processers.

Then, those functions:

should be rewritten to avoid global state, i.e. non local to the task (by passing shared state as argument to/closure members of the task if necessary),

Yes! I proposed this in 2019 as a key UI task, however it was deemed too costly I guess (never got an answer to my proposal tho), however this is still a critical point, for example it is not possible to use Coq printer from another domain without doing pretty complex (and fragile) tricks. In #10041 we did a large effort to at least separate the proof state.

Still, the biggest obstacle is Coq's use of camlp5 parsing engine, which is pretty hard to functionalize.

Keeping global state can technically work but it makes things much more difficult for the monitor to keep track that nothing unwind-unsafe escapes.

That's the situation now, fortunately most global state is encapsulated in the summary (not all tho, quite a few offenders actually), so we can either protect the summary (will likely do for 8.20 if not performance impact), or just try to research bad summary unfreeze functions. Most of the state is just setting a ref, so it can be recovered easily.

Was it hard to locate all the global state used by the interruptible functions? Do you have a methodical way to do so?

It was indeed quite tricky, but I develop a bit of improved infra in coq-lsp as to properly handle these problems. Once I was able to load large developments in the LSP server, it was surprisingly easy to trigger races!

How realistic is the idea to keep track of all shared state at the level of monitors, by avoiding global state inside tasks?

This is in a sense what we do, but we have stuff like dynload and camlp5 which are not easy (or just impossible) to functionalize, but what you propose is likely what we will end up adopting, unless we find performance problems.

Do you expect masking to introduce performance problems ? As of today we typically mask once per-sentence (tho this is not the case exactly in coq-lsp, need to tweak some parts that may unfreeze the state twice)

I had a quick glance at the changes and those are the questions that came to mind.

Thanks a lot for all your help, I find the scope resource style much much better than what we had before with try ... with -> ... ; reraise exn

ejgallego · 2024-06-17T17:25:28Z

@gadmm actually could you have a look at the new function here Util.atomify? Is that the right way to do that? TIA!

coqbot-app · 2024-06-18T02:13:31Z

🏁 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-fiat-core │   55.95    57.07  -1.96 │   233057340099    237129080217  -1.72 │   344327174455    344268452224   0.02 │  471608   468748   0.61 │
│                           coq-verdi │   48.30    49.01  -1.45 │   217220539693    220118175164  -1.32 │   337016955888    336867936493   0.04 │  526464   527584  -0.21 │
│                         coq-coqutil │   42.40    43.01  -1.42 │   187254557153    189552651797  -1.21 │   268825842180    268744081189   0.03 │  662736   662580   0.02 │
│                    coq-math-classes │   86.01    86.93  -1.06 │   386219995570    392147199046  -1.51 │   535389508705    535424194687  -0.01 │  502024   501780   0.05 │
│                            coq-hott │  164.07   165.48  -0.85 │   734008345529    738619582640  -0.62 │  1162407378243   1162025645482   0.03 │  472588   470540   0.44 │
│                      coq-verdi-raft │  577.46   582.09  -0.80 │  2628017748632   2647504434679  -0.74 │  4117712058995   4117229341250   0.01 │  828372   829000  -0.08 │
│                           coq-color │  248.19   249.94  -0.70 │  1115664379167   1123863262615  -0.73 │  1598053808617   1597491683865   0.04 │ 1128576  1128736  -0.01 │
│                         coq-bignums │   29.24    29.44  -0.68 │   133454896531    133399951312   0.04 │   190579801243    190541119801   0.02 │  471180   471344  -0.03 │
│                        coq-coqprime │   47.92    48.22  -0.62 │   215768129627    216821923277  -0.49 │   329597242875    329550107511   0.01 │  774988   774968   0.00 │
│                    coq-fiat-parsers │  297.35   299.17  -0.61 │  1327576287641   1334814453463  -0.54 │  2332755797835   2332455371230   0.01 │ 2373016  2374068  -0.04 │
│        coq-fiat-crypto-with-bedrock │ 5696.98  5728.90  -0.56 │ 25940149447052  26085495142722  -0.56 │ 46582097644977  46580025408988   0.00 │ 3246116  3246072   0.00 │
│                         coq-unimath │ 2571.08  2584.17  -0.51 │ 11713023724007  11770676563572  -0.49 │ 23134180765787  23133590260188   0.00 │ 1309776  1307720   0.16 │
│ coq-neural-net-interp-computed-lite │  240.31   241.26  -0.39 │  1096965861716   1101249086048  -0.39 │  2306941067502   2306883809987   0.00 │  786164   785884   0.04 │
│                        coq-compcert │  275.21   276.25  -0.38 │  1244723240363   1248672079619  -0.32 │  1882186899356   1881867275348   0.02 │ 1056672  1055644   0.10 │
│          coq-performance-tests-lite │  883.41   886.21  -0.32 │  4002011020144   4015513640992  -0.34 │  7218365096722   7219172872299  -0.01 │ 2181700  2182036  -0.02 │
│         coq-rewriter-perf-SuperFast │  783.12   785.49  -0.30 │  3560709713988   3569355914874  -0.24 │  6188611522186   6188085891568   0.01 │ 1588292  1590868  -0.16 │
│                            coq-corn │  709.63   711.04  -0.20 │  3226936740980   3230876199735  -0.12 │  4996870259332   4995642480057   0.02 │  757344   748504   1.18 │
│                 coq-category-theory │  660.81   661.43  -0.09 │  3003724931482   3008870093836  -0.17 │  4906191493390   4906047854340   0.00 │  967272   991768  -2.47 │
│               coq-engine-bench-lite │  156.22   156.21   0.01 │   661832751619    662929890733  -0.17 │  1216075673366   1219152770636  -0.25 │  945524   945224   0.03 │
│                          coq-stdlib │  346.36   346.30   0.02 │  1477317482436   1472099561524   0.35 │  1245733577332   1245306196872   0.03 │  702192   709220  -0.99 │
│                   coq-iris-examples │  467.65   467.26   0.08 │  2126034296598   2125512663261   0.02 │  3248556301656   3248310412207   0.01 │ 1129320  1132988  -0.32 │
│                        coq-rewriter │  388.04   387.60   0.11 │  1764476616306   1762418584152   0.12 │  2928330646297   2928759252213  -0.01 │ 1477276  1477340  -0.00 │
│                       coq-equations │   11.79    11.77   0.17 │    49171774996     49637030926  -0.94 │    77426294394     77454792387  -0.04 │  418304   420288  -0.47 │
│                        coq-bedrock2 │  364.68   364.03   0.18 │  1662247484426   1658923722970   0.20 │  3101471289304   3102137211145  -0.02 │  841320   841908  -0.07 │
│                            coq-core │  128.82   128.40   0.33 │   505275560220    502836073674   0.49 │   532814625794    532351163082   0.09 │  461792   458356   0.75 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-mathcomp-ssreflect (dependency install failed in NEW)
coq-metacoq-template (dependency install failed in NEW)
coq-metacoq-pcuic (dependency install failed in NEW)
coq-vst

coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-algebra (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-solvable (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-field (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-character (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-odd-order (dependency coq-mathcomp-ssreflect failed)
coq-metacoq-safechecker (dependency coq-metacoq-pcuic failed)
coq-metacoq-erasure (dependency coq-metacoq-template failed)
coq-metacoq-translations (dependency coq-metacoq-template failed)
coq-coquelicot (dependency coq-mathcomp-ssreflect failed)
coq-fourcolor (dependency coq-mathcomp-ssreflect failed)

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                             │
│   OLD       NEW      DIFF   %DIFF    Ln                     FILE                                                                            │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  15.9710   17.0410  1.0700   6.70%   828  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                           │
│  46.2340   46.9080  0.6740   1.46%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                        │
│   3.0280    3.5990  0.5710  18.86%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                        │
│  36.8190   37.3740  0.5550   1.51%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                  │
│   2.3590    2.9000  0.5410  22.93%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                                        │
│  46.0350   46.4730  0.4380   0.95%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html      │
│  23.7870   24.1820  0.3950   1.66%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                           │
│  33.9310   34.3120  0.3810   1.12%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html  │
│  49.0880   49.4610  0.3730   0.76%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│  12.2040   12.5710  0.3670   3.01%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                          │
│ 235.3730  235.7380  0.3650   0.16%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                        │
│  25.9730   26.3200  0.3470   1.34%   129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                             │
│  17.7160   18.0470  0.3310   1.87%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                         │
│   4.5790    4.9090  0.3300   7.21%   195  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                        │
│  28.7510   29.0790  0.3280   1.14%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html                │
│  38.3650   38.6840  0.3190   0.83%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                    │
│  18.1780   18.4810  0.3030   1.67%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                 │
│   1.6480    1.9440  0.2960  17.96%   196  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                          │
│  17.4650   17.7490  0.2840   1.63%    32  coq-performance-tests-lite/src/pattern.v.html                                                     │
│  21.3340   21.6080  0.2740   1.28%   376  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.v.html     │
│   3.1610    3.4080  0.2470   7.81%  4023  coq-unimath/UniMath/HomologicalAlgebra/MappingCone.v.html                                         │
│   0.6740    0.9180  0.2440  36.20%   813  coq-stdlib/MSets/MSetRBT.v.html                                                                   │
│  39.3320   39.5600  0.2280   0.58%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html         │
│  36.5080   36.7330  0.2250   0.62%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                      │
│   0.5190    0.7300  0.2110  40.66%   190  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                          │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                     │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                                 │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 183.3420  181.7810  -1.5610   -0.85%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  97.3660   96.1030  -1.2630   -1.30%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  97.2700   96.0440  -1.2260   -1.26%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│   4.9820    3.8100  -1.1720  -23.52%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│ 200.4350  199.3530  -1.0820   -0.54%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│  66.7690   65.7000  -1.0690   -1.60%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│ 154.4540  153.4930  -0.9610   -0.62%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│  64.0040   63.1830  -0.8210   -1.28%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│   3.3680    2.6090  -0.7590  -22.54%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  37.8190   37.1370  -0.6820   -1.80%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                        │
│  29.3340   28.7000  -0.6340   -2.16%    32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  18.6300   18.0940  -0.5360   -2.88%   708  coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html                                            │
│  46.7560   46.2380  -0.5180   -1.11%   926  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│  17.3850   16.9010  -0.4840   -2.78%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MulSplit.v.html                                        │
│  13.1400   12.6700  -0.4700   -3.58%  1555  coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html                                             │
│  25.7580   25.3270  -0.4310   -1.67%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                                   │
│  27.3110   26.8850  -0.4260   -1.56%    35  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  13.3730   12.9930  -0.3800   -2.84%  1028  coq-unimath/UniMath/CategoryTheory/LocalizingClass.v.html                                               │
│  26.2330   25.8560  -0.3770   -1.44%   345  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                                      │
│  21.4570   21.0970  -0.3600   -1.68%   213  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                        │
│  15.3070   14.9560  -0.3510   -2.29%  1382  coq-rewriter/src/Rewriter/Language/Wf.v.html                                                            │
│  19.8700   19.5250  -0.3450   -1.74%  1286  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│  13.2850   12.9520  -0.3330   -2.51%    17  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  13.2280   12.9070  -0.3210   -2.43%    22  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  39.9480   39.6310  -0.3170   -0.79%   835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

ejgallego · 2024-06-18T09:49:53Z

@SkySkimmer indeed bench found some trouble, will rebase and re-run.

ejgallego · 2024-06-18T11:45:00Z

@coqbot bench

coqbot-app · 2024-06-19T00:57:36Z

🏁 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-bedrock2 │  363.93   365.75  -0.50 │  1642457798286   1649555931173  -0.43 │  3109283286389   3109157888935   0.00 │  891704   890604   0.12 │
│                 coq-metacoq-erasure │  539.47   541.74  -0.42 │  2443726397599   2452871363233  -0.37 │  3842354939190   3842533906610  -0.00 │ 1947120  1946080   0.05 │
│             coq-metacoq-safechecker │  409.25   410.81  -0.38 │  1864823324816   1872478951927  -0.41 │  3100060464157   3100675660835  -0.02 │ 2050656  2044508   0.30 │
│               coq-mathcomp-fingroup │   31.01    31.11  -0.32 │   140794626172    141370031464  -0.41 │   212302438333    212276891206   0.01 │  561684   562540  -0.15 │
│                   coq-metacoq-pcuic │  731.32   732.21  -0.12 │  3305410014328   3307150127206  -0.05 │  4906377847513   4904644232562   0.04 │ 3226696  3228708  -0.06 │
│                      coq-coquelicot │   38.90    38.92  -0.05 │   171980657688    172490535513  -0.30 │   242097848741    241988616446   0.05 │  780928   780216   0.09 │
│                coq-metacoq-template │  153.25   153.24   0.01 │   675723791376    675536914433   0.03 │  1065009534782   1064951056393   0.01 │ 1260492  1260280   0.02 │
│                coq-mathcomp-algebra │  207.58   207.56   0.01 │   940057008447    940499690052  -0.05 │  1479065903540   1479246865631  -0.01 │ 1293180  1276916   1.27 │
│                    coq-fiat-parsers │  302.68   302.54   0.05 │  1338498726384   1337088660386   0.11 │  2362466227949   2361433082177   0.04 │ 2631960  2611880   0.77 │
│                            coq-core │  130.39   130.32   0.05 │   499114148294    500305298051  -0.24 │   533069334521    532943780047   0.02 │  457620   457172   0.10 │
│                       coq-fourcolor │ 1395.70  1394.64   0.08 │  6349189826572   6347694020174   0.02 │ 12802591468150  12802457458802   0.00 │  833320   831324   0.24 │
│               coq-engine-bench-lite │  154.65   154.53   0.08 │   649526622179    647970575068   0.24 │  1208610937657   1208814265410  -0.02 │ 1059256  1059164   0.01 │
│ coq-neural-net-interp-computed-lite │  241.49   241.23   0.11 │  1100429972625   1098193475747   0.20 │  2311178950582   2310501720334   0.03 │  831132   831900  -0.09 │
│                        coq-compcert │  280.31   279.97   0.12 │  1260169722586   1257628987118   0.20 │  1919770549837   1919669664587   0.01 │ 1103772  1102780   0.09 │
│                   coq-iris-examples │  467.04   466.35   0.15 │  2113580512713   2109460697078   0.20 │  3268706475417   3268804274772  -0.00 │ 1082732  1079148   0.33 │
│        coq-fiat-crypto-with-bedrock │ 5734.02  5724.45   0.17 │ 25951274700440  25888861114201   0.24 │ 46715356627313  46709565363805   0.01 │ 3245972  3246128  -0.00 │
│                         coq-coqutil │   42.83    42.72   0.26 │   188068620006    187699262306   0.20 │   271802485800    271707266609   0.04 │  681584   680944   0.09 │
│                        coq-rewriter │  390.98   389.97   0.26 │  1762219948896   1757019662468   0.30 │  2945068249877   2945511348028  -0.02 │ 1504292  1504844  -0.04 │
│          coq-performance-tests-lite │  889.90   887.52   0.27 │  4004019823015   3991541375197   0.31 │  7244278991982   7246821457739  -0.04 │ 2444712  2444796  -0.00 │
│                          coq-stdlib │  362.03   361.03   0.28 │  1515700555951   1514341525953   0.09 │  1275673602059   1275522772168   0.01 │  708636   709776  -0.16 │
│                       coq-fiat-core │   57.30    57.12   0.32 │   235923277306    234477904392   0.62 │   351508609516    351129457925   0.11 │  471804   469208   0.55 │
│                            coq-corn │  721.69   719.27   0.34 │  3262470215546   3253581561845   0.27 │  5095134169865   5093074507188   0.04 │  725192   729060  -0.53 │
│                            coq-hott │  162.08   161.53   0.34 │   716782132204    715693886312   0.15 │  1146293764506   1146033392679   0.02 │  464148   466492  -0.50 │
│              coq-mathcomp-odd-order │  682.54   679.84   0.40 │  3111874987462   3099660400485   0.39 │  4873414036566   4877455031443  -0.08 │ 1619464  1603860   0.97 │
│                  coq-mathcomp-field │  132.60   131.98   0.47 │   600827811956    597648057719   0.53 │   967882828160    968329565398  -0.05 │ 1278012  1277716   0.02 │
│                         coq-bignums │   29.65    29.51   0.47 │   134112431104    133354522631   0.57 │   193061140245    193042329747   0.01 │  471252   471204   0.01 │
│                           coq-color │  252.29   251.06   0.49 │  1125769131979   1121293745140   0.40 │  1627959695970   1628381819184  -0.03 │ 1211208  1215536  -0.36 │
│                    coq-math-classes │   87.08    86.57   0.59 │   388595174043    387143925202   0.37 │   543754974607    543742680056   0.00 │  503992   503852   0.03 │
│               coq-mathcomp-solvable │  122.46   121.73   0.60 │   557492735207    554530169911   0.53 │   887568608502    886676811289   0.10 │  864252   866384  -0.25 │
│         coq-rewriter-perf-SuperFast │  799.77   794.87   0.62 │  3572232874146   3548713191056   0.66 │  6215143443068   6213345794222   0.03 │ 1603568  1606468  -0.18 │
│                 coq-category-theory │  652.24   648.19   0.62 │  2950409711855   2933280441813   0.58 │  4855718190552   4848460768350   0.15 │  983284   980188   0.32 │
│                         coq-unimath │ 2589.16  2569.99   0.75 │ 11740785826383  11647228982448   0.80 │ 23167781468705  23172379343771  -0.02 │ 1316044  1327780  -0.88 │
│                        coq-coqprime │   48.71    48.31   0.83 │   216514338472    215317468296   0.56 │   334536562438    334412794597   0.04 │  777052   774756   0.30 │
│              coq-mathcomp-ssreflect │  174.50   172.99   0.87 │   788311987119    781753143183   0.84 │  1165310963722   1165512334026  -0.02 │ 1680328  1657696   1.37 │
│                      coq-verdi-raft │  583.36   577.48   1.02 │  2647048013702   2620131013574   1.03 │  4159207379408   4157942019292   0.03 │  831476   835272  -0.45 │
│                           coq-verdi │   49.63    49.03   1.22 │   222260546630    219954047661   1.05 │   343452202559    343391646907   0.02 │  525348   528416  -0.58 │
│              coq-mathcomp-character │  111.87   110.18   1.53 │   508421388271    501011468846   1.48 │   804499864279    804412499809   0.01 │ 1062748  1060420   0.22 │
│                       coq-equations │   11.88    11.67   1.80 │    49149398586     48934569298   0.44 │    77861861878     77875431846  -0.02 │  416360   415752   0.15 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-metacoq-translations
coq-vst

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                 TOP 25 SLOW DOWNS                                                                 │
│                                                                                                                                                   │
│   OLD       NEW      DIFF   %DIFF    Ln                      FILE                                                                                 │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 179.9630  183.9870  4.0240   2.24%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│ 153.1760  154.9030  1.7270   1.13%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│  95.4980   96.9140  1.4160   1.48%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  95.8020   97.0070  1.2050   1.26%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  12.9020   13.8560  0.9540   7.39%  2103  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                                  │
│  46.8500   47.7930  0.9430   2.01%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                              │
│  38.7790   39.6610  0.8820   2.27%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                          │
│  72.4970   73.3500  0.8530   1.18%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                                    │
│   3.1460    3.9660  0.8200  26.06%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  17.8180   18.5520  0.7340   4.12%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                       │
│   1.7030    2.3200  0.6170  36.23%   196  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                                │
│  46.7990   47.4160  0.6170   1.32%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html            │
│   4.2620    4.8610  0.5990  14.05%  4414  coq-unimath/UniMath/HomologicalAlgebra/MappingCone.v.html                                               │
│  46.7980   47.3380  0.5400   1.15%   926  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│  33.8610   34.3290  0.4680   1.38%   839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│ 235.6780  236.1150  0.4370   0.19%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  10.5280   10.9400  0.4120   3.91%  2089  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                                  │
│   4.3840    4.7830  0.3990   9.10%   733  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
│  18.7440   19.1300  0.3860   2.06%     6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.v.html   │
│  21.9890   22.3710  0.3820   1.74%   587  coq-unimath/UniMath/AlgebraicTheories/RepresentationTheorem.v.html                                      │
│  10.0340   10.4130  0.3790   3.78%   768  coq-unimath/UniMath/CategoryTheory/Actegories/ConstructionOfActegoryMorphisms.v.html                    │
│  31.0150   31.3660  0.3510   1.13%    12  coq-fourcolor/theories/job254to270.v.html                                                               │
│   9.8140   10.1570  0.3430   3.50%   496  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html                                             │
│   3.7460    4.0860  0.3400   9.08%   275  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
│   3.9450    4.2780  0.3330   8.44%   240  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SPEED UPS                                                                │
│                                                                                                                                               │
│   OLD       NEW      DIFF     %DIFF    Ln                     FILE                                                                            │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  64.5770   62.3090  -2.2680   -3.51%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                       │
│  35.0560   33.3320  -1.7240   -4.92%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html  │
│  37.8920   36.4020  -1.4900   -3.93%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                  │
│  50.4070   49.0890  -1.3180   -2.61%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                   │
│  50.4860   49.3670  -1.1190   -2.22%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│  27.2340   26.6430  -0.5910   -2.17%    12  coq-fourcolor/theories/job190to206.v.html                                                         │
│ 132.5390  131.9570  -0.5820   -0.44%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                            │
│   4.3100    3.7660  -0.5440  -12.62%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                        │
│  39.0050   38.5680  -0.4370   -1.12%   338  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                       │
│  37.8760   37.4450  -0.4310   -1.14%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html             │
│   7.6990    7.3020  -0.3970   -5.16%   602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html    │
│  25.3980   25.0010  -0.3970   -1.56%    12  coq-fourcolor/theories/job227to230.v.html                                                         │
│  36.5030   36.1290  -0.3740   -1.02%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                      │
│  28.9930   28.6690  -0.3240   -1.12%   144  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                      │
│ 103.2940  102.9710  -0.3230   -0.31%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                       │
│   1.4490    1.1320  -0.3170  -21.88%   854  coq-stdlib/FSets/FMapAVL.v.html                                                                   │
│  27.3790   27.0630  -0.3160   -1.15%   147  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                      │
│  96.9840   96.6780  -0.3060   -0.32%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                       │
│   3.2580    2.9690  -0.2890   -8.87%  3222  coq-metacoq-pcuic/pcuic/theories/PCUICConfluence.v.html                                           │
│   2.6610    2.3790  -0.2820  -10.60%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                                        │
│  83.1720   82.8920  -0.2800   -0.34%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                           │
│  33.0780   32.8020  -0.2760   -0.83%    12  coq-fourcolor/theories/job439to465.v.html                                                         │
│  29.8040   29.5280  -0.2760   -0.93%    79  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │
│  23.8300   23.5640  -0.2660   -1.12%    12  coq-fourcolor/theories/job295to298.v.html                                                         │
│   2.7470    2.4890  -0.2580   -9.39%   698  coq-category-theory/Construction/Comma/Adjunction.v.html                                          │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

ejgallego · 2024-06-19T08:08:16Z

IMHO noise / no-effect (we should actually have a different metric that %, as for equations 11 seconds runtime, 2% is not significative)

@SkySkimmer how would it best to go ahead with this? Depending PR is IMHO ready, this one too but I cannot undraft it until we merge the other one.

ppedrot · 2024-06-24T13:30:06Z

@ejgallego you should probably rebase and undraft quickly if you want this in 8.20.

ejgallego · 2024-06-24T15:16:25Z

@ejgallego you should probably rebase and undraft quickly if you want this in 8.20.

Yes, when is the deadline? Running the test suite for this unfortunately not trivial.

@ejgallego

CHANGES: ------------------------ - [fleche] fix quick fixes for errors being lost due to incorrect handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850) - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872) - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#879) - [js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo Heuzard for longstanding continued support of the jsCoq and coq-lsp projects (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Fix build for Coq -> Rocq renaming and stdlib split (@ejgallego, rocq-community/rocq-lsp#881) - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer, rocq-community/rocq-lsp#883) - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890) - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890) - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815, rocq-community/rocq-lsp#890) - [petanque] `petanque/start` now fails when the theorem was parsed but not successfully executed (@ejgallego, reported by @gbdrt, rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886) - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904) - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly reduces the Stack Overflow in the proof engine (@ejgallego, @corwin-of-amber, rocq-community/rocq-lsp#905) - [js worker] [build] Include Coq WaterProof in the default Web Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888) - [vscode] [web] Fix web extension not exporting the coq-lsp extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes rocq-community/rocq-lsp#877) - [build] [general] Rename our internal `Lsp` library to `Fleche_lsp`; this should help avoiding conflicts with the OCaml `lsp` library (@ejgallego, reported by @blackbird1128, rocq-community/rocq-lsp#912, fixes rocq-community/rocq-lsp#861) - [workspace] Remove support legacy ML-search path semantics. These were basically unused since Coq 8.16. As a consequence, `coq-lsp` / `fcc` don't accept the `-I` flag anymore, use `OCAMLPATH` or the `--ocamlpath=` option to pass extra `findlib` paths. We still respect the -I flag in `_CoqMakefile` (@ejgallego, rocq-community/rocq-lsp#916) - [lsp] [debug] Respect `$/setTrace` call , refactor logging system, and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919, fixes rocq-community/rocq-lsp#868) - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#891) - [ci] [deps] Remove support for OCaml 4.12 and 4.13, following upstream's rocq-prover/rocq#20576 Note that these compiler versions have been unsupported for a long time, please upgrade (@ejgallego, rocq-community/rocq-lsp#951) - [hover] New option `show_state_hash_on_hover` that displays state hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954) - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023, thanks to Patrick Nicodemus for pointing out the outdated documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817) - [vscode] [macos] Resolve keybinding conflict with Cmd+N and Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei Listochkin, rocq-community/rocq-lsp#926) - [rocq] [fleche] Disable memprof-limits interruption backend by default, as released Rocq versions are not safe yet. If you want to enable it, you can still do it with the `--int_backend=Mp` command line option (@ejgallego, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#857, reported by @dariusf, cc: rocq-prover/rocq#19177) - [lsp] [controller] Include Rocq feedback on request errors, using the optional `data` field. This is useful to still be able to obtain feedback messages such as debug messages even when a request fails. This also opens the door to better protocol handling and petanque integration (@ejgallego, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#961) - [petanque] Add feedback field to `Run_result.t`, this is important for many use cases. We also return feedback on petanque errors. (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#960) - [petanque] new `get_state_at_pos` and `get_root_state` calls, that allow to retrieve a petanque proof state from position (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962) - [doc] [petanque] Document petanque v1, improve readme (@ejgallego, rocq-community/rocq-lsp#963) - [plugin] [astdump] Make the JSON and SEXP output into a line per object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874) - [doc] [emacs] [protocol] Improve documentation for `proof/goals`, add link to official emacs mode by Josselin Poiret (@ejgallego, rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941) - [goals] Include `range` in `proof/goals` answer. This is useful for clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)

SkySkimmer · 2025-06-06T12:19:06Z

I'm planning to branch 9.1 next week, it would be nice if this could be finished before that.

@ejgallego

CHANGES: ------------------------ - [fleche] fix quick fixes for errors being lost due to incorrect handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850) - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872) - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#879) - [js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo Heuzard for longstanding continued support of the jsCoq and coq-lsp projects (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Fix build for Coq -> Rocq renaming and stdlib split (@ejgallego, rocq-community/rocq-lsp#881) - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer, rocq-community/rocq-lsp#883) - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890) - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890) - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815, rocq-community/rocq-lsp#890) - [petanque] `petanque/start` now fails when the theorem was parsed but not successfully executed (@ejgallego, reported by @gbdrt, rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886) - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904) - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly reduces the Stack Overflow in the proof engine (@ejgallego, @corwin-of-amber, rocq-community/rocq-lsp#905) - [js worker] [build] Include Coq WaterProof in the default Web Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888) - [vscode] [web] Fix web extension not exporting the coq-lsp extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes rocq-community/rocq-lsp#877) - [build] [general] Rename our internal `Lsp` library to `Fleche_lsp`; this should help avoiding conflicts with the OCaml `lsp` library (@ejgallego, reported by @blackbird1128, rocq-community/rocq-lsp#912, fixes rocq-community/rocq-lsp#861) - [workspace] Remove support legacy ML-search path semantics. These were basically unused since Coq 8.16. As a consequence, `coq-lsp` / `fcc` don't accept the `-I` flag anymore, use `OCAMLPATH` or the `--ocamlpath=` option to pass extra `findlib` paths. We still respect the -I flag in `_CoqMakefile` (@ejgallego, rocq-community/rocq-lsp#916) - [lsp] [debug] Respect `$/setTrace` call , refactor logging system, and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919, fixes rocq-community/rocq-lsp#868) - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#891) - [ci] [deps] Remove support for OCaml 4.12 and 4.13, following upstream's rocq-prover/rocq#20576 Note that these compiler versions have been unsupported for a long time, please upgrade (@ejgallego, rocq-community/rocq-lsp#951) - [hover] New option `show_state_hash_on_hover` that displays state hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954) - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023, thanks to Patrick Nicodemus for pointing out the outdated documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817) - [vscode] [macos] Resolve keybinding conflict with Cmd+N and Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei Listochkin, rocq-community/rocq-lsp#926) - [rocq] [fleche] Disable memprof-limits interruption backend by default, as released Rocq versions are not safe yet. If you want to enable it, you can still do it with the `--int_backend=Mp` command line option (@ejgallego, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#857, reported by @dariusf, cc: rocq-prover/rocq#19177) - [lsp] [controller] Include Rocq feedback on request errors, using the optional `data` field. This is useful to still be able to obtain feedback messages such as debug messages even when a request fails. This also opens the door to better protocol handling and petanque integration (@ejgallego, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#961) - [petanque] Add feedback field to `Run_result.t`, this is important for many use cases. We also return feedback on petanque errors. (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#960) - [petanque] new `get_state_at_pos` and `get_root_state` calls, that allow to retrieve a petanque proof state from position (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962) - [doc] [petanque] Document petanque v1, improve readme (@ejgallego, rocq-community/rocq-lsp#963) - [plugin] [astdump] Make the JSON and SEXP output into a line per object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874) - [doc] [emacs] [protocol] Improve documentation for `proof/goals`, add link to official emacs mode by Josselin Poiret (@ejgallego, rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941) - [goals] Include `range` in `proof/goals` answer. This is useful for clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)

@ejgallego

CHANGES: ------------------------ - [fleche] fix quick fixes for errors being lost due to incorrect handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850) - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872) - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#879) - [js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo Heuzard for longstanding continued support of the jsCoq and coq-lsp projects (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Fix build for Coq -> Rocq renaming and stdlib split (@ejgallego, rocq-community/rocq-lsp#881) - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer, rocq-community/rocq-lsp#883) - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890) - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890) - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815, rocq-community/rocq-lsp#890) - [petanque] `petanque/start` now fails when the theorem was parsed but not successfully executed (@ejgallego, reported by @gbdrt, rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886) - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904) - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly reduces the Stack Overflow in the proof engine (@ejgallego, @corwin-of-amber, rocq-community/rocq-lsp#905) - [js worker] [build] Include Coq WaterProof in the default Web Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888) - [vscode] [web] Fix web extension not exporting the coq-lsp extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes rocq-community/rocq-lsp#877) - [build] [general] Rename our internal `Lsp` library to `Fleche_lsp`; this should help avoiding conflicts with the OCaml `lsp` library (@ejgallego, reported by @blackbird1128, rocq-community/rocq-lsp#912, fixes rocq-community/rocq-lsp#861) - [workspace] Remove support legacy ML-search path semantics. These were basically unused since Coq 8.16. As a consequence, `coq-lsp` / `fcc` don't accept the `-I` flag anymore, use `OCAMLPATH` or the `--ocamlpath=` option to pass extra `findlib` paths. We still respect the -I flag in `_CoqMakefile` (@ejgallego, rocq-community/rocq-lsp#916) - [lsp] [debug] Respect `$/setTrace` call , refactor logging system, and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919, fixes rocq-community/rocq-lsp#868) - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#891) - [ci] [deps] Remove support for OCaml 4.12 and 4.13, following upstream's rocq-prover/rocq#20576 Note that these compiler versions have been unsupported for a long time, please upgrade (@ejgallego, rocq-community/rocq-lsp#951) - [hover] New option `show_state_hash_on_hover` that displays state hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954) - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023, thanks to Patrick Nicodemus for pointing out the outdated documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817) - [vscode] [macos] Resolve keybinding conflict with Cmd+N and Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei Listochkin, rocq-community/rocq-lsp#926) - [rocq] [fleche] Disable memprof-limits interruption backend by default, as released Rocq versions are not safe yet. If you want to enable it, you can still do it with the `--int_backend=Mp` command line option (@ejgallego, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#857, reported by @dariusf, cc: rocq-prover/rocq#19177) - [lsp] [controller] Include Rocq feedback on request errors, using the optional `data` field. This is useful to still be able to obtain feedback messages such as debug messages even when a request fails. This also opens the door to better protocol handling and petanque integration (@ejgallego, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#961) - [petanque] Add feedback field to `Run_result.t`, this is important for many use cases. We also return feedback on petanque errors. (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#960) - [petanque] new `get_state_at_pos` and `get_root_state` calls, that allow to retrieve a petanque proof state from position (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962) - [doc] [petanque] Document petanque v1, improve readme (@ejgallego, rocq-community/rocq-lsp#963) - [plugin] [astdump] Make the JSON and SEXP output into a line per object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874) - [doc] [emacs] [protocol] Improve documentation for `proof/goals`, add link to official emacs mode by Josselin Poiret (@ejgallego, rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941) - [goals] Include `range` in `proof/goals` answer. This is useful for clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)

@ejgallego

CHANGES: ------------------------ - [fleche] fix quick fixes for errors being lost due to incorrect handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850) - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872) - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#879) - [js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo Heuzard for longstanding continued support of the jsCoq and coq-lsp projects (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Fix build for Coq -> Rocq renaming and stdlib split (@ejgallego, rocq-community/rocq-lsp#881) - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer, rocq-community/rocq-lsp#883) - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890) - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890) - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815, rocq-community/rocq-lsp#890) - [petanque] `petanque/start` now fails when the theorem was parsed but not successfully executed (@ejgallego, reported by @gbdrt, rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886) - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904) - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly reduces the Stack Overflow in the proof engine (@ejgallego, @corwin-of-amber, rocq-community/rocq-lsp#905) - [js worker] [build] Include Coq WaterProof in the default Web Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888) - [vscode] [web] Fix web extension not exporting the coq-lsp extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes rocq-community/rocq-lsp#877) - [build] [general] Rename our internal `Lsp` library to `Fleche_lsp`; this should help avoiding conflicts with the OCaml `lsp` library (@ejgallego, reported by @blackbird1128, rocq-community/rocq-lsp#912, fixes rocq-community/rocq-lsp#861) - [workspace] Remove support legacy ML-search path semantics. These were basically unused since Coq 8.16. As a consequence, `coq-lsp` / `fcc` don't accept the `-I` flag anymore, use `OCAMLPATH` or the `--ocamlpath=` option to pass extra `findlib` paths. We still respect the -I flag in `_CoqMakefile` (@ejgallego, rocq-community/rocq-lsp#916) - [lsp] [debug] Respect `$/setTrace` call , refactor logging system, and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919, fixes rocq-community/rocq-lsp#868) - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#891) - [ci] [deps] Remove support for OCaml 4.12 and 4.13, following upstream's rocq-prover/rocq#20576 Note that these compiler versions have been unsupported for a long time, please upgrade (@ejgallego, rocq-community/rocq-lsp#951) - [hover] New option `show_state_hash_on_hover` that displays state hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954) - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023, thanks to Patrick Nicodemus for pointing out the outdated documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817) - [vscode] [macos] Resolve keybinding conflict with Cmd+N and Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei Listochkin, rocq-community/rocq-lsp#926) - [rocq] [fleche] Disable memprof-limits interruption backend by default, as released Rocq versions are not safe yet. If you want to enable it, you can still do it with the `--int_backend=Mp` command line option (@ejgallego, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#857, reported by @dariusf, cc: rocq-prover/rocq#19177) - [lsp] [controller] Include Rocq feedback on request errors, using the optional `data` field. This is useful to still be able to obtain feedback messages such as debug messages even when a request fails. This also opens the door to better protocol handling and petanque integration (@ejgallego, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#961) - [petanque] Add feedback field to `Run_result.t`, this is important for many use cases. We also return feedback on petanque errors. (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#960) - [petanque] new `get_state_at_pos` and `get_root_state` calls, that allow to retrieve a petanque proof state from position (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962) - [doc] [petanque] Document petanque v1, improve readme (@ejgallego, rocq-community/rocq-lsp#963) - [plugin] [astdump] Make the JSON and SEXP output into a line per object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874) - [doc] [emacs] [protocol] Improve documentation for `proof/goals`, add link to official emacs mode by Josselin Poiret (@ejgallego, rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941) - [goals] Include `range` in `proof/goals` answer. This is useful for clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)

@ejgallego

CHANGES: ------------------------ - [fleche] fix quick fixes for errors being lost due to incorrect handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850) - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872) - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#879) - [js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo Heuzard for longstanding continued support of the jsCoq and coq-lsp projects (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Fix build for Coq -> Rocq renaming and stdlib split (@ejgallego, rocq-community/rocq-lsp#881) - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer, rocq-community/rocq-lsp#883) - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890) - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890) - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815, rocq-community/rocq-lsp#890) - [petanque] `petanque/start` now fails when the theorem was parsed but not successfully executed (@ejgallego, reported by @gbdrt, rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886) - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904) - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly reduces the Stack Overflow in the proof engine (@ejgallego, @corwin-of-amber, rocq-community/rocq-lsp#905) - [js worker] [build] Include Coq WaterProof in the default Web Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888) - [vscode] [web] Fix web extension not exporting the coq-lsp extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes rocq-community/rocq-lsp#877) - [build] [general] Rename our internal `Lsp` library to `Fleche_lsp`; this should help avoiding conflicts with the OCaml `lsp` library (@ejgallego, reported by @blackbird1128, rocq-community/rocq-lsp#912, fixes rocq-community/rocq-lsp#861) - [workspace] Remove support legacy ML-search path semantics. These were basically unused since Coq 8.16. As a consequence, `coq-lsp` / `fcc` don't accept the `-I` flag anymore, use `OCAMLPATH` or the `--ocamlpath=` option to pass extra `findlib` paths. We still respect the -I flag in `_CoqMakefile` (@ejgallego, rocq-community/rocq-lsp#916) - [lsp] [debug] Respect `$/setTrace` call , refactor logging system, and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919, fixes rocq-community/rocq-lsp#868) - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#891) - [ci] [deps] Remove support for OCaml 4.12 and 4.13, following upstream's rocq-prover/rocq#20576 Note that these compiler versions have been unsupported for a long time, please upgrade (@ejgallego, rocq-community/rocq-lsp#951) - [hover] New option `show_state_hash_on_hover` that displays state hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954) - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023, thanks to Patrick Nicodemus for pointing out the outdated documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817) - [vscode] [macos] Resolve keybinding conflict with Cmd+N and Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei Listochkin, rocq-community/rocq-lsp#926) - [rocq] [fleche] Disable memprof-limits interruption backend by default, as released Rocq versions are not safe yet. If you want to enable it, you can still do it with the `--int_backend=Mp` command line option (@ejgallego, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#857, reported by @dariusf, cc: rocq-prover/rocq#19177) - [lsp] [controller] Include Rocq feedback on request errors, using the optional `data` field. This is useful to still be able to obtain feedback messages such as debug messages even when a request fails. This also opens the door to better protocol handling and petanque integration (@ejgallego, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#961) - [petanque] Add feedback field to `Run_result.t`, this is important for many use cases. We also return feedback on petanque errors. (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#960) - [petanque] new `get_state_at_pos` and `get_root_state` calls, that allow to retrieve a petanque proof state from position (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962) - [doc] [petanque] Document petanque v1, improve readme (@ejgallego, rocq-community/rocq-lsp#963) - [plugin] [astdump] Make the JSON and SEXP output into a line per object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874) - [doc] [emacs] [protocol] Improve documentation for `proof/goals`, add link to official emacs mode by Josselin Poiret (@ejgallego, rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941) - [goals] Include `range` in `proof/goals` answer. This is useful for clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)

@ejgallego

CHANGES: ------------------------ - [fleche] fix quick fixes for errors being lost due to incorrect handling of `send_diags_extra_data` (@ejgallego, rocq-community/rocq-lsp#850) - [vscode] Syntax highlighting for Coq 8.17-8.20 (@4ever2, rocq-community/rocq-lsp#872) - [build] Adapt to Coq -> Rocq renaming (@ejgallego, @proux, rocq-community/rocq-lsp#879) - [js worker] Update js_of_ocaml to 5.9.1 , thanks a lot to Hugo Heuzard for longstanding continued support of the jsCoq and coq-lsp projects (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Update stubs (@ejgallego, @hhugo, rocq-community/rocq-lsp#881) - [js worker] Fix build for Coq -> Rocq renaming and stdlib split (@ejgallego, rocq-community/rocq-lsp#881) - [general] Adapt to Coq -> Rocq renaming (@ejgallego, @SkySkimmer, rocq-community/rocq-lsp#883) - [general] [js] Adapt to Rocq stdlib split (@ejgallego, rocq-community/rocq-lsp#890) - [ci] Bump setup-ocaml to v3 (@ejgallego, rocq-community/rocq-lsp#890) - [ci] [windows] Use Opam 2.2 to build on windows (@ejgallego, rocq-community/rocq-lsp#815, rocq-community/rocq-lsp#890) - [petanque] `petanque/start` now fails when the theorem was parsed but not successfully executed (@ejgallego, reported by @gbdrt, rocq-community/rocq-lsp#901, fixes rocq-community/rocq-lsp#886) - [ci] Test Ocaml 5.3 (@ejgallego, rocq-community/rocq-lsp#904) - [js worker] Add Shachar Itzhaky's trampoline patch; this greatly reduces the Stack Overflow in the proof engine (@ejgallego, @corwin-of-amber, rocq-community/rocq-lsp#905) - [js worker] [build] Include Coq WaterProof in the default Web Worker build (@ejgallego, waterproof team, rocq-community/rocq-lsp#905, closes rocq-community/rocq-lsp#888) - [vscode] [web] Fix web extension not exporting the coq-lsp extension API (@ejgallego, reported by @amblafont, rocq-community/rocq-lsp#911, fixes rocq-community/rocq-lsp#877) - [build] [general] Rename our internal `Lsp` library to `Fleche_lsp`; this should help avoiding conflicts with the OCaml `lsp` library (@ejgallego, reported by @blackbird1128, rocq-community/rocq-lsp#912, fixes rocq-community/rocq-lsp#861) - [workspace] Remove support legacy ML-search path semantics. These were basically unused since Coq 8.16. As a consequence, `coq-lsp` / `fcc` don't accept the `-I` flag anymore, use `OCAMLPATH` or the `--ocamlpath=` option to pass extra `findlib` paths. We still respect the -I flag in `_CoqMakefile` (@ejgallego, rocq-community/rocq-lsp#916) - [lsp] [debug] Respect `$/setTrace` call , refactor logging system, and allow file logging of protocol traces again (@ejgallego, rocq-community/rocq-lsp#919, fixes rocq-community/rocq-lsp#868) - [coq] Support Coq relocatable mode (@SkySkimmer, rocq-community/rocq-lsp#891) - [ci] [deps] Remove support for OCaml 4.12 and 4.13, following upstream's rocq-prover/rocq#20576 Note that these compiler versions have been unsupported for a long time, please upgrade (@ejgallego, rocq-community/rocq-lsp#951) - [hover] New option `show_state_hash_on_hover` that displays state hash on hover for debug (@ejgallego, rocq-community/rocq-lsp#954) - [doc] [faq] Updated FAQ to account for VSCoq 2 release in 2023, thanks to Patrick Nicodemus for pointing out the outdated documentation (@ejgallego, rocq-community/rocq-lsp#846, fixes rocq-community/rocq-lsp#817) - [vscode] [macos] Resolve keybinding conflict with Cmd+N and Cmd+Enter, we now use Alt+N and Alt+Shift+Enter, (Andrei Listochkin, rocq-community/rocq-lsp#926) - [rocq] [fleche] Disable memprof-limits interruption backend by default, as released Rocq versions are not safe yet. If you want to enable it, you can still do it with the `--int_backend=Mp` command line option (@ejgallego, rocq-community/rocq-lsp#957, fixes rocq-community/rocq-lsp#857, reported by @dariusf, cc: rocq-prover/rocq#19177) - [lsp] [controller] Include Rocq feedback on request errors, using the optional `data` field. This is useful to still be able to obtain feedback messages such as debug messages even when a request fails. This also opens the door to better protocol handling and petanque integration (@ejgallego, rocq-community/rocq-lsp#959, rocq-community/rocq-lsp#961) - [petanque] Add feedback field to `Run_result.t`, this is important for many use cases. We also return feedback on petanque errors. (@ejgallego, @JulesViennotFranca, rocq-community/rocq-lsp#960) - [petanque] new `get_state_at_pos` and `get_root_state` calls, that allow to retrieve a petanque proof state from position (@JulesViennotFranca, @ejgallego, rocq-community/rocq-lsp#962) - [doc] [petanque] Document petanque v1, improve readme (@ejgallego, rocq-community/rocq-lsp#963) - [plugin] [astdump] Make the JSON and SEXP output into a line per object by default (@blackbird1128, @ejgallego, rocq-community/rocq-lsp#874) - [doc] [emacs] [protocol] Improve documentation for `proof/goals`, add link to official emacs mode by Josselin Poiret (@ejgallego, rocq-community/rocq-lsp#969, thanks to @jpoiret, cc: rocq-community/rocq-lsp#941) - [goals] Include `range` in `proof/goals` answer. This is useful for clients willing to do highlighting (@ejgallego, @jpoiret, rocq-community/rocq-lsp#970)

gadmm · 2025-09-17T16:24:14Z

memprof-limits 0.3.0 with support for OCaml ≥ 5.3 has been released

See discussion in rocq-prover#19177 , indeed, there are some parts of Coq code that set some global imperative flags in a scoped way; this is tricky to get right and maintain, and given the current uses, we should not favor this style but instead make it deprecated. As of today we have 2 kinds of these flags: - printing: IMO it is a priority to make the printer fully functional, which will remove the uses here - debug flags: they should be disabled in production, so shouldn't matter a lot

This is a proof-of-concept (based on rocq-prover#19175), but could be merged as is. It should fix a few bugs we had when interrupting Coq: - `Pcoq.unfreeze` caused grammar state to go wrong (in a non recoverable way) - Interrupting module dynlink was also leaving the system in a bad state. It is hard to review the codebase for potential problems like this.

SkySkimmer · 2025-11-12T19:06:09Z

@coqbot run full ci

SkySkimmer

I'm going to merge this, we can finish whatever remains later.

SkySkimmer · 2025-11-13T16:33:54Z

@coqbot merge now

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 7, 2024

ejgallego force-pushed the mask_try_catch branch from 1146ef1 to 1789c91 Compare June 7, 2024 16:56

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 10, 2024

ejgallego mentioned this pull request Jun 10, 2024

[lib] Add primitives for async-safe resource masking and thread_maps from memprof-limits #19175

Merged

ejgallego added this to the 8.20+rc1 milestone Jun 10, 2024

proux01 modified the milestones: 8.20+rc1, 8.21+rc1 Jun 17, 2024

ejgallego added the kind: fix This fixes a bug or incorrect documentation. label Jun 17, 2024

ejgallego commented Jun 17, 2024

View reviewed changes

ejgallego force-pushed the mask_try_catch branch from 1789c91 to 7419e7e Compare June 18, 2024 11:44

coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 18, 2024

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 19, 2024

ejgallego force-pushed the mask_try_catch branch from 7419e7e to 95627c3 Compare June 24, 2024 15:17

coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Jun 24, 2024

ejgallego mentioned this pull request Jun 4, 2025

[new release] coq-lsp (0.2.3+8.17) ocaml/opam-repository#27993

Merged

ejgallego removed this from the 9.1+rc1 milestone Jun 6, 2025

ejgallego force-pushed the mask_try_catch branch from 5761860 to a41fc98 Compare October 7, 2025 16:21

github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 14, 2025

ejgallego mentioned this pull request Oct 28, 2025

Experiment: command modifier and tactic for allocation limits #17266

Open

ejgallego force-pushed the mask_try_catch branch from a41fc98 to 7f71eb0 Compare October 30, 2025 17:57

coqbot-app bot removed the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Oct 30, 2025

ejgallego force-pushed the mask_try_catch branch from 7f71eb0 to f0345e7 Compare November 4, 2025 14:46

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 12, 2025

SkySkimmer added this to the 9.2+rc1 milestone Nov 12, 2025

SkySkimmer approved these changes Nov 13, 2025

View reviewed changes

SkySkimmer removed needs: progress Work in progress: awaiting action from the author. needs: testing Some manual testing is required. labels Nov 13, 2025

coqbot-app bot merged commit 1138b1d into rocq-prover:master Nov 13, 2025
7 checks passed

github-project-automation bot moved this from Needs review to Done in LSP server Nov 13, 2025

SkySkimmer deleted the mask_try_catch branch November 13, 2025 16:34

SkySkimmer restored the mask_try_catch branch November 13, 2025 16:34

ejgallego deleted the mask_try_catch branch November 13, 2025 16:36

Conversation

ejgallego commented Jun 7, 2024

Uh oh!

ejgallego commented Jun 7, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ejgallego commented Jun 10, 2024

Uh oh!

gadmm commented Jun 10, 2024

Uh oh!

proux01 commented Jun 17, 2024

Uh oh!

SkySkimmer commented Jun 17, 2024

Uh oh!

ejgallego commented Jun 17, 2024

Uh oh!

SkySkimmer commented Jun 17, 2024

Uh oh!

ejgallego Jun 17, 2024

Choose a reason for hiding this comment

Uh oh!

SkySkimmer Jun 17, 2024

Choose a reason for hiding this comment

Uh oh!

ejgallego Jun 17, 2024

Choose a reason for hiding this comment

Uh oh!

ejgallego Jun 17, 2024

Choose a reason for hiding this comment

Uh oh!

ejgallego commented Jun 17, 2024

Uh oh!

ejgallego commented Jun 17, 2024

Uh oh!

coqbot-app bot commented Jun 18, 2024

Uh oh!

ejgallego commented Jun 18, 2024

Uh oh!

ejgallego commented Jun 18, 2024

Uh oh!

coqbot-app bot commented Jun 19, 2024

Uh oh!

ejgallego commented Jun 19, 2024

Uh oh!

ppedrot commented Jun 24, 2024

Uh oh!

ejgallego commented Jun 24, 2024

Uh oh!

SkySkimmer commented Jun 6, 2025

Uh oh!

gadmm commented Sep 17, 2025

Uh oh!

SkySkimmer commented Nov 12, 2025

Uh oh!

SkySkimmer left a comment

Choose a reason for hiding this comment

Uh oh!

SkySkimmer commented Nov 13, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

ejgallego commented Jun 7, 2024 •

edited

Loading