Recurse less in extraction by SkySkimmer · Pull Request #16206 · rocq-prover/rocq

SkySkimmer · 2022-06-17T12:28:43Z

SkySkimmer · 2022-06-17T12:29:01Z

SkySkimmer · 2022-06-17T12:29:21Z

@JasonGross could you test this on your original example?

JasonGross · 2022-06-17T14:13:04Z

My laptop is currently broken and I don't have access to Coq, but the code is available at mit-plv/fiat-crypto#1293, just run make SKIP_BEDROCK2=1 src/ExtractionOCaml/saturated_solinas.ml TIMED=1 and see if it takes closer to 20 seconds than 90 minutes to extract the .ml file.

coqbot-app · 2022-06-18T04:39:48Z

🏁 Bench results:

┌──────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                              │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │   mem faults    │
│                              │                         │                                       │                                       │                         │                 │
│         package_name         │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │ NEW  OLD  PDIFF │
├──────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│      coq-metacoq-safechecker │  211.19   212.64  -0.68 │   956660705129    964310532899  -0.79 │  1432729501890   1433721213508  -0.07 │ 1424576  1424100   0.03 │   0    0    nan │
│        coq-mathcomp-fingroup │   22.25    22.40  -0.67 │   101210970688    101301378242  -0.09 │   151270562872    151242847895   0.02 │  484812   487308  -0.51 │   0    0    nan │
│                coq-fiat-core │   57.27    57.63  -0.62 │   243064574111    243905949913  -0.34 │   358994648767    358959114586   0.01 │  477220   478608  -0.29 │   0    0    nan │
│       coq-mathcomp-ssreflect │   25.79    25.94  -0.58 │   116175240396    116635914713  -0.39 │   152323351664    152228398750   0.06 │  528096   530064  -0.37 │   0    0    nan │
│                 coq-compcert │  292.51   294.08  -0.53 │  1311645649533   1318314424840  -0.51 │  2048981067477   2049000113782  -0.00 │ 1119484  1122884  -0.30 │   0    0    nan │
│             coq-math-classes │   95.23    95.72  -0.51 │   427323270918    430392493774  -0.71 │   629819013709    629812374602   0.00 │  509896   505756   0.82 │   0    0    nan │
│                 coq-rewriter │  329.70   331.15  -0.44 │  1492438940931   1498650819037  -0.41 │  2511373581679   2511467626561  -0.00 │  968916   969212  -0.03 │   0    0    nan │
│          coq-category-theory │ 1649.38  1656.47  -0.43 │  7526726858364   7558785019213  -0.42 │ 15633707589670  15632959331518   0.00 │ 1316240  1316196   0.00 │   0    0    nan │
│               coq-coquelicot │   35.34    35.48  -0.39 │   156919585025    156504018788   0.27 │   216954405082    216825678381   0.06 │  753756   750448   0.44 │   0    0    nan │
│       coq-mathcomp-odd-order │  511.03   512.93  -0.37 │  2331577169289   2339720158593  -0.35 │  4035574519593   4035475704155   0.00 │  861564   939356  -8.28 │   0    0    nan │
│     coq-metacoq-translations │   13.62    13.66  -0.29 │    59918986855     59966774415  -0.08 │    99508282543     99559414305  -0.05 │  746880   746428   0.06 │   0    0    nan │
│  coq-rewriter-perf-SuperFast │  869.39   871.93  -0.29 │  3907538112695   3919125173913  -0.30 │  7058295705552   7058748391446  -0.01 │ 1226844  1226864  -0.00 │   0    0    nan │
│       coq-mathcomp-character │   68.06    68.25  -0.28 │   309375832044    310151130482  -0.25 │   478060111382    478083334438  -0.00 │  724316   723352   0.13 │   0    0    nan │
│         coq-metacoq-template │  136.16   136.41  -0.18 │   605630335510    607126086685  -0.25 │  1013448005840   1015413498737  -0.19 │ 1191768  1194072  -0.19 │   0    0    nan │
│                   coq-stdlib │  421.84   422.60  -0.18 │  1746930144527   1748529105504  -0.09 │  1531978358873   1532146832651  -0.01 │  598436   601488  -0.51 │   0    0    nan │
│        coq-mathcomp-solvable │   82.26    82.39  -0.16 │   372693963756    374083346121  -0.37 │   582306625576    582360067407  -0.01 │  641744   644520  -0.43 │   0    0    nan │
│                    coq-verdi │   47.95    48.01  -0.12 │   214914301614    215301401818  -0.18 │   331395856229    331357073947   0.01 │  777768   778108  -0.04 │   0    0    nan │
│                    coq-color │  227.94   228.19  -0.11 │  1014574588881   1016924681753  -0.23 │  1495570290009   1495466908027   0.01 │ 1042800  1040904   0.18 │   0    0    nan │
│                  coq-unimath │ 4943.17  4948.13  -0.10 │ 22447536129130  22463041779947  -0.07 │ 45398209215570  45397944339062   0.00 │ 3832808  3833336  -0.01 │   0    0    nan │
│                     coq-corn │  793.63   794.32  -0.09 │  3583363581414   3585018609437  -0.05 │  5735109453300   5734934872213   0.00 │  811080   812556  -0.18 │   0    0    nan │
│          coq-metacoq-erasure │  181.42   181.53  -0.06 │   814140014104    815333164439  -0.15 │  1325737034294   1327892694838  -0.16 │ 1473436  1494712  -1.42 │   0    0    nan │
│           coq-mathcomp-field │   97.93    97.95  -0.02 │   445152646674    445740482737  -0.13 │   742030297131    742101332573  -0.01 │  637184   636736   0.07 │   0    0    nan │
│                     coq-hott │  174.11   174.14  -0.02 │   782820674537    781358685127   0.19 │  1266836946979   1266819141449   0.00 │  620704   618660   0.33 │   0    0    nan │
│                coq-perennial │ 3986.71  3984.77   0.05 │ 18021556634548  18015412849614   0.03 │ 30028456866206  30027900614354   0.00 │ 2623920  2622384   0.06 │   0    0    nan │
│ coq-fiat-crypto-with-bedrock │ 5616.32  5610.14   0.11 │ 25300434573949  25288555827775   0.05 │ 46481092108350  46503082454770  -0.05 │ 3839692  3839152   0.01 │   0    0    nan │
│                coq-fourcolor │ 1502.06  1500.34   0.11 │  6644990442807   6634918481925   0.15 │ 12215123227998  12215563285506  -0.00 │  724272   724336  -0.01 │   0    0    nan │
│                  coq-coqutil │   35.85    35.80   0.14 │   159325772363    158501898677   0.52 │   232308710821    232223665607   0.04 │  586148   586140   0.00 │   0    0    nan │
│                  coq-bignums │   28.36    28.32   0.14 │   127621762019    127411716180   0.16 │   183431542897    183430639676   0.00 │  466604   466452   0.03 │   0    0    nan │
│   coq-performance-tests-lite │  807.55   806.28   0.16 │  3612512401713   3602804826381   0.27 │  6372168953830   6373898226368  -0.03 │ 2056584  2056488   0.00 │   0    0    nan │
│            coq-iris-examples │  439.10   438.37   0.17 │  1977228531708   1975155998239   0.10 │  3059171916455   3059413728697  -0.01 │ 1187136  1187264  -0.01 │   0    0    nan │
│        coq-engine-bench-lite │  169.20   168.87   0.20 │   724413272087    722487206552   0.27 │  1386952960942   1382143976207   0.35 │ 1228948  1228896   0.00 │   0    0    nan │
│                   coq-geocoq │  705.84   704.43   0.20 │  3188604040647   3180697779647   0.25 │  5209259614982   5209361248769  -0.00 │  978140   976184   0.20 │   0    0    nan │
│                     coq-core │  110.97   110.74   0.21 │   461402090663    459837410612   0.34 │   483231443756    482833046210   0.08 │  285740   286260  -0.18 │   0    0    nan │
│               coq-verdi-raft │  545.28   543.89   0.26 │  2473121041687   2468212045560   0.20 │  3922838198616   3922538086204   0.01 │ 1200252  1198180   0.17 │   0    0    nan │
│                   coq-flocq3 │   75.01    74.81   0.27 │   338503892985    338284888061   0.06 │   460841502865    460897094841  -0.01 │  991544   991336   0.02 │   0    0    nan │
│                 coq-coqprime │   43.84    43.72   0.27 │   195466725493    195769849540  -0.15 │   302177777552    302291054710  -0.04 │  753876   755272  -0.18 │   0    0    nan │
│             coq-fiat-parsers │  342.26   341.32   0.28 │  1513182338660   1508033814207   0.34 │  2561272963362   2561327296715  -0.00 │ 3442240  3442404  -0.00 │   0    0    nan │
│         coq-mathcomp-algebra │   61.23    60.99   0.39 │   276391500336    275655754652   0.27 │   387433992163    387493191243  -0.02 │  555832   556040  -0.04 │   0    0    nan │
│                 coq-bedrock2 │  373.16   371.43   0.47 │  1674800395579   1666433504150   0.50 │  3284198757311   3284002323027   0.01 │ 1832704  1830656   0.11 │   0    0    nan │
│            coq-metacoq-pcuic │  566.54   563.57   0.53 │  2553817862142   2543148492056   0.42 │  3778071341418   3777974365910   0.00 │ 1927152  1926388   0.04 │   0    0    nan │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

🐢 Top 25 slow downs

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                 TOP 25 SLOW DOWNS                                                                 │
│                                                                                                                                                   │
│   OLD       NEW      DIFF   %DIFF    Ln                      FILE                                                                                 │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 210.1660  211.6950  1.5290   0.73%   139  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│ 120.8410  122.0450  1.2040   1.00%   153  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│ 157.8990  158.7350  0.8360   0.53%   232  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  49.1930   49.7490  0.5560   1.13%    57  coq-category-theory/Construction/Comma/Natural/Transformation.v.html                                    │
│  27.8320   28.2900  0.4580   1.65%    10  coq-fourcolor/theories/job618to622.v.html                                                               │
│ 128.9160  129.3670  0.4510   0.35%   706  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│  14.6120   15.0480  0.4360   2.98%   183  coq-perennial/src/goose_lang/interpreter/disk_interpreter.v.html                                        │
│  20.8800   21.3150  0.4350   2.08%    10  coq-fourcolor/theories/job207to214.v.html                                                               │
│  17.0380   17.4640  0.4260   2.50%   128  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v.html        │
│  19.2780   19.6390  0.3610   1.87%    10  coq-fourcolor/theories/job550to553.v.html                                                               │
│  50.5100   50.8590  0.3490   0.69%    84  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html                                  │
│   1.2380    1.5790  0.3410  27.54%   141  coq-category-theory/Construction/Comma/Adjunction.v.html                                                │
│  76.7920   77.1200  0.3280   0.43%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│  21.8060   22.1330  0.3270   1.50%    10  coq-fourcolor/theories/job239to253.v.html                                                               │
│  17.2800   17.5980  0.3180   1.84%   235  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v.html        │
│  10.6710   10.9850  0.3140   2.94%   911  coq-unimath/UniMath/Bicategories/PseudoFunctors/Examples/CompositionPseudoFunctor.v.html                │
│  62.4980   62.8110  0.3130   0.50%   137  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                            │
│  27.6550   27.9670  0.3120   1.13%  1640  coq-geocoq/Tarski_dev/Ch16_coordinates_with_functions.v.html                                            │
│   3.2230    3.5270  0.3040   9.43%   278  coq-perennial/src/program_proof/examples/async_mem_alloc_dir_proof.v.html                               │
│  18.8860   19.1760  0.2900   1.54%   274  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v.html        │
│  20.4150   20.7030  0.2880   1.41%    10  coq-fourcolor/theories/job315to318.v.html                                                               │
│  47.9310   48.2090  0.2780   0.58%    66  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadder.v.html                         │
│  17.1540   17.4230  0.2690   1.57%   209  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v.html        │
│   0.4690    0.7220  0.2530  53.94%   583  coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html                                             │
│  17.4240   17.6760  0.2520   1.45%   248  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v.html        │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SPEED UPS                                                                │
│                                                                                                                                               │
│   OLD       NEW      DIFF     %DIFF    Ln                     FILE                                                                            │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 108.6290  107.5260  -1.1030   -1.02%  1104  coq-unimath/UniMath/Bicategories/PseudoFunctors/Preservation/BiadjunctionPreserveInserters.v.html │
│  24.3370   23.2980  -1.0390   -4.27%   287  coq-unimath/UniMath/Bicategories/MonoidalCategories/Actions.v.html                                │
│ 131.8500  131.2250  -0.6250   -0.47%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│  41.7430   41.1230  -0.6200   -1.49%   235  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                        │
│ 131.8190  131.2360  -0.5830   -0.44%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│  15.8590   15.4280  -0.4310   -2.72%   594  coq-unimath/UniMath/Algebra/GroupAction.v.html                                                    │
│  24.1230   23.7100  -0.4130   -1.71%  1936  coq-unimath/UniMath/Bicategories/MonoidalCategories/ActionBasedStrongFunctorsMonoidal.v.html      │
│  56.7900   56.4170  -0.3730   -0.66%   820  coq-unimath/UniMath/SubstitutionSystems/LiftingInitial.v.html                                     │
│  18.8830   18.5180  -0.3650   -1.93%    78  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html                │
│  10.0300    9.6730  -0.3570   -3.56%   545  coq-category-theory/Construction/Comma/Adjunction.v.html                                          │
│  41.9010   41.5460  -0.3550   -0.85%   235  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html         │
│  16.0550   15.7250  -0.3300   -2.06%   320  coq-category-theory/Construction/Comma/Adjunction.v.html                                          │
│  19.4580   19.1430  -0.3150   -1.62%   773  coq-category-theory/Construction/Comma/Adjunction.v.html                                          │
│   3.9460    3.6330  -0.3130   -7.93%   279  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomeryReificationCache.v.html  │
│  32.5090   32.2060  -0.3030   -0.93%  1332  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html  │
│  54.8990   54.6080  -0.2910   -0.53%   857  coq-unimath/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.v.html                │
│   6.2580    5.9760  -0.2820   -4.51%   261  coq-unimath/UniMath/Bicategories/MonoidalCategories/Actions.v.html                                │
│  28.3750   28.0940  -0.2810   -0.99%    10  coq-fourcolor/theories/job223to226.v.html                                                         │
│  23.3680   23.0930  -0.2750   -1.18%    10  coq-fourcolor/theories/job307to310.v.html                                                         │
│  10.0460    9.8080  -0.2380   -2.37%   252  coq-unimath/UniMath/Bicategories/Limits/Examples/OpCellBicatLimits.v.html                         │
│   1.2190    1.0020  -0.2170  -17.80%   468  coq-metacoq-pcuic/pcuic/theories/PCUICWfUniverses.v.html                                          │
│   5.4560    5.2460  -0.2100   -3.85%   268  coq-unimath/UniMath/Bicategories/MonoidalCategories/Actions.v.html                                │
│  27.1050   26.8980  -0.2070   -0.76%   736  coq-unimath/UniMath/Bicategories/DisplayedBicats/DispTransformation.v.html                        │
│  27.6920   27.4870  -0.2050   -0.74%    10  coq-fourcolor/theories/job299to302.v.html                                                         │
│  29.7000   29.4950  -0.2050   -0.69%    10  coq-fourcolor/theories/job611to617.v.html                                                         │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

SkySkimmer · 2022-06-18T19:51:07Z

Messed up the testing overlay the first time, let's try this again

SkySkimmer · 2022-06-19T08:19:50Z

It timed out in the Assembly/Symbolic that @ppedrot mentioned on zulip

ppedrot · 2022-06-19T10:00:42Z

Ah! Told you so. I have a partially written fix for this though, I can push it somewhere after some polishing.

JasonGross · 2022-06-19T12:20:14Z

That is very strange, it seems to work fine on our CI https://github.com/mit-plv/fiat-crypto/runs/6943380653?check_suite_focus=true , taking only 34s on master (https://github.com/mit-plv/fiat-crypto/runs/6943380973?check_suite_focus=true#step:7:3159). This might be using an outdated version of master, though, since I haven't gotten around to updating my launchpad packages to have the latest dune, not to fix the issue with configure failing to detect the lablgtk version

ppedrot · 2022-06-19T12:24:44Z

I would be very surprised if this has to do with some recent change on master, though. The problem is basically the same as the exponential blowup of the reduced type for extraction. Here we're performing a (nonsensical) recursive analysis of nested inductive types to compute equality schemes, and since it reduces the constructor types, you get the blowup as well.

SkySkimmer · 2022-06-19T12:49:49Z

It's the Symbolic version in mit-plv/fiat-crypto#1293 that's got an issue not the fiat-crypto master version. You can see it fail on that PR's CI too.

JasonGross · 2022-06-19T12:58:01Z

Oh, I see, that makes sense. I guess the version I was timing the commit on was old enough (8.14, maybe? Or 8.11?) that it wasn't generating equality schemes for records, or something like that, and hence on that certain Symbolic went from 30s to 26s. I'll probably disable scheme generation for that record when I actually merge the PR (and/or will make the type not exponentially sized).

Should help with performance issues of rocq-prover/rocq#16206 (comment)

JasonGross · 2022-06-22T22:10:49Z

Ah! Told you so. I have a partially written fix for this though, I can push it somewhere after some polishing.

@ppedrot Should we open a separate issue to track this?

I've pushed an update to mit-plv/fiat-crypto#1293 disabling the equality generation and I've restarted the CI here. I've also opened rocq-community/coq-performance-tests#22 with the smaller examples

Should help with performance issues of rocq-prover/rocq#16206 (comment)

JasonGross · 2022-06-24T13:48:04Z

Seems to work!

      Time |   Peak Mem | File Name                       
------------------------------------------------------------------------------------------------------
  0m50.12s | 2330152 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
  0m50.12s | 2330648 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
  0m48.75s | 2287600 ko | ExtractionOCaml/word_by_word_montgomery.ml
  0m33.02s | 1988808 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
  0m32.82s | 1988728 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
  0m30.68s | 1871988 ko | ExtractionOCaml/unsaturated_solinas.ml
  0m27.56s | 1828552 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
  0m27.51s | 1849064 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
  0m27.42s | 1828688 ko | ExtractionOCaml/bedrock2_base_conversion.ml
  0m27.15s | 1848784 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
  0m25.41s | 1769136 ko | ExtractionOCaml/saturated_solinas.ml
  0m25.26s | 1734456 ko | ExtractionOCaml/base_conversion.ml
  0m23.38s | 1751072 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
  0m22.28s | 1707496 ko | ExtractionOCaml/perf_unsaturated_solinas.ml

JasonGross · 2022-06-24T13:48:39Z

Er, wait, was that run without the overlay pointing it at the right branch?

JasonGross · 2022-06-24T13:49:37Z

Could you re-add the overlay and we can test this here?

JasonGross · 2022-07-04T10:04:44Z

Ping @SkySkimmer

Fix rocq-prover#16172

SkySkimmer · 2022-07-04T14:37:31Z

@JasonGross looks like something extracted wrongly, can you minimize?

JasonGross · 2022-07-05T16:24:08Z

Gah, I did not realize that the CI merges the overlay with the current master, I guess I'll have to adjust the overlay branch

JasonGross · 2022-07-05T16:29:48Z

I still have to look into the failures at the OCaml job and the underlying fiat-crypto job, but let me try running this with the intended branch

JasonGross · 2022-07-05T17:40:07Z

@SkySkimmer Minimized: #16288 This issue is already present in master, it was just exposed here by merging the overlay branch into fiat-crypto's master

JasonGross · 2022-07-05T20:06:03Z

@SkySkimmer CI looks to be building fiat-crypto fine now, and this PR seems to fix the issue:

      Time |   Peak Mem | File Name             
---------------------------------------------------------------------------------------------------------
  0m55.07s | 2347376 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml
  0m55.02s | 2347808 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml
  0m52.72s | 2332244 ko | ExtractionOCaml/word_by_word_montgomery.ml
  0m37.16s | 2023224 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml
  0m37.10s | 2022888 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml
  0m35.08s | 1909716 ko | ExtractionOCaml/unsaturated_solinas.ml
  0m31.97s | 1948772 ko | ExtractionOCaml/bedrock2_base_conversion.ml
  0m31.92s | 1948516 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml
  0m31.66s | 1899424 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml
  0m31.26s | 1899196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml
  0m29.98s | 1808244 ko | ExtractionOCaml/base_conversion.ml
  0m29.78s | 1853300 ko | ExtractionOCaml/saturated_solinas.ml
  0m26.05s | 1803544 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml
  0m24.63s | 1771960 ko | ExtractionOCaml/perf_unsaturated_solinas.ml

Shall we merge, or do you want a formal bench?

Alizter · 2022-07-09T14:04:41Z

@JasonGross Do you want this in 8.16? If we ask @ppedrot nicely he might agree.

JasonGross · 2022-07-09T16:37:53Z

It would be nice to have in 8.16, but I don't feel particularly strongly

Alizter · 2022-07-09T17:24:20Z

@ppedrot Please consider this for 8.16, but no biggie.

Alizter · 2022-07-09T17:24:28Z

@coqbot merge now

coqbot-app · 2022-07-09T17:24:31Z

@Alizter: Please take care of the following overlays:

16206-extraction-less-recurse.sh

Alizter · 2022-07-09T17:49:22Z

@SkySkimmer Where is the overlay?

SkySkimmer · 2022-07-09T18:12:30Z

It's not a real overlay, it's only for testing

SkySkimmer requested a review from a team as a code owner June 17, 2022 12:28

SkySkimmer force-pushed the extraction-less-recurse branch from 399e865 to 2168253 Compare June 18, 2022 19:50

JasonGross added a commit to JasonGross/fiat-crypto that referenced this pull request Jun 22, 2022

Disable equality schemes for symbolic_state

d21e8a1

Should help with performance issues of rocq-prover/rocq#16206 (comment)

JasonGross mentioned this pull request Jun 22, 2022

Disable equality schemes for symbolic_state mit-plv/fiat-crypto#1306

Merged

JasonGross added a commit to mit-plv/fiat-crypto that referenced this pull request Jun 23, 2022

Disable equality schemes for symbolic_state (#1306)

d563f21

Should help with performance issues of rocq-prover/rocq#16206 (comment)

SkySkimmer force-pushed the extraction-less-recurse branch from 2168253 to e88f586 Compare June 23, 2022 06:32

SkySkimmer added 2 commits July 4, 2022 12:19

Recurse less in extraction

81ae126

Fix rocq-prover#16172

testing

48d0b8a

SkySkimmer force-pushed the extraction-less-recurse branch from e88f586 to 48d0b8a Compare July 4, 2022 10:19

JasonGross mentioned this pull request Jul 5, 2022

Scheme Equality depends on the size of the fully reduced type when it should not #16290

Open

Alizter approved these changes Jul 9, 2022

View reviewed changes

Alizter self-assigned this Jul 9, 2022

Alizter added kind: fix This fixes a bug or incorrect documentation. part: extraction The extraction mechanism. labels Jul 9, 2022

Alizter added this to the 8.17+rc1 milestone Jul 9, 2022

Alizter modified the milestones: 8.17+rc1, 8.16.0 Jul 9, 2022

coqbot-app Bot merged commit 8cfcd27 into rocq-prover:master Jul 9, 2022

SkySkimmer deleted the extraction-less-recurse branch July 10, 2022 18:59

ppedrot added a commit to ppedrot/coq that referenced this pull request Jul 21, 2022

Backport PR rocq-prover#16206: Recurse less in extraction

db1f12a

Conversation

SkySkimmer commented Jun 17, 2022

Uh oh!

SkySkimmer commented Jun 17, 2022

Uh oh!

SkySkimmer commented Jun 17, 2022

Uh oh!

JasonGross commented Jun 17, 2022

Uh oh!

coqbot-app Bot commented Jun 18, 2022

Uh oh!

SkySkimmer commented Jun 18, 2022

Uh oh!

SkySkimmer commented Jun 19, 2022

Uh oh!

ppedrot commented Jun 19, 2022

Uh oh!

JasonGross commented Jun 19, 2022

Uh oh!

ppedrot commented Jun 19, 2022

Uh oh!

SkySkimmer commented Jun 19, 2022

Uh oh!

JasonGross commented Jun 19, 2022

Uh oh!

JasonGross commented Jun 22, 2022

Uh oh!

JasonGross commented Jun 24, 2022

Uh oh!

JasonGross commented Jun 24, 2022

Uh oh!

JasonGross commented Jun 24, 2022

Uh oh!

JasonGross commented Jul 4, 2022

Uh oh!

SkySkimmer commented Jul 4, 2022

Uh oh!

JasonGross commented Jul 5, 2022

Uh oh!

JasonGross commented Jul 5, 2022

Uh oh!

JasonGross commented Jul 5, 2022

Uh oh!

JasonGross commented Jul 5, 2022

Uh oh!

Alizter commented Jul 9, 2022

Uh oh!

JasonGross commented Jul 9, 2022

Uh oh!

Alizter commented Jul 9, 2022

Uh oh!

Alizter commented Jul 9, 2022

Uh oh!

coqbot-app Bot commented Jul 9, 2022

Uh oh!

Alizter commented Jul 9, 2022

Uh oh!

SkySkimmer commented Jul 9, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants