Use algebraic datatypes to signal failure in Conversion API #19120

ppedrot · 2024-05-30T20:41:39Z

Instead of haphazardly raising exceptions on a unit type and hoping that somebody will eventually catch them, we make the kernel conversion function return a parameterized result type that additionally indicates the ways in which the function may fail.

As a a result, I found at least two bugs in Typeops where a stray NotConvertible exception could have reached toplevel without being caught when given ill-typed terms.

This should also alleviate the hassle of the upper layers where it's never clear which part of the code is supposed to handle the variouse universe failures in universe unification.

Overlays:

Adapt w.r.t. coq/coq#19120. smtcoq/smtcoq#143

ppedrot · 2024-05-30T20:42:32Z

Just in case @coqbot bench

pretyping/reductionops.ml

kernel/conversion.ml

SkySkimmer · 2024-05-30T21:02:10Z

kernel/conversion.ml

         let () = if irr_flex infos.cnv_inf fl1 then raise NotConvertible (* trigger the fallback *) in
         convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
-       with NotConvertible | UGraph.UniverseInconsistency _ ->
+       with NotConvertible | NotConvertibleTrace _ ->


It doesn't need to be in this PR, but in the case where neither fflex is unfoldable we may want to reraise this error instead of raising NotConvertible and dropping any further information.

coqbot-app · 2024-05-31T07:53:20Z

🏁 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-verdi-raft │  574.47   581.91  -1.28 │  2616379929740   2647855619952  -1.19 │  4105966287792   4144679110269  -0.93 │  852368   852376  -0.00 │
│                           coq-verdi │   48.63    49.12  -1.00 │   219437556307    220640038336  -0.54 │   336879066281    339170626879  -0.68 │  531348   530236   0.21 │
│                       coq-fourcolor │ 1377.70  1390.14  -0.89 │  6304751834343   6360726753850  -0.88 │ 12780901656764  12781294708440  -0.00 │  833980   834068  -0.01 │
│                         coq-bignums │   29.31    29.46  -0.51 │   132919173854    133565478928  -0.48 │   191197918794    192079091231  -0.46 │  472668   474748  -0.44 │
│                        coq-bedrock2 │  362.42   363.49  -0.29 │  1653471952183   1655607875003  -0.13 │  3108810702630   3104139669634   0.15 │  878380   875736   0.30 │
│               coq-engine-bench-lite │  155.90   156.28  -0.24 │   660118000245    661940322823  -0.28 │  1220795861381   1217947488172   0.23 │ 1111880  1111780   0.01 │
│                        coq-coqprime │   48.23    48.33  -0.21 │   216861370743    216754353221   0.05 │   331567310972    332148679739  -0.18 │  784964   782408   0.33 │
│         coq-rewriter-perf-SuperFast │  779.41   780.77  -0.17 │  3543423626180   3550646501123  -0.20 │  6153199989559   6161635024930  -0.14 │ 1573252  1566860   0.41 │
│                            coq-core │  127.53   127.72  -0.15 │   510209278771    508750992088   0.29 │   532823890731    532122902978   0.13 │  457996   456808   0.26 │
│                        coq-rewriter │  386.39   386.01   0.10 │  1755372215337   1755378311272  -0.00 │  2922784436070   2931764353778  -0.31 │ 1482032  1480196   0.12 │
│        coq-fiat-crypto-with-bedrock │ 5940.47  5928.10   0.21 │ 27054568153341  26996605847482   0.21 │ 47958376105693  48029643811551  -0.15 │ 3246044  3246112  -0.00 │
│                          coq-stdlib │  347.81   347.03   0.22 │  1482760663324   1476312075289   0.44 │  1257821139755   1257632622806   0.01 │  715052   712900   0.30 │
│                            coq-hott │  163.76   163.17   0.36 │   734903429927    730287423099   0.63 │  1155550846731   1155825071415  -0.02 │  470440   467448   0.64 │
│                    coq-math-classes │   86.15    85.71   0.51 │   386497758376    385148660220   0.35 │   536360315839    536781687777  -0.08 │  504196   504124   0.01 │
│                           coq-color │  253.63   252.30   0.53 │  1141021139178   1133909166638   0.63 │  1624695209779   1629157255514  -0.27 │ 1168220  1166920   0.11 │
│               coq-mathcomp-fingroup │   31.17    31.00   0.55 │   142241039871    140413202637   1.30 │   211361281915    211288499589   0.03 │  566744   567528  -0.14 │
│                coq-mathcomp-algebra │  264.37   262.55   0.69 │  1205648520102   1198020786293   0.64 │  2025256416745   2025266611591  -0.00 │ 1335740  1316868   1.43 │
│ coq-neural-net-interp-computed-lite │  241.33   239.65   0.70 │  1102008651729   1094100344142   0.72 │  2307270697868   2307467238938  -0.01 │  834248   834040   0.02 │
│              coq-mathcomp-ssreflect │  221.97   220.39   0.72 │  1013266572260   1006247145586   0.70 │  1681618983825   1680679945155   0.06 │ 1733108  1737036  -0.23 │
│          coq-performance-tests-lite │  872.55   866.21   0.73 │  3950979518696   3921274979378   0.76 │  6979238558018   6985436098550  -0.09 │ 2275440  2275632  -0.01 │
│                        coq-compcert │  281.60   279.40   0.79 │  1274272662181   1263027968141   0.89 │  1933610638137   1932279063015   0.07 │ 1107852  1107536   0.03 │
│                    coq-fiat-parsers │  307.20   304.57   0.86 │  1371079289470   1356893695060   1.05 │  2387331319330   2388764809333  -0.06 │ 2674676  2685032  -0.39 │
│                   coq-iris-examples │  471.53   467.28   0.91 │  2144772998046   2124225380802   0.97 │  3258450078202   3262730415125  -0.13 │ 1114660  1116804  -0.19 │
│              coq-mathcomp-character │  111.98   110.94   0.94 │   511595763145    506796964252   0.95 │   803383222888    803372163673   0.00 │ 1141904  1160872  -1.63 │
│                      coq-coquelicot │   39.10    38.72   0.98 │   174654780289    173704106448   0.55 │   243563402679    243446261999   0.05 │  802032   802736  -0.09 │
│                            coq-corn │  722.21   714.92   1.02 │  3281006785015   3246223568694   1.07 │  5066161085379   5073146895836  -0.14 │  787260   787128   0.02 │
│                             coq-vst │  877.70   868.02   1.12 │  3991532792747   3948696462816   1.08 │  6713306381897   6704383386166   0.13 │ 2180644  2197796  -0.78 │
│               coq-mathcomp-solvable │  121.81   120.34   1.22 │   556313215871    549624149736   1.22 │   875360019583    875105749655   0.03 │  875180   875168   0.00 │
│                  coq-mathcomp-field │  146.43   144.52   1.32 │   668643842037    660014219685   1.31 │  1092715745172   1092134083801   0.05 │ 1277404  1272896   0.35 │
│                       coq-fiat-core │   59.75    58.96   1.34 │   249843124061    246113787346   1.52 │   365347985705    365865108093  -0.14 │  485168   482056   0.65 │
│                         coq-coqutil │   42.58    42.01   1.36 │   187718449543    186394726178   0.71 │   268333342605    269517270691  -0.44 │  561352   561012   0.06 │
│              coq-mathcomp-odd-order │  815.30   786.44   3.67 │  3734213917200   3601786146322   3.68 │  6136252861876   6134353847255   0.03 │ 1656696  1660548  -0.23 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-equations
coq-unimath

coq-metacoq-template (dependency coq-equations failed)
coq-metacoq-pcuic (dependency coq-equations failed)
coq-metacoq-safechecker (dependency coq-equations failed)
coq-metacoq-erasure (dependency coq-equations failed)
coq-metacoq-translations (dependency coq-equations failed)
coq-category-theory (dependency coq-equations failed)

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                 TOP 25 SLOW DOWNS                                                                  │
│                                                                                                                                                    │
│   OLD       NEW      DIFF    %DIFF    Ln                      FILE                                                                                 │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  76.3400   86.8600  10.5200  13.78%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                       │
│  63.3860   72.0720   8.6860  13.70%   368  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                       │
│ 217.7880  220.6330   2.8450   1.31%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                     │
│  19.5350   22.1730   2.6380  13.50%  2061  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│ 180.6530  182.2260   1.5730   0.87%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  48.1390   49.5420   1.4030   2.91%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│  48.2520   49.5670   1.3150   2.73%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                         │
│ 199.0940  200.3650   1.2710   0.64%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│  16.1150   17.2930   1.1780   7.31%   828  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 │
│   3.0180    3.9580   0.9400  31.15%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  16.9900   17.8350   0.8450   4.97%   607  coq-mathcomp-odd-order/theories/PFsection9.v.html                                                       │
│  43.9300   44.6800   0.7500   1.71%   834  coq-vst/veric/binop_lemmas4.v.html                                                                      │
│  33.3670   34.1000   0.7330   2.20%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│  37.6250   38.3510   0.7260   1.93%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html                   │
│  11.3020   11.9830   0.6810   6.03%  2103  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                                  │
│  26.9450   27.4440   0.4990   1.85%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html      │
│  46.1320   46.6170   0.4850   1.05%   926  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                               │
│  36.1980   36.6780   0.4800   1.33%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│  37.5740   38.0520   0.4780   1.27%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                        │
│  27.6570   28.0470   0.3900   1.41%  1933  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v.html                         │
│  36.6770   37.0660   0.3890   1.06%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│  32.8830   33.2420   0.3590   1.09%    97  coq-vst/veric/binop_lemmas5.v.html                                                                      │
│  21.4870   21.8370   0.3500   1.63%   376  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvMetric.v.html           │
│  14.9950   15.3210   0.3260   2.17%  1382  coq-rewriter/src/Rewriter/Language/Wf.v.html                                                            │
│  29.7780   30.0880   0.3100   1.04%   194  coq-vst/veric/expr_lemmas4.v.html                                                                       │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SPEED UPS                                                              │
│                                                                                                                                           │
│   OLD       NEW      DIFF     %DIFF    Ln                    FILE                                                                         │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  64.8180   62.6220  -2.1960   -3.39%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │
│  64.1490   62.0200  -2.1290   -3.32%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                   │
│ 101.3350   99.9840  -1.3510   -1.33%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                   │
│  40.2220   39.1510  -1.0710   -2.66%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html     │
│ 236.4230  235.4480  -0.9750   -0.41%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                    │
│ 131.0580  130.2430  -0.8150   -0.62%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                        │
│  25.5340   24.8260  -0.7080   -2.77%    12  coq-fourcolor/theories/job227to230.v.html                                                     │
│  47.0730   46.3740  -0.6990   -1.48%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html  │
│ 135.6380  134.9870  -0.6510   -0.48%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                    │
│  96.3010   95.7020  -0.5990   -0.62%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  12.3470   11.7890  -0.5580   -4.52%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                      │
│  96.2910   95.7480  -0.5430   -0.56%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  38.7560   38.2210  -0.5350   -1.38%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                │
│  19.9760   19.4530  -0.5230   -2.62%    12  coq-fourcolor/theories/job507to510.v.html                                                     │
│   4.8950    4.4030  -0.4920  -10.05%  1109  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v.html │
│  30.0530   29.5720  -0.4810   -1.60%    12  coq-fourcolor/theories/job165to189.v.html                                                     │
│  26.7330   26.2540  -0.4790   -1.79%    12  coq-fourcolor/theories/job399to438.v.html                                                     │
│  25.2340   24.7880  -0.4460   -1.77%    12  coq-fourcolor/theories/job291to294.v.html                                                     │
│  10.1480    9.7130  -0.4350   -4.29%   496  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                                  │
│  25.5440   25.1160  -0.4280   -1.68%    12  coq-fourcolor/theories/job499to502.v.html                                                     │
│  20.1700   19.7460  -0.4240   -2.10%   214  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                          │
│  24.2370   23.8250  -0.4120   -1.70%    12  coq-fourcolor/theories/job231to234.v.html                                                     │
│  19.9120   19.5090  -0.4030   -2.02%   325  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                          │
│  31.0300   30.6330  -0.3970   -1.28%    12  coq-fourcolor/theories/job254to270.v.html                                                     │
│  26.5200   26.1320  -0.3880   -1.46%    12  coq-fourcolor/theories/job190to206.v.html                                                     │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

ppedrot · 2024-05-31T08:01:00Z

│ coq-mathcomp-odd-order │ 815.30 786.44 3.67 │ 3734213917200 3601786146322 3.68 │ 6136252861876 6134353847255 0.03 │ 1656696 1660548 -0.23 │

Is this an actual slowdown? @silene claimed in another PR that the only column that mattered was the CPU instruction ones, which would mean that this is noise, but I'm a bit wary. The odd-order dev seems to be a bit noisy these days.

silene · 2024-05-31T08:20:05Z

To be clearer, it is the only column we can trust to be reproducible. The "user time" column matters too, but its results can be meaningfully interpreted only in -j1 mode on an otherwise idle machine.

ppedrot · 2024-05-31T09:14:13Z

The slow odd-order lines from the bench are really degenerated, and profiling them doesn't show any remarkable diff w.r.t. conversion. Rather, it's largely dominated by evar expansion, which is unrelated to this PR.

SkySkimmer · 2024-05-31T09:17:08Z

The bench is -j1 on an idle machine (except coq-core and coq-stdlib which have bigger -j)

silene · 2024-05-31T12:09:18Z

I stand corrected. I hadn't understood that the various bench runners were running on physically distinct servers, and I had missed the -j1 part due to opam var --global jobs=$number_of_processors. But then I have no explanation for a 4% difference in running time; this is no longer in the noise for an idle machine.

ppedrot · 2024-06-01T12:39:44Z

In any case, the slight slowdown from odd-order will be made moot by #19123. These lines were hitting right in an algorithmic limitation of evar expansion, and after that PR they're 10 times faster or so (~80s to ~7s on my machine).

This may generate slightly better error messages in some cases.

There are some dubious parts of the code where the NotConvertible exception is not properly caught, we leave a FIXME there to enhance the message at some future point.

Now all functions are returning algebraic errors so there is no point in exposing this internal detail.

We have to create local extensible types to do this in a type-safe way, but it should not matter for performance since this is only done once per toplevel invocation of conversion.

We only call fail_check from within eqappr rather than export wrappers that perform the call internally.

Adapt w.r.t. rocq-prover/rocq#19120.

ppedrot · 2024-06-01T18:24:22Z

Let's rerun a bench in any case. @coqbot bench

coqbot-app · 2024-06-02T13:21:27Z

🏁 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 │   59.18    60.29  -1.84 │   246555443875    250155480293  -1.44 │   368752068912    369228362946  -0.13 │  482772   485112  -0.48 │
│              coq-mathcomp-odd-order │  792.63   805.06  -1.54 │  3629410228607   3687392009991  -1.57 │  6136079230839   6134490141055   0.03 │ 1650528  1651336  -0.05 │
│                       coq-equations │   12.05    12.22  -1.39 │    50725997704     50870912744  -0.28 │    79737435260     79843108670  -0.13 │  426348   425212   0.27 │
│                      coq-verdi-raft │  574.52   581.87  -1.26 │  2615534236803   2647138833106  -1.19 │  4110334447011   4148545239767  -0.92 │  854328   854388  -0.01 │
│            coq-metacoq-translations │   16.89    17.10  -1.23 │    75403941983     76062742187  -0.87 │   124423272210    124569722329  -0.12 │  836968   843688  -0.80 │
│                         coq-coqutil │   42.17    42.64  -1.10 │   185825597624    189103492205  -1.73 │   270073631261    271371570505  -0.48 │  560744   560560   0.03 │
│                           coq-verdi │   48.45    48.98  -1.08 │   218356982143    221173874908  -1.27 │   337491832420    339988400868  -0.73 │  530800   529512   0.24 │
│                           coq-color │  251.42   253.52  -0.83 │  1129276696560   1140098372927  -0.95 │  1629344533717   1633635083020  -0.26 │ 1167400  1165744   0.14 │
│                            coq-core │  127.74   128.57  -0.65 │   505802747016    502608544186   0.64 │   532477695476    532303619300   0.03 │  459028   458188   0.18 │
│                          coq-stdlib │  347.64   349.79  -0.61 │  1481372761327   1488095561348  -0.45 │  1259479559112   1259242586528   0.02 │  713048   714292  -0.17 │
│ coq-neural-net-interp-computed-lite │  241.97   243.43  -0.60 │  1104694422815   1111439394716  -0.61 │  2309521741298   2309760950101  -0.01 │  817084   817184  -0.01 │
│                            coq-corn │  718.89   722.93  -0.56 │  3261934697120   3284290909374  -0.68 │  5067908695389   5074817027259  -0.14 │  788136   785576   0.33 │
│                        coq-coqprime │   48.10    48.37  -0.56 │   216010896506    217051910095  -0.48 │   332526367598    333113248476  -0.18 │  786216   787272  -0.13 │
│          coq-performance-tests-lite │  864.57   868.91  -0.50 │  3914864725278   3934259117209  -0.49 │  6981199536542   6985333943299  -0.06 │ 2275116  2276416  -0.06 │
│                            coq-hott │  163.35   164.05  -0.43 │   730361834086    735591301980  -0.71 │  1159003912254   1159172828670  -0.01 │  467420   469784  -0.50 │
│                  coq-mathcomp-field │  138.03   138.57  -0.39 │   630810309696    632576663772  -0.28 │  1038942666967   1038628296989   0.03 │ 1273756  1273604   0.01 │
│                coq-metacoq-template │  150.75   151.32  -0.38 │   668241595929    672077227152  -0.57 │  1044603833725   1046057820290  -0.14 │ 1514484  1512268   0.15 │
│                    coq-fiat-parsers │  305.79   306.90  -0.36 │  1364566932312   1367938908172  -0.25 │  2399608513836   2395206503559   0.18 │ 2434908  2680612  -9.17 │
│                    coq-math-classes │   85.85    86.15  -0.35 │   385855495493    386402340321  -0.14 │   537042012113    537566146468  -0.10 │  503504   504492  -0.20 │
│                         coq-bignums │   29.51    29.60  -0.30 │   133590387153    134620533701  -0.77 │   191275400707    192151475034  -0.46 │  472552   474792  -0.47 │
│                 coq-category-theory │  659.23   659.79  -0.08 │  2998903732200   3001975071816  -0.10 │  4898020919003   4905995256512  -0.16 │  971832   987876  -1.62 │
│                      coq-coquelicot │   39.28    39.31  -0.08 │   175223000917    174853039186   0.21 │   245067099586    244986517589   0.03 │  801860   803532  -0.21 │
│        coq-fiat-crypto-with-bedrock │ 5925.52  5929.88  -0.07 │ 26983972547340  27001610143357  -0.07 │ 47962905500894  48050852673972  -0.18 │ 3246108  3246120  -0.00 │
│              coq-mathcomp-character │  109.03   109.08  -0.05 │   498020394426    498288601573  -0.05 │   790596411346    790414710156   0.02 │ 1092252  1117264  -2.24 │
│              coq-mathcomp-ssreflect │  203.33   203.38  -0.02 │   927878042034    928461854822  -0.06 │  1550500152344   1550959070555  -0.03 │ 1716452  1739064  -1.30 │
│                             coq-vst │  873.67   872.79   0.10 │  3971152731225   3971623382250  -0.01 │  6712485573967   6703822395636   0.13 │ 2244984  2200648   2.01 │
│               coq-engine-bench-lite │  156.30   155.93   0.24 │   663288838994    659831880568   0.52 │  1224463758467   1217949468597   0.53 │ 1112008  1111808   0.02 │
│                        coq-rewriter │  388.27   387.33   0.24 │  1765376676260   1761030017298   0.25 │  2925696149683   2934987477428  -0.32 │ 1481488  1477944   0.24 │
│                        coq-compcert │  281.78   281.02   0.27 │  1274029860871   1270708183845   0.26 │  1934230328739   1932680370218   0.08 │ 1108916  1109700  -0.07 │
│                        coq-bedrock2 │  364.67   363.68   0.27 │  1661221473362   1655745326973   0.33 │  3111546628787   3106687441102   0.16 │  880880   876632   0.48 │
│                coq-mathcomp-algebra │  242.67   241.74   0.38 │  1106625146902   1102338542769   0.39 │  1857906674154   1857698150275   0.01 │ 1321984  1323940  -0.15 │
│         coq-rewriter-perf-SuperFast │  784.33   781.03   0.42 │  3565357389306   3550635633389   0.41 │  6157272144502   6168285499918  -0.18 │ 1575804  1568956   0.44 │
│                   coq-metacoq-pcuic │  991.25   986.58   0.47 │  4441606007446   4419964926295   0.49 │  6465016705386   6476364326367  -0.18 │ 2679312  2678728   0.02 │
│                 coq-metacoq-erasure │  537.80   534.73   0.57 │  2454045288612   2439694041773   0.59 │  3807622046123   3813726521204  -0.16 │ 2101356  2083808   0.84 │
│             coq-metacoq-safechecker │  423.43   420.38   0.73 │  1938341444448   1923895718570   0.75 │  3175893257082   3175120685575   0.02 │ 2057928  2039576   0.90 │
│               coq-mathcomp-solvable │  121.43   120.38   0.87 │   554822057223    549687558874   0.93 │   874309854158    873336398164   0.11 │  874116   876428  -0.26 │
│                       coq-fourcolor │ 1387.36  1374.38   0.94 │  6348337791821   6289035012506   0.94 │ 12780997183106  12781637117971  -0.01 │  834280   833972   0.04 │
│                   coq-iris-examples │  471.58   465.19   1.37 │  2146059223326   2115134228078   1.46 │  3265046722311   3268829002347  -0.12 │ 1114700  1113056   0.15 │
│               coq-mathcomp-fingroup │   31.01    30.58   1.41 │   141309424849    139228043045   1.49 │   210352306656    210185320340   0.08 │  565972   563984   0.35 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite
coq-unimath

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                 TOP 25 SLOW DOWNS                                                                 │
│                                                                                                                                                   │
│   OLD       NEW      DIFF   %DIFF    Ln                      FILE                                                                                 │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 256.1640  259.0930  2.9290   1.14%  1629  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                                                         │
│  19.9930   21.8300  1.8370   9.19%  2061  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│ 181.3290  182.7070  1.3780   0.76%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  94.5390   95.8520  1.3130   1.39%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  48.0640   49.2750  1.2110   2.52%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                         │
│  94.6500   95.8350  1.1850   1.25%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  46.3850   47.3810  0.9960   2.15%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html            │
│ 129.6190  130.5790  0.9600   0.74%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│  46.3890   47.2440  0.8550   1.84%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                              │
│  36.3530   37.1680  0.8150   2.24%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│  33.3440   34.1070  0.7630   2.29%  1333  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│   3.1110    3.8630  0.7520  24.17%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  11.8190   12.4230  0.6040   5.11%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│  48.3770   48.9690  0.5920   1.22%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│   3.5890    4.1520  0.5630  15.69%   128  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│  43.8430   44.3990  0.5560   1.27%   834  coq-vst/veric/binop_lemmas4.v.html                                                                      │
│  36.3070   36.8610  0.5540   1.53%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│  65.6070   66.1100  0.5030   0.77%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  30.5100   30.9730  0.4630   1.52%    12  coq-fourcolor/theories/job254to270.v.html                                                               │
│  24.3320   24.7920  0.4600   1.89%    12  coq-fourcolor/theories/job503to506.v.html                                                               │
│  19.8790   20.3390  0.4600   2.31%   214  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                                    │
│  29.6210   30.0620  0.4410   1.49%    12  coq-fourcolor/theories/job001to106.v.html                                                               │
│  26.9110   27.3500  0.4390   1.63%    12  coq-fourcolor/theories/job287to290.v.html                                                               │
│  26.2930   26.7230  0.4300   1.64%    12  coq-fourcolor/theories/job611to617.v.html                                                               │
│  19.6220   20.0430  0.4210   2.15%   325  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                                    │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                 │
│                                                                                                                                                 │
│   OLD       NEW      DIFF     %DIFF    Ln                      FILE                                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  86.2880   76.4550  -9.8330  -11.40%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                   │
│  71.5770   63.4080  -8.1690  -11.41%   368  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                   │
│ 202.5640  201.0450  -1.5190   -0.75%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html       │
│  38.3980   37.3100  -1.0880   -2.83%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html               │
│  10.5930    9.6990  -0.8940   -8.44%   496  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html                                         │
│  38.1500   37.3530  -0.7970   -2.09%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                    │
│  23.5300   22.8610  -0.6690   -2.84%   296  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                          │
│  10.4590    9.8240  -0.6350   -6.07%   496  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                                        │
│  36.7410   36.1210  -0.6200   -1.69%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                             │
│   4.9370    4.3460  -0.5910  -11.97%  1109  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/ValidComputable/Expr.v.html       │
│  27.6210   27.0440  -0.5770   -2.09%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html  │
│  11.7700   11.2290  -0.5410   -4.60%  2103  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                              │
│ 100.2900   99.7560  -0.5340   -0.53%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                         │
│  27.4140   26.9750  -0.4390   -1.60%    35  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                │
│  29.1290   28.7260  -0.4030   -1.38%    32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                │
│  16.1130   15.7250  -0.3880   -2.41%   828  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                             │
│  23.7380   23.4220  -0.3160   -1.33%     6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html │
│   3.9000    3.5980  -0.3020   -7.74%   884  coq-mathcomp-odd-order/theories/BGsection16.v.html                                                  │
│   4.0120    3.7180  -0.2940   -7.33%   441  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                           │
│   0.6600    0.3700  -0.2900  -43.94%   868  coq-stdlib/MSets/MSetRBT.v.html                                                                     │
│  18.2030   17.9170  -0.2860   -1.57%   708  coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html                                        │
│  15.2960   15.0140  -0.2820   -1.84%   613  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html             │
│   4.7350    4.4570  -0.2780   -5.87%     5  coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed11.v.html      │
│   7.5240    7.2540  -0.2700   -3.59%   356  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html                                         │
│  12.9110   12.6660  -0.2450   -1.90%  1555  coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

ppedrot · 2024-06-02T14:56:31Z

No more oddorder slowdown, this may have been noise after all.

SkySkimmer · 2024-06-03T08:42:34Z

@coqbot merge now

coqbot-app · 2024-06-03T08:42:38Z

@SkySkimmer: Please take care of the following overlays:

19120-ppedrot-conversion-no-inner-exception-api.sh

ppedrot added kind: cleanup Code removal, deprecation, refactorings, etc. request: full CI Use this label when you want your next push to trigger a full CI. labels May 30, 2024

ppedrot requested review from a team as code owners May 30, 2024 20:41

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

SkySkimmer reviewed May 30, 2024

View reviewed changes

pretyping/reductionops.ml Outdated Show resolved Hide resolved

kernel/conversion.ml Outdated Show resolved Hide resolved

SkySkimmer self-assigned this May 30, 2024

SkySkimmer reviewed May 30, 2024

View reviewed changes

SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label May 31, 2024

ppedrot added 5 commits June 1, 2024 14:53

Stop relying on exceptions for universe unification in Conversion API.

83b1012

This may generate slightly better error messages in some cases.

Return an algebraic error out of kernel conversion functions.

df388f1

There are some dubious parts of the code where the NotConvertible exception is not properly caught, we leave a FIXME there to enhance the message at some future point.

Remove the NotConvertible error from the Conversion API.

fd6ea33

Now all functions are returning algebraic errors so there is no point in exposing this internal detail.

Parameterize the type of errors in conversion API.

f8e53e2

We have to create local extensible types to do this in a type-safe way, but it should not matter for performance since this is only done once per toplevel invocation of conversion.

Small change of calling convention in Conversion.

64dabc7

We only call fail_check from within eqappr rather than export wrappers that perform the call internally.

ppedrot added a commit to ppedrot/Coq-Equations that referenced this pull request Jun 1, 2024

Adapt w.r.t. rocq-prover/rocq#19120.

7d20d45

ppedrot added a commit to ppedrot/smtcoq that referenced this pull request Jun 1, 2024

Adapt w.r.t. rocq-prover/rocq#19120.

0c55859

ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request Jun 1, 2024

Merge pull request #605 from ppedrot/conversion-no-inner-exception-api

a8d8f44

Adapt w.r.t. rocq-prover/rocq#19120.

Add overlays.

79b9667

ppedrot added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 1, 2024

ppedrot force-pushed the conversion-no-inner-exception-api branch from 08c3e2f to 79b9667 Compare June 1, 2024 13:37

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

ppedrot removed the needs: overlay This is breaking external developments we track in CI. label Jun 1, 2024

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

ppedrot added this to the 8.20+rc1 milestone Jun 2, 2024

SkySkimmer approved these changes Jun 3, 2024

View reviewed changes

coqbot-app bot merged commit 4248ee4 into rocq-prover:master Jun 3, 2024

ckeller pushed a commit to smtcoq/smtcoq that referenced this pull request Jun 3, 2024

Adapt w.r.t. rocq-prover/rocq#19120. (#143)

d951f13

ppedrot deleted the conversion-no-inner-exception-api branch June 3, 2024 08:47

ckeller pushed a commit to smtcoq/smtcoq that referenced this pull request Sep 18, 2024

Adapt w.r.t. rocq-prover/rocq#19120. (#143)

3c81149

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Use algebraic datatypes to signal failure in Conversion API #19120

Use algebraic datatypes to signal failure in Conversion API #19120

Uh oh!

ppedrot commented May 30, 2024 •

edited

Loading

Uh oh!

ppedrot commented May 30, 2024

Uh oh!

Uh oh!

Uh oh!

SkySkimmer May 30, 2024

Uh oh!

coqbot-app bot commented May 31, 2024

Uh oh!

ppedrot commented May 31, 2024

Uh oh!

silene commented May 31, 2024

Uh oh!

ppedrot commented May 31, 2024

Uh oh!

SkySkimmer commented May 31, 2024

Uh oh!

silene commented May 31, 2024

Uh oh!

ppedrot commented Jun 1, 2024

Uh oh!

ppedrot commented Jun 1, 2024

Uh oh!

coqbot-app bot commented Jun 2, 2024

Uh oh!

ppedrot commented Jun 2, 2024

Uh oh!

SkySkimmer commented Jun 3, 2024

Uh oh!

coqbot-app bot commented Jun 3, 2024

Uh oh!

Uh oh!

Use algebraic datatypes to signal failure in Conversion API #19120

Use algebraic datatypes to signal failure in Conversion API #19120

Uh oh!

Conversation

ppedrot commented May 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ppedrot commented May 30, 2024

Uh oh!

Uh oh!

Uh oh!

SkySkimmer May 30, 2024

Choose a reason for hiding this comment

Uh oh!

coqbot-app bot commented May 31, 2024

Uh oh!

ppedrot commented May 31, 2024

Uh oh!

silene commented May 31, 2024

Uh oh!

ppedrot commented May 31, 2024

Uh oh!

SkySkimmer commented May 31, 2024

Uh oh!

silene commented May 31, 2024

Uh oh!

ppedrot commented Jun 1, 2024

Uh oh!

ppedrot commented Jun 1, 2024

Uh oh!

coqbot-app bot commented Jun 2, 2024

Uh oh!

ppedrot commented Jun 2, 2024

Uh oh!

SkySkimmer commented Jun 3, 2024

Uh oh!

coqbot-app bot commented Jun 3, 2024

Uh oh!

Uh oh!

ppedrot commented May 30, 2024 •

edited

Loading