Using same refolding strategy for named cofixpoints in tactic "simpl" as is done for named fixpoints #18576

herbelin · 2024-01-28T10:47:56Z

We mostly reuse for named cofixpoints the code existing to refold named fixpoints.

Fixes #4056 and makes simpl's behavior more uniform and a bit closer to cbn.

The 5 first commit are code restructuration (no change of semantics in principle). The 6th is a shortcut in the code. Only the last commit changes the behavior wrt cofixpoints refolding.

Added / updated test-suite.
Added changelog.

Note: I'm considering eventually introducing refolding also in lazy and cbv.

SkySkimmer · 2024-01-28T11:30:50Z

@coqbot bench

coqbot-app · 2024-01-28T23:19: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-neural-net-interp-computed-lite │  300.85   307.59  -2.19 │  1374486193705   1404422868764  -2.13 │  3423838853936   3423802630510   0.00 │ 1115332  1114948   0.03 │
│                    coq-math-classes │   87.37    88.47  -1.24 │   393963208823    396584324966  -0.66 │   554212801496    554189633868   0.00 │  510764   510952  -0.04 │
│                          coq-stdlib │  368.17   370.97  -0.75 │  1560463001762   1568819994613  -0.53 │  1358308850562   1357737953087   0.04 │  737460   735664   0.24 │
│                         coq-unimath │ 1901.52  1915.28  -0.72 │  8646576635561   8710778590217  -0.74 │ 16726446008373  16844896788770  -0.70 │ 1305320  1304948   0.03 │
│                        coq-coqprime │   47.74    48.02  -0.58 │   215243457301    215540728598  -0.14 │   331003583465    330920326282   0.03 │  792276   791952   0.04 │
│                   coq-iris-examples │  463.28   465.91  -0.56 │  2106260333369   2117660195146  -0.54 │  3244663963766   3245813073801  -0.04 │ 1098124  1106168  -0.73 │
│                            coq-corn │  784.91   788.46  -0.45 │  3567163522647   3581941121863  -0.41 │  5480288930277   5503476680315  -0.42 │  839668   815668   2.94 │
│                    coq-fiat-parsers │  307.78   308.84  -0.34 │  1373339800381   1376772867104  -0.25 │  2411484543946   2411338406059   0.01 │ 3049876  3050696  -0.03 │
│                        coq-compcert │  279.29   280.19  -0.32 │  1264209267340   1266699144035  -0.20 │  1934934864772   1934074524264   0.04 │ 1134704  1136400  -0.15 │
│                           coq-color │  234.91   235.50  -0.25 │  1055724669124   1057569973090  -0.17 │  1562007397154   1561429122236   0.04 │ 1222444  1222536  -0.01 │
│                           coq-verdi │   49.12    49.19  -0.14 │   221368203249    221479329472  -0.05 │   342044661943    341876940463   0.05 │  535612   532148   0.65 │
│                         coq-bignums │   29.73    29.74  -0.03 │   134376450313    134653556545  -0.21 │   192764127333    193069992255  -0.16 │  484756   486604  -0.38 │
│             coq-metacoq-safechecker │  415.79   415.82  -0.01 │  1903462808066   1903661749542  -0.01 │  3182877269598   3175255792656   0.24 │ 1884400  1892372  -0.42 │
│                         coq-coqutil │   41.14    41.12   0.05 │   181436058551    182422437599  -0.54 │   264070232754    264060787336   0.00 │  567928   567808   0.02 │
│                                 coq │  749.35   748.87   0.06 │  3159278306439   3158762179825   0.02 │  5652432426132   5653796452225  -0.02 │ 2426732  2426288   0.02 │
│                      coq-verdi-raft │  580.37   579.84   0.09 │  2639939776688   2638401867372   0.06 │  4160375041073   4156875858486   0.08 │  868624   869856  -0.14 │
│                        coq-bedrock2 │  388.42   388.03   0.10 │  1771074745150   1769508988171   0.09 │  3430901997412   3432315235158  -0.04 │  960524   960380   0.01 │
│        coq-fiat-crypto-with-bedrock │ 5858.18  5851.11   0.12 │ 26685684474421  26651644770456   0.13 │ 48411677312867  48388868168933   0.05 │ 3246156  3246188  -0.00 │
│                        coq-rewriter │  403.04   402.44   0.15 │  1833393097732   1829325461311   0.22 │  2989758827508   2989209413447   0.02 │ 1493232  1497580  -0.29 │
│                            coq-hott │  152.39   152.13   0.17 │   680141622551    678914134498   0.18 │  1071913909775   1070473800039   0.13 │  530124   528620   0.28 │
│                coq-metacoq-template │  147.86   147.54   0.22 │   656086610086    656024555104   0.01 │  1024883932967   1025041515107  -0.02 │ 1148348  1153220  -0.42 │
│          coq-performance-tests-lite │  701.86   700.29   0.22 │  3171490361329   3163009113950   0.27 │  5583292726679   5581992927332   0.02 │ 1751168  1754864  -0.21 │
│                            coq-core │  127.45   127.12   0.26 │   484491910693    482328436364   0.45 │   521387332277    521254189812   0.03 │  435684   435852  -0.04 │
│                 coq-category-theory │  762.43   760.11   0.31 │  3471231370735   3460563909103   0.31 │  5776992894669   5783585047594  -0.11 │  988472   988556  -0.01 │
│                             coq-vst │  858.48   855.83   0.31 │  3903440092974   3892807869281   0.27 │  6563122860615   6561416989005   0.03 │ 2461808  2457792   0.16 │
│               coq-engine-bench-lite │  157.23   156.59   0.41 │   667597344512    663727878182   0.58 │  1219504584279   1216964800498   0.21 │ 1263720  1263436   0.02 │
│                 coq-metacoq-erasure │  502.70   500.43   0.45 │  2295026549434   2283276046509   0.51 │  3576705391765   3575362149513   0.04 │ 1826680  1834816  -0.44 │
│         coq-rewriter-perf-SuperFast │  796.00   791.49   0.57 │  3618262907806   3598762480979   0.54 │  6192426334766   6192568857542  -0.00 │ 1598168  1597676   0.03 │
│                   coq-metacoq-pcuic │  786.60   781.09   0.71 │  3586758439339   3561303086176   0.71 │  5339732221280   5338214155525   0.03 │ 2382348  2371764   0.45 │
│            coq-metacoq-translations │   16.92    16.80   0.71 │    75331033450     74926103715   0.54 │   124049595643    124072909535  -0.02 │  859008   860092  -0.13 │
│                       coq-fiat-core │   59.33    58.76   0.97 │   246899283024    245014558085   0.77 │   365645329784    365552147426   0.03 │  482080   482120  -0.01 │
│                       coq-equations │    7.84     7.72   1.55 │    32209212986     32183543761   0.08 │    52090476594     52090860667  -0.00 │  387016   387116  -0.03 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-mathcomp-ssreflect (dependency install failed in NEW)

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-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                                                                           │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  19.8430   22.2420  2.3990  12.09%  2061  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│ 130.0910  131.5430  1.4520   1.12%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                           │
│   3.8720    4.9930  1.1210  28.95%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                           │
│  62.7070   63.7060  0.9990   1.59%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html    │
│ 152.0810  152.8290  0.7480   0.49%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                    │
│   2.6630    3.3800  0.7170  26.92%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                           │
│ 100.8470  101.5190  0.6720   0.67%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                      │
│  66.3810   67.0500  0.6690   1.01%  1629  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                                                  │
│  67.4300   68.0910  0.6610   0.98%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                         │
│  44.0330   44.6780  0.6450   1.46%   827  coq-vst/veric/binop_lemmas4.v.html                                                               │
│  77.9750   78.5450  0.5700   0.73%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                          │
│  22.5500   23.0820  0.5320   2.36%   595  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                    │
│   0.9930    1.3990  0.4060  40.89%   853  coq-stdlib/FSets/FMapAVL.v.html                                                                  │
│  95.2090   95.5920  0.3830   0.40%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│   3.9210    4.2860  0.3650   9.31%     8  coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html                                  │
│  37.4010   37.7580  0.3570   0.95%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html            │
│  18.0920   18.4180  0.3260   1.80%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                        │
│  32.8950   33.2130  0.3180   0.97%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│  17.8690   18.1790  0.3100   1.73%  3158  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                              │
│  94.1100   94.3930  0.2830   0.30%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                              │
│  14.9400   15.2170  0.2770   1.85%  3090  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                              │
│   0.6100    0.8810  0.2710  44.43%   816  coq-stdlib/MSets/MSetRBT.v.html                                                                  │
│  95.3800   95.6420  0.2620   0.27%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│   9.2110    9.4580  0.2470   2.68%   183  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.v.html    │
│   8.5880    8.8320  0.2440   2.84%    27  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v.html                    │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                   TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                      │
│   OLD       NEW      DIFF     %DIFF     Ln                      FILE                                                                                 │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  10.4470    0.9790  -9.4680   -90.63%   603  coq-unimath/UniMath/Algebra/GroupAction.v.html                                                          │
│ 267.1490  260.4370  -6.7120    -2.51%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│ 182.0740  178.4420  -3.6320    -1.99%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  34.0850   33.3800  -0.7050    -2.07%   839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                           │
│  27.4540   26.9370  -0.5170    -1.88%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html      │
│  36.6820   36.2340  -0.4480    -1.22%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│   0.4220    0.0150  -0.4070   -96.45%   259  coq-unimath/UniMath/CategoryTheory/Subobjects.v.html                                                    │
│   4.7230    4.3530  -0.3700    -7.83%   733  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
│   0.5400    0.1820  -0.3580   -66.30%    90  coq-unimath/UniMath/Semantics/LinearLogic/LiftingModel.v.html                                           │
│   2.7850    2.4300  -0.3550   -12.75%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                              │
│   1.0980    0.7700  -0.3280   -29.87%   384  coq-stdlib/MSets/MSetAVL.v.html                                                                         │
│  13.8900   13.5870  -0.3030    -2.18%   216  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│   0.3130    0.0360  -0.2770   -88.50%   290  coq-unimath/UniMath/Algebra/Archimedean.v.html                                                          │
│  17.3350   17.0700  -0.2650    -1.53%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                       │
│  13.1330   12.8680  -0.2650    -2.02%  1028  coq-unimath/UniMath/CategoryTheory/LocalizingClass.v.html                                               │
│   0.5570    0.3140  -0.2430   -43.63%   868  coq-stdlib/MSets/MSetRBT.v.html                                                                         │
│   0.6070    0.3820  -0.2250   -37.07%  2108  coq-stdlib/FSets/FMapFacts.v.html                                                                       │
│   0.7450    0.5220  -0.2230   -29.93%   590  coq-stdlib/Strings/Byte.v.html                                                                          │
│  10.3750   10.1570  -0.2180    -2.10%   304  coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html                                             │
│   0.2890    0.0720  -0.2170   -75.09%   250  coq-metacoq-safechecker/safechecker/theories/PCUICSafeRetyping.v.html                                   │
│   0.2170    0.0010  -0.2160   -99.54%   430  coq-metacoq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v.html                                   │
│  41.1570   40.9440  -0.2130    -0.52%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│   0.2120    0.0000  -0.2120  -100.00%   374  coq-metacoq-erasure/erasure/theories/EGenericGlobalMap.v.html                                           │
│   0.2070    0.0000  -0.2070  -100.00%   360  coq-metacoq-pcuic/pcuic/theories/Bidirectional/BDFromPCUIC.v.html                                       │
│   0.2180    0.0120  -0.2060   -94.50%   303  coq-metacoq-pcuic/pcuic/theories/PCUICEtaExpand.v.html                                                  │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

herbelin · 2024-01-29T08:06:19Z

CI green at this stage (except coq_library_undecidability and http as in other PRs).

ppedrot · 2024-01-29T12:18:48Z

pretyping/reductionops.mli

@@ -58,7 +58,8 @@ module Stack : sig

  val pr_app_node : (EConstr.t -> Pp.t) -> app_node -> Pp.t

-  type case_stk
+  type case_stk =
+    case_info * EInstance.t * EConstr.t array * EConstr.t pcase_return * EConstr.t pcase_invert * EConstr.t pcase_branch array


It seems you only build values of this type. If that's the case (no pun intended) don't expose the type definition but a builder function instead.

It is the case... Done

You didn't hide the type though.

Lol, looks like I was a bit absent-minded. Done

Because the argument of a Case cannot be a lambda.

At the same time, we start putting an architecture to nest the recursive calls "simpl", so that it can (eventually!) be configured to work like "cbn", as in: Definition pred_add x y := pred (x+y). Eval simpl in pred_add 3 4. (* Currently unreduced *) Eval cbn in pred_add 3 4. (* 6 *) Definition add_succ x y := (x+y) + 1. Eval simpl in add_succ 3 4. (* Currently unreduced *) Eval cbn in pred_add 3 4. (* 8 *)

We mostly reuse the code existing to refold fixpoints.

ppedrot · 2024-02-04T17:18:19Z

@coqbot run full ci

ppedrot · 2024-02-07T11:09:21Z

pretyping/tacred.ml

    reversible constants, eventually refolding to the initial constant
    for unary fixpoints and to the last constant encapsulating the Fix
    for mutual fixpoints *)

-let compute_consteval ((cache,_),allowed_reds as cache_reds) env sigma ref u =


I think we should introduce a proper record for reduction caches.

Eventually yes. I could do it as soon as this PR if you insist, or, maybe, simpler to me, at the time of rebasing PR #18580 which also adds a new component.

ppedrot · 2024-02-07T14:25:08Z

@coqbot merge now

coqbot-app · 2024-02-07T14:25:10Z

@ppedrot: You can't merge the PR because it hasn't been approved yet.

ppedrot · 2024-02-07T14:25:29Z

@coqbot merge now

herbelin added part: tactics kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. part: reduction strategies The Strategy command for defining reduction straegies. request: full CI Use this label when you want your next push to trigger a full CI. labels Jan 28, 2024

herbelin added this to the 8.20+rc1 milestone Jan 28, 2024

coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Jan 28, 2024

herbelin mentioned this pull request Jan 28, 2024

Fixes #7982: add support for reduction of primitive projection of cofixpoints in "simpl" reduction strategy #18577

Merged

2 tasks

herbelin mentioned this pull request Jan 28, 2024

Take "simpl never" into account for "simpl" in position of argument of a "match", "fix" or projection #18581

Open

2 tasks

herbelin marked this pull request as ready for review January 29, 2024 07:38

herbelin requested a review from a team as a code owner January 29, 2024 07:38

herbelin mentioned this pull request Jan 29, 2024

inconsistent results with simpl, cofix, and section variables #4056

Closed

herbelin added a commit to herbelin/github-coq that referenced this pull request Jan 29, 2024

Adding change log for coq#18576

b0824ed

herbelin requested review from a team as code owners January 29, 2024 08:06

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 Jan 29, 2024

herbelin added a commit to herbelin/github-coq that referenced this pull request Jan 29, 2024

Adding change log for coq#18576

b3961e7

herbelin force-pushed the master+fix4056-refolding-simpl-cofix branch from b0824ed to b3961e7 Compare January 29, 2024 11:30

ppedrot reviewed Jan 29, 2024

View reviewed changes

herbelin added 2 commits January 29, 2024 19:23

Slight improve of code regularity in "simpl" tactic.

ef34c9f

Robustness of pattern-matching in evaluable_reference_eq.

51f5f81

herbelin added a commit to herbelin/github-coq that referenced this pull request Jan 29, 2024

Adding change log for coq#18576

2f6c5d9

herbelin force-pushed the master+fix4056-refolding-simpl-cofix branch from b3961e7 to 2f6c5d9 Compare January 29, 2024 18:24

herbelin added 5 commits January 30, 2024 11:56

Export a builder for the Stack.Case argument.

c715039

A useless "when" clause in "simpl" tactic.

9fc2f4c

Because the argument of a Case cannot be a lambda.

Mini-improvement code locality in "simpl".

9fc66b5

Fixing coq#4056: add refolding of named cofixpoints in tactic "simpl".

c728193

We mostly reuse the code existing to refold fixpoints.

Adding change log for coq#18576

a90fcef

herbelin force-pushed the master+fix4056-refolding-simpl-cofix branch from 2f6c5d9 to a90fcef Compare January 30, 2024 11:00

ppedrot self-assigned this Jan 30, 2024

herbelin mentioned this pull request Jan 30, 2024

Refolding "simpl never" constants hiding fixpoints in position of argument of a destructor in tactic "simpl" #18591

Open

2 tasks

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 Feb 4, 2024

herbelin mentioned this pull request Feb 5, 2024

Take into account the local delta flags for "simpl" #18621

Open

3 tasks

ppedrot reviewed Feb 7, 2024

View reviewed changes

ppedrot approved these changes Feb 7, 2024

View reviewed changes

coqbot-app bot merged commit 7d678e4 into coq:master Feb 7, 2024
5 of 6 checks passed

louiseddp pushed a commit to louiseddp/coq that referenced this pull request Feb 27, 2024

Adding change log for coq#18576

62e3756

SkySkimmer mentioned this pull request Feb 28, 2024

bench master NEW=2024-02-27 OLD=2024-01-25 #18724

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Using same refolding strategy for named cofixpoints in tactic "simpl" as is done for named fixpoints #18576

Using same refolding strategy for named cofixpoints in tactic "simpl" as is done for named fixpoints #18576

herbelin commented Jan 28, 2024 •

edited

SkySkimmer commented Jan 28, 2024

coqbot-app bot commented Jan 28, 2024

herbelin commented Jan 29, 2024

ppedrot Jan 29, 2024

herbelin Jan 29, 2024

ppedrot Jan 30, 2024

herbelin Jan 30, 2024

ppedrot commented Feb 4, 2024

ppedrot Feb 7, 2024

herbelin Feb 7, 2024

ppedrot commented Feb 7, 2024

coqbot-app bot commented Feb 7, 2024

ppedrot commented Feb 7, 2024

Using same refolding strategy for named cofixpoints in tactic "simpl" as is done for named fixpoints #18576

Using same refolding strategy for named cofixpoints in tactic "simpl" as is done for named fixpoints #18576

Conversation

herbelin commented Jan 28, 2024 • edited

SkySkimmer commented Jan 28, 2024

coqbot-app bot commented Jan 28, 2024

herbelin commented Jan 29, 2024

ppedrot Jan 29, 2024

Choose a reason for hiding this comment

herbelin Jan 29, 2024

Choose a reason for hiding this comment

ppedrot Jan 30, 2024

Choose a reason for hiding this comment

herbelin Jan 30, 2024

Choose a reason for hiding this comment

ppedrot commented Feb 4, 2024

ppedrot Feb 7, 2024

Choose a reason for hiding this comment

herbelin Feb 7, 2024

Choose a reason for hiding this comment

ppedrot commented Feb 7, 2024

coqbot-app bot commented Feb 7, 2024

ppedrot commented Feb 7, 2024

herbelin commented Jan 28, 2024 •

edited