Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Code factorization around Evarutil.finalize and prepare_obligations #19050

Merged
merged 3 commits into from
May 24, 2024
Merged

Code factorization around Evarutil.finalize and prepare_obligations #19050

merged 3 commits into from
May 24, 2024

Conversation

herbelin
Copy link
Member

@herbelin herbelin commented May 17, 2024 •
edited
Loading

The PR experiments:

  1. using Evarutil.finalize in.wf-based Program Fixpoint (what ensures minimization of universes of the main obligation-based constant)
  2. changing the flow of control so that finalize for definition is called without the abort flag to false

I suspect 1.a. to be observable but I don't know well how to build an example (is there a standard example to observe minimization?)

Note also that this is only an intermediate step. See coq/ceps#89 for further possible steps.

  • Added / updated test-suite.

@herbelin herbelin added the kind: cleanup Code removal, deprecation, refactorings, etc. label May 17, 2024
@herbelin herbelin added this to the 8.20+rc1 milestone May 17, 2024
@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 17, 2024
@herbelin
Using Declare.prepare_obligations in Program Fixpoing wf/measure.
d41b8fa 
This ensures a similar treatment as in other places, e.g. that
universes are minimized and restricted in the main obligations-based
constant as done for definitions.
@herbelin
Reorganizing prepare_definition to avoid calling finalize possibly wi…
dfb1448 
…th evars.
@herbelin herbelin force-pushed the master+prepare_obligation-in-program-fixpoint-wf branch from 71da4bb to dfb1448 Compare May 17, 2024 19:26
@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 17, 2024
@herbelin herbelin added the request: full CI Use this label when you want your next push to trigger a full CI. label May 20, 2024
@herbelin
Copy link
Member Author

@coqbot run full ci

@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels May 20, 2024
@herbelin herbelin added the part: universes The universe system. label May 20, 2024
@herbelin herbelin marked this pull request as ready for review May 20, 2024 12:49
@herbelin herbelin requested a review from a team as a code owner May 20, 2024 12:49
SkySkimmer
SkySkimmer reviewed May 23, 2024
View reviewed changes
vernac/declare.ml Outdated Show resolved Hide resolved
@SkySkimmer SkySkimmer self-assigned this May 23, 2024
@SkySkimmer
Copy link
Contributor

@coqbot bench

@herbelin @SkySkimmer
Update vernac/declare.ml
e8f4099 
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
@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 May 23, 2024
@coqbot-app coqbot-app
Copy link
Contributor

coqbot-app bot commented May 24, 2024

🏁 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-mathcomp-field │  141.24   143.48  -1.56 │   645300626093    654322553277  -1.38 │  1073671385492   1073677771934  -0.00 │ 1435988  1438204  -0.15 │
│               coq-engine-bench-lite │  155.65   157.65  -1.27 │   662475362470    667011586726  -0.68 │  1225512511218   1223910905440   0.13 │ 1324428  1321136   0.25 │
│              coq-mathcomp-odd-order │  781.15   790.30  -1.16 │  3576254754983   3618846281713  -1.18 │  6077856886021   6078381758692  -0.01 │ 1664932  1665420  -0.03 │
│                        coq-bedrock2 │  358.90   362.69  -1.04 │  1636096640128   1652352833479  -0.98 │  3110480539784   3110424927643   0.00 │  863896   860548   0.39 │
│                            coq-core │  128.58   129.74  -0.89 │   506644583275    504315016551   0.46 │   531740333923    531645860159   0.02 │  458260   456852   0.31 │
│                       coq-fourcolor │ 1394.81  1405.36  -0.75 │  6380051107545   6429575076965  -0.77 │ 13511260688707  13511553295362  -0.00 │ 2139684  2137684   0.09 │
│                coq-mathcomp-algebra │  258.24   260.03  -0.69 │  1178261837681   1185634285688  -0.62 │  1999573069820   1999519621806   0.00 │ 1334928  1334864   0.00 │
│              coq-mathcomp-ssreflect │  219.77   221.20  -0.65 │  1003263966949   1010325979449  -0.70 │  1676004678112   1676050822052  -0.00 │ 1743244  1743236   0.00 │
│              coq-mathcomp-character │  108.82   109.49  -0.61 │   497047667404    500335267323  -0.66 │   790232969348    790244277331  -0.00 │ 1128384  1128680  -0.03 │
│            coq-metacoq-translations │   16.91    17.01  -0.59 │    75842357736     75893581924  -0.07 │   124578923084    124554967226   0.02 │  843336   843512  -0.02 │
│                         coq-unimath │ 2569.04  2579.74  -0.41 │ 11698810216422  11746098887483  -0.40 │ 23109246005618  23111642914911  -0.01 │ 1273056  1274652  -0.13 │
│               coq-mathcomp-fingroup │   30.68    30.80  -0.39 │   139088379479    139841402531  -0.54 │   207747995886    207755836690  -0.00 │  569160   569184  -0.00 │
│                           coq-color │  252.58   253.10  -0.21 │  1135990714630   1137224187816  -0.11 │  1633030942630   1632964229772   0.00 │ 1183492  1186840  -0.28 │
│                        coq-rewriter │  388.31   388.95  -0.16 │  1766010515570   1766532837602  -0.03 │  2990133698450   2990155922193  -0.00 │ 1483620  1484144  -0.04 │
│                 coq-category-theory │  660.67   661.62  -0.14 │  3002806796955   3006822287010  -0.13 │  4925640825032   4925086630244   0.01 │  976372   977252  -0.09 │
│                    coq-math-classes │   86.33    86.39  -0.07 │   388124299663    387899289728   0.06 │   536890784398    536886242035   0.00 │  504036   503196   0.17 │
│                            coq-hott │  162.25   162.36  -0.07 │   725891447873    726200379826  -0.04 │  1151582732286   1151629858561  -0.00 │  480652   479148   0.31 │
│               coq-mathcomp-solvable │  119.23   119.26  -0.03 │   544342602090    544981624278  -0.12 │   857132244668    857115611766   0.00 │  881024   883080  -0.23 │
│                      coq-coquelicot │   39.75    39.72   0.08 │   176879872728    176529291530   0.20 │   249339944367    249358706083  -0.01 │  852936   857176  -0.49 │
│                 coq-metacoq-erasure │  534.09   533.45   0.12 │  2438107264637   2432578235642   0.23 │  3811581226477   3811622365135  -0.00 │ 2103380  2104220  -0.04 │
│        coq-fiat-crypto-with-bedrock │ 6231.26  6223.33   0.13 │ 28384096477698  28350268641433   0.12 │ 51226932575738  51226624750197   0.00 │ 3246128  3246192  -0.00 │
│                    coq-fiat-parsers │  313.87   313.28   0.19 │  1399640442784   1398097185944   0.11 │  2488425576865   2488308990468   0.00 │ 2416880  2416424   0.02 │
│                       coq-equations │   12.01    11.98   0.25 │    50860837810     50686304992   0.34 │    79607440442     79582590585   0.03 │  427536   427108   0.10 │
│                        coq-coqprime │   48.46    48.32   0.29 │   217583174297    216227861631   0.63 │   334676319090    334638343390   0.01 │  785172   785364  -0.02 │
│                coq-metacoq-template │  151.04   150.57   0.31 │   669650905809    667315157394   0.35 │  1045593412657   1045491235711   0.01 │ 1507616  1509920  -0.15 │
│                           coq-verdi │   49.17    49.00   0.35 │   220855728953    220133225453   0.33 │   340812105361    340791741869   0.01 │  529092   530120  -0.19 │
│                         coq-bignums │   29.41    29.30   0.38 │   133306087996    133059829363   0.19 │   192207828141    192222449395  -0.01 │  478332   478076   0.05 │
│          coq-performance-tests-lite │  709.95   707.05   0.41 │  3205411817800   3193441236835   0.37 │  5686694923835   5687431205310  -0.01 │ 2275296  2274552   0.03 │
│         coq-rewriter-perf-SuperFast │  790.84   787.40   0.44 │  3595296296530   3578166943257   0.48 │  6257636757768   6257558801360   0.00 │ 1579312  1581488  -0.14 │
│ coq-neural-net-interp-computed-lite │  299.40   297.78   0.54 │  1366581394154   1359420763845   0.53 │  3618460935001   3618385967687   0.00 │ 1119048  1113140   0.53 │
│                          coq-stdlib │  350.54   348.61   0.55 │  1492750360485   1484608023630   0.55 │  1258566609694   1258558265048   0.00 │  719396   719548  -0.02 │
│             coq-metacoq-safechecker │  419.90   417.46   0.58 │  1922726289176   1910865486915   0.62 │  3176340920821   3177335715202  -0.03 │ 2061316  2063892  -0.12 │
│                            coq-corn │  723.45   718.86   0.64 │  3283998755550   3265028304418   0.58 │  5076473115504   5076400453927   0.00 │  789144   789000   0.02 │
│                        coq-compcert │  282.49   280.63   0.66 │  1277349003832   1269659693025   0.61 │  1944444989998   1944384503840   0.00 │ 1107524  1108992  -0.13 │
│                   coq-metacoq-pcuic │  990.24   982.22   0.82 │  4433730713930   4403721445463   0.68 │  6468730401275   6468281956301   0.01 │ 2678420  2680560  -0.08 │
│                         coq-coqutil │   43.08    42.69   0.91 │   189580860386    188415442669   0.62 │   271070864703    270995672780   0.03 │  561476   560960   0.09 │
│                             coq-vst │  882.61   874.52   0.93 │  4013096606053   3975365861385   0.95 │  6738927557716   6738830454069   0.00 │ 2238604  2234580   0.18 │
│                   coq-iris-examples │  470.95   466.46   0.96 │  2141375209913   2121367828964   0.94 │  3277879711689   3277734899511   0.00 │ 1119204  1115360   0.34 │
│                      coq-verdi-raft │  585.19   579.28   1.02 │  2661836319305   2637548192932   0.92 │  4162135558813   4161961509123   0.00 │  850420   850188   0.03 │
│                       coq-fiat-core │   59.97    59.23   1.25 │   250196725164    247544305179   1.07 │   368796427909    368859698430  -0.02 │  484088   482624   0.30 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-test-suite

🐢 Top 25 slow downs 
┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                 TOP 25 SLOW DOWNS                                                                 │
│                                                                                                                                                   │
│   OLD       NEW      DIFF   %DIFF    Ln                      FILE                                                                                 │
├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 215.8670  221.4600  5.5930   2.59%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                     │
│ 180.4470  184.0040  3.5570   1.97%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│ 254.8370  257.7240  2.8870   1.13%  1629  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                                                         │
│ 255.7150  257.4500  1.7350   0.68%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│ 241.8400  243.4990  1.6590   0.69%   141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  25.6130   26.7610  1.1480   4.48%   129  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html                                   │
│ 138.5450  139.5980  1.0530   0.76%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  27.1580   28.1000  0.9420   3.47%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html      │
│  72.8130   73.4860  0.6730   0.92%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                                    │
│  11.9160   12.5230  0.6070   5.09%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│  22.6470   23.2300  0.5830   2.57%  1073  coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html                                     │
│   3.3090    3.7590  0.4500  13.60%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                              │
│  17.8570   18.2600  0.4030   2.26%   708  coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html                                            │
│  29.8580   30.2590  0.4010   1.34%   194  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│  44.2340   44.6200  0.3860   0.87%   827  coq-vst/veric/binop_lemmas4.v.html                                                                      │
│  30.7120   31.0560  0.3440   1.12%   147  coq-vst/veric/expr_lemmas4.v.html                                                                       │
│  14.1570   14.4860  0.3290   2.32%  1204  coq-vst/floyd/Component.v.html                                                                          │
│  14.1550   14.4780  0.3230   2.28%  1505  coq-vst/floyd/VSU.v.html                                                                                │
│  26.6130   26.9080  0.2950   1.11%    17  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│  14.1740   14.4490  0.2750   1.94%  1218  coq-vst/floyd/Component.v.html                                                                          │
│  26.6230   26.8960  0.2730   1.03%    22  coq-fiat-crypto-with-bedrock/src/Spec/Test/X25519.v.html                                                │
│   0.5210    0.7920  0.2710  52.02%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                                                                │
│   0.3190    0.5850  0.2660  83.39%   868  coq-stdlib/MSets/MSetRBT.v.html                                                                         │
│   7.8820    8.1250  0.2430   3.08%  1265  coq-verdi-raft/theories/Raft/CommonTheorems.v.html                                                      │
│  24.1130   24.3500  0.2370   0.98%    85  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html                                  │
└───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SPEED UPS                                                               │
│                                                                                                                                              │
│   OLD       NEW     DIFF     %DIFF    Ln                     FILE                                                                            │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  82.6910  76.9970  -5.6940   -6.89%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                 │
│  68.5080  63.8770  -4.6310   -6.76%   368  coq-mathcomp-odd-order/theories/PFsection4.v.html                                                 │
│  47.7660  46.4590  -1.3070   -2.74%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                        │
│  62.2180  61.0270  -1.1910   -1.91%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                       │
│  63.0480  62.1190  -0.9290   -1.47%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html     │
│   3.2960   2.4320  -0.8640  -26.21%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                                        │
│  17.4940  16.6620  -0.8320   -4.76%   607  coq-mathcomp-odd-order/theories/PFsection9.v.html                                                 │
│ 100.3310  99.6280  -0.7030   -0.70%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                       │
│  81.5320  80.9190  -0.6130   -0.75%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                           │
│   7.1180   6.5440  -0.5740   -8.06%  1933  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Profunctors/Composition/CompositionProf.v.html    │
│  46.6570  46.0930  -0.5640   -1.21%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html      │
│  47.8380  47.2820  -0.5560   -1.16%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│  98.3080  97.7600  -0.5480   -0.56%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                       │
│  20.1930  19.6520  -0.5410   -2.68%   214  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                              │
│  27.8990  27.3730  -0.5260   -1.89%    12  coq-fourcolor/theories/job287to290.v.html                                                         │
│  24.2560  23.7640  -0.4920   -2.03%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                           │
│  12.0190  11.5320  -0.4870   -4.05%  2103  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                            │
│  25.5630  25.0800  -0.4830   -1.89%    12  coq-fourcolor/theories/job299to302.v.html                                                         │
│   1.4320   0.9950  -0.4370  -30.52%   854  coq-stdlib/FSets/FMapAVL.v.html                                                                   │
│  19.6430  19.2180  -0.4250   -2.16%   957  coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v.html            │
│  36.3460  35.9300  -0.4160   -1.14%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                           │
│  27.1890  26.7760  -0.4130   -1.52%    12  coq-fourcolor/theories/job611to617.v.html                                                         │
│  22.8550  22.4630  -0.3920   -1.72%    12  coq-fourcolor/theories/job303to306.v.html                                                         │
│  13.0730  12.6960  -0.3770   -2.88%  1555  coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html                                       │
│  29.8130  29.4440  -0.3690   -1.24%    12  coq-fourcolor/theories/job323to383.v.html                                                         │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@SkySkimmer SkySkimmer 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 24, 2024
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 34411e9 into coq:master May 24, 2024
6 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer approved these changes

Assignees

@SkySkimmer SkySkimmer

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. part: universes The universe system.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@herbelin @SkySkimmer