Skip to content

Exit early from conversion in all cases that directly involve evars#21964

Draft
Janno wants to merge 2 commits into
rocq-prover:masterfrom
Janno:janno/conversion-exit-evars
Draft

Exit early from conversion in all cases that directly involve evars#21964
Janno wants to merge 2 commits into
rocq-prover:masterfrom
Janno:janno/conversion-exit-evars

Conversation

@Janno
Copy link
Copy Markdown
Contributor

@Janno Janno commented Apr 27, 2026

Context: #Rocq users > Another situation where Rocq's type-checker diverges

Fixes / closes #????

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Documented any new / changed user messages.
    • Updated documented syntax by running make doc_gram_rsts.
  • Opened overlay pull requests.

@coqbot-app 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 Apr 27, 2026
@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented Apr 27, 2026

This is maybe correct when conversion is called from unification, but that's not the only way to call conversion from outside the kernel.
eg convert https://rocq-prover.org/doc/master/refman/proof-engine/ltac.html#rocq:tacn.convert should handle evars as opaque but not fail if it merely encounters one IMO

@Janno
Copy link
Copy Markdown
Contributor Author

Janno commented Apr 27, 2026

Performance reports on our in-house proofs show an overall 0.25% performance improvement that is almost entirely contained within a single file. Our proofs tend to use evars as little as possible so I didn't expect anything huge. There are also a bunch of failures from ssreflect rewrite, I think. Probably not worth running a full bench here until I fix convert and ssreflect rewrite.

@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented May 5, 2026

@coqbot run full ci

@coqbot-app 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 May 5, 2026
@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented May 5, 2026

@coqbot bench

@coqbot-app
Copy link
Copy Markdown
Contributor

coqbot-app Bot commented May 6, 2026

🏁 Bench results:

┌─────────────────────────────────────┬───────────────────────┬─────────────────────────────────────┬─────────────────────────┐
│                                     │     user time [s]     │          CPU instructions           │  max resident mem [KB]  │
│                                     │                       │                                     │                         │
│            package_name             │  NEW     OLD    PDIFF │      NEW            OLD       PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼───────────────────────┼─────────────────────────────────────┼─────────────────────────┤
│                             coq-vst │ 839.90  845.16  -0.62 │ 6314822538143  6388355489035  -1.15 │ 2096336  2088336   0.38 │
│                           rocq-core │   6.80    6.84  -0.58 │   41544655832    41549356302  -0.01 │  447912   443920   0.90 │
│                        rocq-bignums │  25.09   25.21  -0.48 │  159583147254   159589732389  -0.00 │  461276   460004   0.28 │
│                           coq-verdi │  43.33   43.46  -0.30 │  286529245804   286493053387   0.01 │  525860   524436   0.27 │
│                           coq-color │ 230.04  230.47  -0.19 │ 1456068563180  1456412909407  -0.02 │ 1177636  1181400  -0.32 │
│          coq-performance-tests-lite │ 902.51  903.84  -0.15 │ 7225124123086  7223283762792   0.03 │ 1219692  1214004   0.47 │
│                    coq-math-classes │  82.89   83.01  -0.14 │  499631482273   499796350277  -0.03 │  514160   514280  -0.02 │
│                        coq-coqprime │  53.29   53.36  -0.13 │  360526478453   360476516948   0.01 │  824280   824144   0.02 │
│                   coq-iris-examples │ 365.90  366.07  -0.05 │ 2377999552428  2382015999694  -0.17 │ 1071236  1088328  -1.57 │
│                        coq-compcert │ 304.97  304.81   0.05 │ 1983720248024  1986723395525  -0.15 │ 1211528  1159964   4.45 │
│                        rocq-runtime │  75.94   75.82   0.16 │  549080946525   549026445730   0.01 │  493388   493820  -0.09 │
│ coq-neural-net-interp-computed-lite │ 235.69  235.28   0.17 │ 2262013918584  2261724930828   0.01 │  880640   877072   0.41 │
│               coq-engine-bench-lite │ 129.00  128.63   0.29 │  957198495549   957204776814  -0.00 │ 1039556  1039464   0.01 │
│                         rocq-stdlib │ 439.82  438.41   0.32 │ 1550859595723  1551399816184  -0.03 │  630572   632584  -0.32 │
│                      coq-verdi-raft │ 495.51  493.83   0.34 │ 3410290864744  3408598080360   0.05 │  817988   818132  -0.02 │
│                       coq-fiat-core │  55.49   55.26   0.42 │  333599756533   333641572818  -0.01 │  480220   484584  -0.90 │
│                         coq-coqutil │  46.96   46.75   0.45 │  288723416700   288740529194  -0.01 │  566240   568068  -0.32 │
│                            coq-core │   2.77    2.68   3.36 │   18390215208    18394721947  -0.02 │   90724    90428   0.33 │
└─────────────────────────────────────┴───────────────────────┴─────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-hott (in NEW)
rocq-elpi (in NEW)
rocq-equations (in NEW)
coq-bedrock2 (in NEW)
coq-rewriter (in NEW)
coq-fiat-parsers (in NEW)
coq-unimath (in NEW)

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

🐢 Top 25 slow downs 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                          TOP 25 SLOW DOWNS                                                           │
│                                                                                                                                      │
│  OLD     NEW     DIFF    %DIFF    Ln                    FILE                                                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   18.0    18.6  0.6233    3.47%    32  coq-performance-tests-lite/src/pattern.v.html                                                 │
│ 33.951  34.555  0.6040    1.78%   194  coq-vst/veric/expr_lemmas4.v.html                                                             │
│   3.86    4.45  0.5986   15.52%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                          │
│    200     201  0.5815    0.29%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│ 35.101  35.629  0.5280    1.50%   147  coq-vst/veric/expr_lemmas4.v.html                                                             │
│  0.193   0.694  0.5004  259.13%   586  rocq-stdlib/theories/Strings/Byte.v.html                                                      │
│   17.9    18.3  0.4385    2.46%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                     │
│    1.9   2.324  0.4240   22.32%   243  coq-vst/floyd/subsume_funspec.v.html                                                          │
│  0.646    1.06  0.4177   64.70%   816  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                     │
│   2.05    2.43  0.3785   18.46%   212  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                            │
│  0.689    1.06  0.3725   54.07%   214  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                            │
│   3.91    4.27  0.3613    9.24%   196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                                 │
│  0.841    1.19  0.3494   41.52%   408  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                     │
│  0.244   0.512  0.2676  109.70%    11  rocq-stdlib/theories/omega/PreOmega.v.html                                                    │
│  0.445   0.684  0.2393   53.77%    83  rocq-stdlib/theories/Numbers/Cyclic/Int63/Sint63.v.html                                       │
│ 15.532  15.761  0.2290    1.47%  1209  coq-vst/floyd/Component.v.html                                                                │
│  0.221   0.444  0.2230  100.76%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                │
│  0.305   0.520  0.2156   70.75%    14  rocq-stdlib/theories/ZArith/auxiliary.v.html                                                  │
│  0.248   0.461  0.2130   85.93%  1166  rocq-stdlib/theories/Strings/Byte.v.html                                                      │
│ 40.351  40.563  0.2120    0.53%   834  coq-vst/veric/binop_lemmas4.v.html                                                            │
│  0.313   0.519  0.2065   66.07%    11  rocq-stdlib/theories/ZArith/Zpow_alt.v.html                                                   │
│  0.299   0.496  0.1970   65.86%    11  rocq-stdlib/theories/ZArith/Zbool.v.html                                                      │
│  0.320   0.510  0.1906   59.67%   484  rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html                                          │
│ 0.0713   0.260  0.1891  265.15%    84  rocq-stdlib/theories/Vectors/Vector.v.html                                                    │
│  0.326   0.512  0.1869   57.42%    13  rocq-stdlib/theories/micromega/ZifyNat.v.html                                                 │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                    TOP 25 SPEED UPS                                                    │
│                                                                                                                        │
│  OLD    NEW    DIFF     %DIFF     Ln                  FILE                                                             │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 3.813  0.252  -3.5610   -93.39%   241  coq-vst/floyd/subsume_funspec.v.html                                            │
│ 2.227  0.005  -2.2220   -99.78%  1496  coq-vst/floyd/SeparationLogicAsLogic.v.html                                     │
│ 0.825     0.  -0.8250  -100.00%   847  coq-vst/veric/SeparationLogic.v.html                                            │
│ 0.507  0.022  -0.4850   -95.66%   777  coq-vst/floyd/Component.v.html                                                  │
│ 0.887  0.407  -0.4804   -54.15%   682  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                                │
│  94.6   94.1  -0.4438    -0.47%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 0.808  0.418  -0.3893   -48.20%   141  rocq-stdlib/theories/Strings/Ascii.v.html                                       │
│ 0.347     0.  -0.3470  -100.00%   853  coq-vst/veric/SeparationLogic.v.html                                            │
│ 0.257     0.  -0.2570  -100.00%   857  coq-vst/veric/SeparationLogic.v.html                                            │
│ 0.565  0.324  -0.2413   -42.72%     1  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                   │
│ 0.474  0.245  -0.2298   -48.44%    11  rocq-stdlib/theories/micromega/Zify.v.html                                      │
│ 0.394  0.180  -0.2140   -54.26%    14  rocq-stdlib/theories/ZArith/Znat.v.html                                         │
│ 0.497  0.293  -0.2039   -41.05%    16  rocq-stdlib/theories/extraction/ExtrOcamlIntConv.v.html                         │
│ 0.579  0.385  -0.1937   -33.48%   596  rocq-stdlib/theories/Strings/Byte.v.html                                        │
│ 0.521  0.342  -0.1790   -34.36%    19  rocq-stdlib/theories/ZArith/Int.v.html                                          │
│ 0.497  0.322  -0.1749   -35.18%    11  rocq-stdlib/theories/micromega/ZifyComparison.v.html                            │
│ 0.537  0.368  -0.1694   -31.53%    13  rocq-stdlib/theories/ZArith/Zmin.v.html                                         │
│ 0.444  0.277  -0.1674   -37.66%    11  rocq-stdlib/theories/QArith/Qround.v.html                                       │
│ 0.165  0.001  -0.1640   -99.39%   781  coq-vst/floyd/Component.v.html                                                  │
│  22.0   21.9  -0.1584    -0.72%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                       │
│ 0.405  0.254  -0.1506   -37.19%    11  rocq-stdlib/theories/omega/OmegaLemmas.v.html                                   │
│ 0.266  0.120  -0.1465   -55.07%    23  rocq-stdlib/theories/Sorting/Sorted.v.html                                      │
│ 0.272  0.128  -0.1437   -52.90%    16  rocq-stdlib/theories/Numbers/NaryFunctions.v.html                               │
│ 0.498  0.357  -0.1413   -28.36%    15  rocq-stdlib/theories/micromega/ZifyInst.v.html                                  │
│ 0.476  0.335  -0.1412   -29.65%  1982  rocq-stdlib/theories/FSets/FMapFacts.v.html                                     │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@coqbot-app coqbot-app Bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label May 6, 2026
@Janno Janno force-pushed the janno/conversion-exit-evars branch from b527554 to f43ed06 Compare May 6, 2026 13:12
@coqbot-app coqbot-app Bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels May 6, 2026
@Janno
Copy link
Copy Markdown
Contributor Author

Janno commented May 6, 2026

I rebased my commits. Maybe that will fix things. ci-hott and ci-equations work fine for me locally. I haven't tried running the bench on my machine, though.

@Janno
Copy link
Copy Markdown
Contributor Author

Janno commented May 6, 2026

@coqbot run full ci

@coqbot-app 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 May 6, 2026
@SkySkimmer
Copy link
Copy Markdown
Contributor

SkySkimmer commented May 6, 2026

@coqbot bench

@Janno
Copy link
Copy Markdown
Contributor Author

Janno commented May 6, 2026 •
edited
Loading

The failure in corn is from this piece of code in expand in unification.ml:

        match infer_conv ~on_evars:Conversion.AbortImmediately ~pb ~ts:convflags curenv sigma m1 n1 with
        | Some sigma -> Some (push_sigma sigma substn)
        | None ->
          if is_ground_term sigma m1 && is_ground_term sigma n1 then
            error_cannot_unify curenv sigma (cM,cN)
          else None

If I change on_evars to ConsiderOpaque it works just fine. This makes sense, too. The code was relying on conversion not getting stuck on x := ?[b] |- x ~= ?b and that's no longer true and hence the code has false negatives due to incomplete ground term checks. But we don't actually want conversion to go wild on these kinds of problems; we want to return to the caller quickly.

Now I wonder if the interface I picked is too restrictive. Callers like this need to distinguish between NotConvertible (or None or Err or whatever ends up being returned) and NotConvertibleEvar (the internal exception that currently does not leak to callers). But only some callers, like the code above, actually need this information.

I am not sure how to bubble up the this specific kind of failure through Reductionops. I could leak the exception (if the client asks for it through a third kind of on_evars value) but I'd hate to add new exception handling code when the existing code is so nicely using options. The alternative is changing Reductions.infer_conv to return a result and the error value could indicate if conversion ran into an evar. That's a decent amount of downstream fallout.

@coqbot-app
Copy link
Copy Markdown
Contributor

coqbot-app Bot commented May 7, 2026

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬──────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]   │
│                                     │                         │                                       │                          │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF  │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼──────────────────────────┤
│             rocq-mathcomp-ssreflect │    1.10     1.12  -1.79 │     7134733231      7137131447  -0.03 │  587444   585820    0.28 │
│                 coq-category-theory │  548.00   554.71  -1.21 │  4023311855479   4046112725409  -0.56 │  871504   893820   -2.50 │
│          rocq-metarocq-translations │   15.69    15.84  -0.95 │   110987886708    110992386426  -0.00 │  784344   781564    0.36 │
│ coq-neural-net-interp-computed-lite │  235.54   237.62  -0.88 │  2264089109666   2263978225001   0.00 │  877976   878672   -0.08 │
│                      rocq-equations │    8.66     8.73  -0.80 │    58591781600     58570801953   0.04 │  400924   400536    0.10 │
│                       coq-fiat-core │   55.32    55.75  -0.77 │   336217071338    335944812455   0.08 │  482120   485036   -0.60 │
│                      coq-verdi-raft │  493.89   496.37  -0.50 │  3425359157600   3419966297670   0.16 │  814752   816412   -0.20 │
│          coq-performance-tests-lite │  899.94   903.93  -0.44 │  7232001806953   7232378216989  -0.01 │ 1306276  1309804   -0.27 │
│                            coq-core │    2.72     2.73  -0.37 │    18585424146     18571588435   0.07 │   90820    91284   -0.51 │
│                           coq-verdi │   43.37    43.52  -0.34 │   288500207642    288279986742   0.08 │  529784   526844    0.56 │
│                        coq-coqprime │   53.18    53.36  -0.34 │   362544320170    362174856228   0.10 │  825708   824208    0.18 │
│           rocq-metarocq-safechecker │  342.70   343.75  -0.31 │  2517745500913   2516700665943   0.04 │ 1853916  1851184    0.15 │
│                 rocq-metarocq-pcuic │  647.02   648.75  -0.27 │  4117269233728   4123134898381  -0.14 │ 2490692  2510268   -0.78 │
│                  rocq-mathcomp-boot │   39.11    39.20  -0.23 │   231417291343    231356467121   0.03 │  658356   660204   -0.28 │
│                rocq-metarocq-common │   40.97    41.04  -0.17 │   263284986439    263094144869   0.07 │  902124   893720    0.94 │
│         coq-rewriter-perf-SuperFast │  474.50   475.27  -0.16 │  3713233013499   3713545493099  -0.01 │ 1240052  1240244   -0.02 │
│                 rocq-metarocq-utils │   24.34    24.36  -0.08 │   157081803651    157001680795   0.05 │  584856   591368   -1.10 │
│                            coq-hott │  159.20   159.30  -0.06 │  1073721605149   1073961383885  -0.02 │  470336   470600   -0.06 │
│                        coq-bedrock2 │  359.86   359.73   0.04 │  2994302695529   2990445690769   0.13 │  832576   832176    0.05 │
│        coq-fiat-crypto-with-bedrock │ 7292.40  7284.91   0.10 │ 60054017536110  60045100780385   0.01 │ 2949840  2966468   -0.56 │
│                   coq-iris-examples │  365.34   364.96   0.10 │  2385791659062   2389591752178  -0.16 │ 1079484  1087492   -0.74 │
│                    coq-math-classes │   82.72    82.62   0.12 │   502529699241    502361497439   0.03 │  514156   514012    0.03 │
│                           coq-color │  231.47   231.16   0.13 │  1466422810034   1465468688214   0.07 │ 1166160  1165664    0.04 │
│                        coq-rewriter │  332.77   332.19   0.17 │  2472881320400   2470723031528   0.09 │ 1466792  1466836   -0.00 │
│                           rocq-elpi │   16.25    16.22   0.18 │   116162014006    116171691803  -0.01 │  450228   448588    0.37 │
│                         rocq-stdlib │  440.71   439.80   0.21 │  1555261693052   1554676220886   0.04 │  636564   630464    0.97 │
│              rocq-metarocq-template │   83.47    83.24   0.28 │   569483291336    569304180303   0.03 │ 1088112  1088444   -0.03 │
│                        rocq-bignums │   25.27    25.19   0.32 │   160285572150    160128788803   0.10 │  461000   459068    0.42 │
│                      coq-coquelicot │   39.25    39.10   0.38 │   235914520599    235912651770   0.00 │  832848   829572    0.39 │
│                        rocq-runtime │   76.31    75.93   0.50 │   550371371396    550460421951  -0.02 │  494448   495292   -0.17 │
│               rocq-metarocq-erasure │  478.07   475.60   0.52 │  3265478726368   3262725120754   0.08 │ 1797196  1786256    0.61 │
│                    coq-fiat-parsers │  278.00   276.32   0.61 │  2119953373372   2119377731435   0.03 │ 2025396  2268172  -10.70 │
│                         coq-coqutil │   47.19    46.88   0.66 │   292132572793    291740784478   0.13 │  563816   563932   -0.02 │
│                 rocq-mathcomp-order │   81.31    80.74   0.71 │   600366001677    600226244472   0.02 │ 1594016  1591472    0.16 │
│               coq-engine-bench-lite │  129.76   128.67   0.85 │   962186235866    957526228479   0.49 │ 1106092  1106868   -0.07 │
│                           rocq-core │    6.98     6.68   4.49 │    41658270010     41646322737   0.03 │  445532   446296   -0.17 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install
rocq-mathcomp-fingroup (in NEW)
coq-corn (in NEW)
coq-compcert (dependency install failed in NEW)
coq-unimath (in NEW)

rocq-mathcomp-algebra (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-solvable (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-field (dependency rocq-mathcomp-fingroup failed)
rocq-mathcomp-character (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-odd-order (dependency rocq-mathcomp-fingroup failed)
coq-mathcomp-analysis (dependency rocq-mathcomp-fingroup failed)
coq-fourcolor (dependency rocq-mathcomp-fingroup failed)
coq-vst (dependency coq-compcert failed)

🐢 Top 25 slow downs 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SLOW DOWNS                                                            │
│                                                                                                                                        │
│  OLD     NEW    DIFF    %DIFF    Ln                     FILE                                                                           │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   21.5   22.7  1.2156    5.66%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                          │
│   44.4   45.6  1.1888    2.68%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html              │
│   42.2   43.3  1.1252    2.67%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                          │
│    107    108  0.9995    0.94%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                           │
│   64.1   65.0  0.9189    1.43%   608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html    │
│   44.1   45.0  0.8204    1.86%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                 │
│   46.0   46.6  0.5827    1.27%   115  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html     │
│  0.175  0.687  0.5121  293.04%   586  rocq-stdlib/theories/Strings/Byte.v.html                                                         │
│   33.4   33.9  0.5119    1.53%   898  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                             │
│  0.237  0.729  0.4914  206.89%    11  rocq-stdlib/theories/ZArith/Zpow_alt.v.html                                                      │
│  0.241  0.707  0.4663  193.48%    17  rocq-stdlib/theories/micromega/Env.v.html                                                        │
│   3.78   4.25  0.4643   12.28%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                             │
│   9.87   10.3  0.4502    4.56%   326  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                         │
│   36.5   36.9  0.4098    1.12%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                     │
│   14.8   15.2  0.4001    2.71%   841  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                          │
│   7.81   8.20  0.3878    4.96%  1831  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│   10.9   11.3  0.3829    3.52%   158  coq-fiat-crypto-with-bedrock/src/Bedrock/P256.v.html                                             │
│   25.3   25.7  0.3818    1.51%   788  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                             │
│ 0.0753  0.453  0.3773  501.21%    22  rocq-stdlib/theories/Vectors/VectorEq.v.html                                                     │
│  0.138  0.511  0.3732  269.85%   270  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                               │
│   9.58   9.95  0.3640    3.80%   304  coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html                                      │
│   18.0   18.4  0.3577    1.98%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                        │
│   2.30   2.63  0.3217   13.96%   212  rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html                                               │
│   21.6   21.9  0.3216    1.49%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                        │
│  0.413  0.733  0.3201   77.52%    16  rocq-stdlib/theories/extraction/ExtrOcamlIntConv.v.html                                          │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                             │
│                                                                                                                                         │
│  OLD    NEW     DIFF     %DIFF    Ln                     FILE                                                                           │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   202     200  -1.9712   -0.97%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html    │
│  45.3    43.4  -1.8901   -4.17%   578  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                 │
│  94.4    92.5  -1.8225   -1.93%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│  94.2    92.7  -1.5958   -1.69%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                  │
│   238     237  -1.1433   -0.48%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                       │
│  25.3    24.4  -0.9728   -3.84%   550  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                  │
│   134     133  -0.9207   -0.69%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                       │
│ 0.788  0.0398  -0.7481  -94.95%   656  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.v.html    │
│ 0.781  0.0398  -0.7413  -94.91%   605  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvCommon.v.html    │
│  3.92    3.18  -0.7398  -18.88%   130  coq-category-theory/Functor/Strong/Product.v.html                                                │
│  54.6    54.0  -0.5627   -1.03%   296  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                               │
│  51.6    51.1  -0.5570   -1.08%   571  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                       │
│  1.54    1.02  -0.5257  -34.07%   572  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                        │
│  39.6    39.2  -0.4658   -1.18%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│  18.6    18.1  -0.4550   -2.45%    32  coq-performance-tests-lite/src/pattern.v.html                                                    │
│ 0.724   0.276  -0.4486  -61.94%    18  rocq-stdlib/theories/ZArith/Zeven.v.html                                                         │
│  36.3    35.8  -0.4294   -1.18%   195  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                    │
│  2.41    2.00  -0.4112  -17.05%   142  rocq-metarocq-pcuic/pcuic/theories/PCUICContextConversion.v.html                                 │
│  38.5    38.1  -0.4049   -1.05%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                   │
│ 0.730   0.331  -0.3985  -54.63%   760  rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html                                             │
│  30.5    30.2  -0.3855   -1.26%   305  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                               │
│  81.3    80.9  -0.3720   -0.46%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                      │
│  1.03   0.670  -0.3607  -34.99%   597  rocq-stdlib/theories/Strings/Byte.v.html                                                         │
│  17.3    16.9  -0.3405   -1.97%   669  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                            │
│ 0.452   0.138  -0.3143  -69.55%    20  rocq-stdlib/theories/Vectors/Bvector.v.html                                                      │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@coqbot-app
Copy link
Copy Markdown
Contributor

coqbot-app Bot commented May 7, 2026

🔴 CI failures at commit f43ed06 without any failure in the test-suite

✔️ Corresponding jobs for the base commit af3cabc succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-corn, ci-quickchick, ci-unimath
  • You can also pass me a specific list of targets to minimize as arguments.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@Janno @SkySkimmer