Revert "Stop doing early universe minimization and nf_evar in abstract" #18640

SkySkimmer · 2024-02-08T12:37:04Z

This reverts commit fea5fcc.

silene · 2024-02-08T13:06:41Z

I have tested these two commits on top of the v8.19 branch, and my larger developments now go through. Among other things, they fix some random failures I was experiencing with auto with zarith (which makes sense, as it uses abstract).

Morally we consider them part of the body univs. Fix coq#18636 (alternative to coq#18640, but this probably isn't as good a candidate for backporting)

Morally we consider them part of the body univs. This makes it so we don't need to disregard keep_body_ucst_separate when there are side effects. Fix coq#18636 (alternative to coq#18640, but this probably isn't as good a candidate for backporting)

ppedrot · 2024-02-08T14:27:14Z

We should probably @coqbot bench

Fixed by reverting fea5fcc The reason the first abstract changes the behaviour is that it changes which branch we take in https://github.com/coq/coq/blob/3d86c1d4569b0a25a00677833b9f47c3059a8345/vernac/declare.ml#L1826 Why we have this code is not clear but removing it (so it becomes just `if not poly && keep_body_ucst_separate`) causes undefined universe anomaly at https://github.com/coq/coq/blob/3d86c1d4569b0a25a00677833b9f47c3059a8345/test-suite/success/rewrite.v#L50 In any case with this code and fea5fcc (indeed from coq#17745) we use an unminimized initial_euctx which has `{foo.5} |= Set = foo.5` which is added to the global env (we are in univ monomorphic mode), and since monomorphic universes are declared `> Set` we get the error. I guess short term we should revert fea5fcc and long term we should look into not checking is_empty_private_constants.

SkySkimmer · 2024-02-09T11:40:48Z

just added changelog

coqbot-app · 2024-02-09T14:36:14Z

🏁 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-stdlib │  364.95   370.50  -1.50 │  1512915972371   1530590416764  -1.15 │  1331512164005   1331437145232   0.01 │  735804   740164  -0.59 │
│                        coq-rewriter │  401.36   404.91  -0.88 │  1803762205515   1820929721898  -0.94 │  2978999607035   2991051298699  -0.40 │ 1501376  1501540  -0.01 │
│                             coq-vst │  857.22   862.72  -0.64 │  3869743272767   3893621163315  -0.61 │  6568651236138   6566334279213   0.04 │ 2468660  2466964   0.07 │
│                           coq-color │  236.49   237.72  -0.52 │  1055255184356   1058351954188  -0.29 │  1566899009837   1564313808961   0.17 │ 1221548  1222032  -0.04 │
│                 coq-metacoq-erasure │  503.19   505.41  -0.44 │  2276531542402   2285181024196  -0.38 │  3573754745066   3577242852543  -0.10 │ 1829500  1821772   0.42 │
│                coq-metacoq-template │  148.24   148.79  -0.37 │   650824126111    653633680080  -0.43 │  1026544890097   1026281921350   0.03 │ 1162052  1158940   0.27 │
│                        coq-bedrock2 │  386.69   388.10  -0.36 │  1747403102525   1753437474030  -0.34 │  3396037056851   3395017168132   0.03 │  962280   961876   0.04 │
│              coq-mathcomp-ssreflect │  111.80   112.15  -0.31 │   503462461501    505094479538  -0.32 │   803244342504    803253839413  -0.00 │ 1319040  1321236  -0.17 │
│                    coq-math-classes │   85.28    85.51  -0.27 │   381520908834    381509467659   0.00 │   530686194645    530778155304  -0.02 │  517192   516960   0.04 │
│                   coq-iris-examples │  466.16   467.23  -0.23 │  2107282339279   2111635002924  -0.21 │  3247778287558   3247938209801  -0.00 │ 1102324  1100548   0.16 │
│                      coq-coquelicot │   39.57    39.66  -0.23 │   174525835354    175184052004  -0.38 │   248497142143    248130492827   0.15 │  852848   855604  -0.32 │
│              coq-mathcomp-odd-order │  765.65   767.16  -0.20 │  3490809918230   3498012642732  -0.21 │  5980801243821   5980508486752   0.00 │ 1625964  1624128   0.11 │
│                                 coq │  728.30   729.01  -0.10 │  3046939452260   3057986914790  -0.36 │  5423089614041   5427359755848  -0.08 │ 2426992  2426320   0.03 │
│                         coq-coqutil │   41.86    41.90  -0.10 │   182977864451    182807833170   0.09 │   265513558033    265522494739  -0.00 │  569400   569896  -0.09 │
│                       coq-fourcolor │ 1358.25  1359.51  -0.09 │  6171942563046   6177867791523  -0.10 │ 12149407458311  12149421418987  -0.00 │ 2199612  2201300  -0.08 │
│                         coq-unimath │ 1914.88  1915.98  -0.06 │  8656205916637   8659794519096  -0.04 │ 16824044835131  16807061316794   0.10 │ 1334200  1343900  -0.72 │
│             coq-metacoq-safechecker │  416.84   416.87  -0.01 │  1901188158941   1900623066295   0.03 │  3182204113387   3183352928529  -0.04 │ 1892632  1889236   0.18 │
│                        coq-compcert │  280.68   280.66   0.01 │  1260014016458   1258819177712   0.09 │  1937070634337   1935686555664   0.07 │ 1136064  1135740   0.03 │
│        coq-fiat-crypto-with-bedrock │ 5863.46  5860.75   0.05 │ 26517181854906  26507574725602   0.04 │ 48303482247967  48327343362769  -0.05 │ 2827460  2827380   0.00 │
│         coq-rewriter-perf-SuperFast │  798.77   798.14   0.08 │  3560121859246   3561356177337  -0.03 │  6209731523808   6194282902690   0.25 │ 1593488  1592904   0.04 │
│                  coq-mathcomp-field │  141.64   141.51   0.09 │   638145085387    638384413753  -0.04 │  1061080243623   1061116332593  -0.00 │ 1365544  1365704  -0.01 │
│                    coq-fiat-parsers │  310.84   310.53   0.10 │  1374583743201   1373838435061   0.05 │  2416310098469   2414183428990   0.09 │ 3044792  3051720  -0.23 │
│                        coq-coqprime │   48.15    48.10   0.10 │   214653533164    215202541993  -0.26 │   331067097135    331106401181  -0.01 │  792752   792624   0.02 │
│                 coq-category-theory │  764.41   763.51   0.12 │  3462850135077   3457846001597   0.14 │  5783301071530   5782875243573   0.01 │  997652   996544   0.11 │
│                            coq-core │  129.09   128.93   0.12 │   480693991162    478965997292   0.36 │   523381099053    523213410080   0.03 │  436440   436900  -0.11 │
│                            coq-hott │  152.77   152.48   0.19 │   673771671192    673425878012   0.05 │  1071448094172   1071949502982  -0.05 │  528600   528636  -0.01 │
│               coq-mathcomp-fingroup │   30.69    30.63   0.20 │   139216804495    138899221190   0.23 │   208561411813    208540268121   0.01 │  567940   569176  -0.22 │
│                            coq-corn │  729.42   727.62   0.25 │  3291470215297   3283773834449   0.23 │  5067994880688   5063635916649   0.09 │  811876   812276  -0.05 │
│                       coq-equations │    7.89     7.87   0.25 │    32377570438     32292286771   0.26 │    52516675745     52505420127   0.02 │  387048   386792   0.07 │
│          coq-performance-tests-lite │  702.13   699.55   0.37 │  3139983503295   3127455580233   0.40 │  5583599383238   5581258822087   0.04 │ 1751468  1751780  -0.02 │
│              coq-mathcomp-character │  104.13   103.71   0.40 │   473117155534    470524264672   0.55 │   747673550620    747719407004  -0.01 │ 1070428  1070352   0.01 │
│               coq-engine-bench-lite │  157.45   156.79   0.42 │   659266772792    657105542489   0.33 │  1217825691122   1217275467387   0.05 │ 1263380  1263516  -0.01 │
│ coq-neural-net-interp-computed-lite │  292.80   291.48   0.45 │  1335136623851   1328435856769   0.50 │  3419993939587   3420003672966  -0.00 │ 1118964  1115352   0.32 │
│                   coq-metacoq-pcuic │  788.62   784.80   0.49 │  3551655508132   3535543544456   0.46 │  5359285399310   5341127459642   0.34 │ 2407300  2383944   0.98 │
│                coq-mathcomp-algebra │  281.58   280.14   0.51 │  1268822735859   1263482573259   0.42 │  2105252989327   2105281926108  -0.00 │ 1332476  1332624  -0.01 │
│               coq-mathcomp-solvable │  117.93   117.25   0.58 │   536087722144    533208176296   0.54 │   849471452162    849491516219  -0.00 │  863184   859552   0.42 │
│                      coq-verdi-raft │  586.81   581.91   0.84 │  2661818182076   2640061140088   0.82 │  4176467976219   4162100218167   0.35 │  874516   872352   0.25 │
│                           coq-verdi │   49.83    49.29   1.10 │   222239967411    220237321238   0.91 │   343161794258    342463098323   0.20 │  535156   533908   0.23 │
│                       coq-fiat-core │   60.33    59.65   1.14 │   247712505724    245368410519   0.96 │   369695291497    367409025903   0.62 │  481552   483292  -0.36 │
│                         coq-bignums │   29.96    29.45   1.73 │   134979630679    133006248144   1.48 │   192750581319    192717740955   0.02 │  485768   485912  -0.03 │
│            coq-metacoq-translations │   17.21    16.91   1.77 │    75085761550     74636647243   0.60 │   124299380781    124352593556  -0.04 │  858392   857736   0.08 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                             │
│   OLD       NEW      DIFF   %DIFF    Ln                     FILE                                                                            │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 250.5120  251.9870  1.4750   0.59%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html     │
│ 150.8370  151.9040  1.0670   0.71%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                     │
│  62.2650   63.2840  1.0190   1.64%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html     │
│   3.1020    3.9830  0.8810  28.40%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                             │
│   8.6970    9.5000  0.8030   9.23%   447  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html            │
│ 100.5370  101.3270  0.7900   0.79%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                       │
│  46.7820   47.5170  0.7350   1.57%   558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │
│  11.0670   11.7960  0.7290   6.59%   410  coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html                              │
│  22.3910   22.9600  0.5690   2.54%   595  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                     │
│  96.1950   96.7200  0.5250   0.55%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│   2.2270    2.7240  0.4970  22.32%   490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                        │
│ 130.4550  130.9430  0.4880   0.37%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                            │
│   0.5230    0.9930  0.4700  89.87%   291  coq-metacoq-pcuic/pcuic/theories/PCUICContextConversion.v.html                                    │
│  96.1480   96.6140  0.4660   0.48%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│  33.9960   34.4530  0.4570   1.34%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html                │
│  24.3490   24.7890  0.4400   1.81%    85  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html                            │
│   9.2280    9.6350  0.4070   4.41%   420  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                              │
│   3.0300    3.4310  0.4010  13.23%   757  coq-fiat-crypto-with-bedrock/src/AbstractInterpretation/ZRangeProofs.v.html                       │
│  33.7720   34.1680  0.3960   1.17%    79  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │
│   0.5260    0.8890  0.3630  69.01%   265  coq-metacoq-pcuic/pcuic/theories/PCUICContextConversion.v.html                                    │
│   0.8110    1.1540  0.3430  42.29%   384  coq-stdlib/MSets/MSetAVL.v.html                                                                   │
│  79.3800   79.6960  0.3160   0.40%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                           │
│   0.5970    0.9090  0.3120  52.26%  1073  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html            │
│  17.8120   18.1120  0.3000   1.68%    32  coq-performance-tests-lite/src/pattern.v.html                                                     │
│   8.8750    9.1620  0.2870   3.23%  3269  coq-fiat-crypto-with-bedrock/src/Assembly/WithBedrock/Proofs.v.html                               │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                            │
│                                                                                                                                        │
│   OLD      NEW     DIFF     %DIFF    Ln                    FILE                                                                        │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 65.5410  63.0580  -2.4830   -3.79%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                  │
│ 67.9390  67.0530  -0.8860   -1.30%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                     │
│ 13.3060  12.4270  -0.8790   -6.61%    82  coq-rewriter/src/Rewriter/Rewriter/Examples.v.html                                           │
│  3.9990   3.1580  -0.8410  -21.03%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                     │
│ 95.2130  94.5230  -0.6900   -0.72%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                          │
│ 13.3920  12.7420  -0.6500   -4.85%    88  coq-rewriter/src/Rewriter/Rewriter/Examples.v.html                                           │
│  9.5490   8.9460  -0.6030   -6.31%   952  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html       │
│ 33.7150  33.1270  -0.5880   -1.74%   839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                │
│ 18.2160  17.6590  -0.5570   -3.06%    61  coq-rewriter/src/Rewriter/Rewriter/Examples/PrefixSums.v.html                                │
│  6.7630   6.2230  -0.5400   -7.98%    23  coq-rewriter/src/Rewriter/Demo.v.html                                                        │
│  8.7660   8.2300  -0.5360   -6.11%    34  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v.html                     │
│ 11.2810  10.7590  -0.5220   -4.63%    79  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                   │
│  8.7510   8.2300  -0.5210   -5.95%    27  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v.html │
│ 11.2030  10.7020  -0.5010   -4.47%    79  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html    │
│ 18.3380  17.8440  -0.4940   -2.69%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                    │
│  2.2520   1.7870  -0.4650  -20.65%   736  coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html                                       │
│ 44.3520  43.9050  -0.4470   -1.01%   827  coq-vst/veric/binop_lemmas4.v.html                                                           │
│  1.0380   0.6100  -0.4280  -41.23%   813  coq-stdlib/MSets/MSetRBT.v.html                                                              │
│  8.7240   8.3170  -0.4070   -4.67%    34  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v.html      │
│  2.0950   1.6920  -0.4030  -19.24%    42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                     │
│  6.5870   6.1990  -0.3880   -5.89%    10  coq-rewriter/src/Rewriter/Rewriter/Examples.v.html                                           │
│ 19.4790  19.0990  -0.3800   -1.95%  2736  coq-metacoq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                         │
│  0.6770   0.2990  -0.3780  -55.83%   870  coq-stdlib/MSets/MSetRBT.v.html                                                              │
│  8.7410   8.3950  -0.3460   -3.96%    27  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.v.html                │
│ 15.2780  14.9350  -0.3430   -2.25%   613  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlattenExpr.v.html      │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

ppedrot

Fine as a hotfix.

ppedrot · 2024-02-19T14:16:40Z

@coqbot merge now

… and nf_evar in abstract"

Morally we consider them part of the body univs. This makes it so we don't need to disregard keep_body_ucst_separate when there are side effects. Fix coq#18636 (alternative to coq#18640, but this probably isn't as good a candidate for backporting)

Revert "Stop doing early universe minimization and nf_evar in abstract"

1fc0553

This reverts commit fea5fcc.

SkySkimmer added kind: fix This fixes a bug or incorrect documentation. part: universes The universe system. request: full CI Use this label when you want your next push to trigger a full CI. labels Feb 8, 2024

SkySkimmer added this to the 8.19.1 milestone Feb 8, 2024

SkySkimmer requested a review from a team as a code owner February 8, 2024 12:37

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

SkySkimmer mentioned this pull request Feb 8, 2024

Spurious universe inconsistencies in Coq 8.19 with abstracted proofs. #18636

Closed

SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Feb 8, 2024

SkySkimmer force-pushed the fix-double-abstract branch from 3b76e88 to a657220 Compare February 8, 2024 14:24

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

SkySkimmer mentioned this pull request Feb 8, 2024

close_proof: merge side effects univs when not keep_body_ucst_separate #18642

Merged

SkySkimmer force-pushed the fix-double-abstract branch from a657220 to 14685d5 Compare February 9, 2024 11:40

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

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

ppedrot self-assigned this Feb 19, 2024

ppedrot approved these changes Feb 19, 2024

View reviewed changes

coqbot-app bot merged commit c3c67fa into coq:master Feb 19, 2024
6 checks passed

coqbot-app bot added this to Request 8.19.1 inclusion in Coq 8.19 Feb 19, 2024

SkySkimmer deleted the fix-double-abstract branch February 19, 2024 15:03

SkySkimmer added a commit to SkySkimmer/coq that referenced this pull request Feb 19, 2024

Backport PR coq#18640: Revert "Stop doing early universe minimization…

d46b347

… and nf_evar in abstract"

coqbot-app bot moved this from Request 8.19.1 inclusion to Shipped in 8.19.1 in Coq 8.19 Feb 19, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Revert "Stop doing early universe minimization and nf_evar in abstract" #18640

Revert "Stop doing early universe minimization and nf_evar in abstract" #18640

SkySkimmer commented Feb 8, 2024

silene commented Feb 8, 2024

ppedrot commented Feb 8, 2024

SkySkimmer commented Feb 9, 2024

coqbot-app bot commented Feb 9, 2024

ppedrot left a comment

ppedrot commented Feb 19, 2024

Revert "Stop doing early universe minimization and nf_evar in abstract" #18640

Revert "Stop doing early universe minimization and nf_evar in abstract" #18640

Conversation

SkySkimmer commented Feb 8, 2024

silene commented Feb 8, 2024

ppedrot commented Feb 8, 2024

SkySkimmer commented Feb 9, 2024

coqbot-app bot commented Feb 9, 2024

ppedrot left a comment

Choose a reason for hiding this comment

ppedrot commented Feb 19, 2024