Skip to content

Be stricter about substitution of evar instances. #16488

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
Merged
merged 2 commits into from
Sep 16, 2022
Merged

Be stricter about substitution of evar instances. #16488

merged 2 commits into from
Sep 16, 2022

Conversation

ppedrot
Copy link
Member

@ppedrot ppedrot commented Sep 14, 2022 •
edited
Loading

Forecasting the change of representation of evar instances, we now assume we cannot access the default parts of the instance without access to an evarmap. This means that all functions from the kernel now raise an anomaly when trying to mess with potential Var nodes of evar instances, and that their counterpart in the upper layer now take an additional evarmap argument.

Overlays:

@ppedrot ppedrot added needs: overlay This is breaking external developments we track in CI. kind: internal API, ML documentation... labels Sep 14, 2022
@ppedrot ppedrot added this to the 8.17+rc1 milestone Sep 14, 2022
@ppedrot ppedrot requested review from a team as code owners September 14, 2022 10:13
ppedrot added a commit to ppedrot/rewriter that referenced this pull request Sep 14, 2022
@ppedrot
Adapt w.r.t. rocq-prover/rocq#16488.
273efff
ppedrot added a commit to ppedrot/Coq-Equations that referenced this pull request Sep 14, 2022
@ppedrot
Adapt w.r.t. rocq-prover/rocq#16488.
8ab5d39
ppedrot added a commit to ppedrot/Coq-Equations that referenced this pull request Sep 14, 2022
@ppedrot
Adapt w.r.t. rocq-prover/rocq#16488.
6690aff
ppedrot added a commit to ppedrot/unicoq that referenced this pull request Sep 14, 2022
@ppedrot
Adapt w.r.t. rocq-prover/rocq#16488.
b0dcee8
ppedrot added a commit to ppedrot/Mtac2 that referenced this pull request Sep 14, 2022
@ppedrot
Adapt w.r.t. rocq-prover/rocq#16488.
db0dcc9
ppedrot added a commit to ppedrot/Coq-Equations that referenced this pull request Sep 14, 2022
@ppedrot
Adapt w.r.t. rocq-prover/rocq#16488.
743b9dd
ppedrot added a commit to ppedrot/relation-algebra that referenced this pull request Sep 14, 2022
@ppedrot
Adapt w.r.t. rocq-prover/rocq#16488.
db7ecfe
ppedrot added a commit to ppedrot/relation-algebra that referenced this pull request Sep 14, 2022
@ppedrot
Adapt w.r.t. rocq-prover/rocq#16488.
1baefde
@ppedrot ppedrot removed the needs: overlay This is breaking external developments we track in CI. label Sep 14, 2022
@ppedrot
Be stricter about substitution of evar instances.
482316c 
Forecasting the change of representation of evar instances, we now assume
we cannot access the default parts of the instance without access to an
evarmap. This means that all functions from the kernel now raise an anomaly
when trying to mess with potential Var nodes of evar instances, and that their
counterpart in the upper layer now take an additional evarmap argument.
@ppedrot
Adding overlays.
0406438
@ppedrot ppedrot force-pushed the stricter-evar-access branch from 689c074 to 0406438 Compare September 14, 2022 17:06
@SkySkimmer
Copy link
Contributor

Should we bench?

@SkySkimmer SkySkimmer removed request for a team September 15, 2022 14:29
@SkySkimmer SkySkimmer requested review from a team and removed request for a team September 15, 2022 14:29
@Alizter
Copy link
Contributor

Alizter commented Sep 15, 2022

@coqbot bench

@ppedrot
Copy link
Member Author

ppedrot commented Sep 15, 2022

This is just adding dead code, I don't see how the bench could observe anything.

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 16, 2022

🏁 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-geocoq │  712.28   714.90  -0.37 │  3246754201034   3257071399505  -0.32 │  5306606924535   5313825820946  -0.14 │ 1107128  1105044    0.19 │   0    0    nan │
│                coq-unimath │ 5604.14  5623.32  -0.34 │ 25621146052982  25705966847547  -0.33 │ 50471051016835  50459497013942   0.02 │ 4745804  4748020   -0.05 │   0    0    nan │
│                 coq-stdlib │  414.03   415.17  -0.27 │  1781346782038   1784443700716  -0.17 │  1539348659931   1538799197500   0.04 │  704708   704584    0.02 │   0    0    nan │
│               coq-bedrock2 │  391.16   391.93  -0.20 │  1786701648690   1788976754276  -0.13 │  3453746046692   3453862610837  -0.00 │ 1910136  1910128    0.00 │   0    0    nan │
│                 coq-flocq3 │   75.71    75.68   0.04 │   343306717418    343247557859   0.02 │   469568015826    469219186328   0.07 │ 1012920  1008844    0.40 │   0    0    nan │
│                   coq-corn │  807.45   807.11   0.04 │  3675549785530   3673385100515   0.06 │  5841240656451   5840244851592   0.02 │  862548   862476    0.01 │   0    0    nan │
│               coq-coqprime │   43.87    43.78   0.21 │   198985211979    198303061799   0.34 │   304369817749    304718426646  -0.11 │  768216   768208    0.00 │   0    0    nan │
│              coq-fourcolor │ 1475.45  1472.41   0.21 │  6732812228812   6715049292051   0.26 │ 12226855705541  12226547243296   0.00 │  740716   739064    0.22 │   0    0    nan │
│                coq-coqutil │   35.89    35.81   0.22 │   161798180843    161570027803   0.14 │   236601997870    236415571855   0.08 │  601132   601020    0.02 │   0    0    nan │
│              coq-perennial │ 4977.01  4964.15   0.26 │ 22693866753279  22633932773114   0.26 │ 37397218799914  37390737724323   0.02 │ 2706932  2696468    0.39 │   0    0    nan │
│     coq-mathcomp-character │   68.97    68.75   0.32 │   314913751730    314025297687   0.28 │   479204899054    478918520219   0.06 │  742368   746000   -0.49 │   0    0    nan │
│         coq-mathcomp-field │   94.95    94.63   0.34 │   434358930731    432310116484   0.47 │   715692253014    715498819714   0.03 │  651616   647140    0.69 │   0    0    nan │
│      coq-engine-bench-lite │  160.13   159.56   0.36 │   689657941784    685665569488   0.58 │  1299303820053   1299637558377  -0.03 │  981476   982152   -0.07 │   0    0    nan │
│      coq-mathcomp-solvable │   82.78    82.44   0.41 │   377837800173    375651462181   0.58 │   582503134971    582229280910   0.05 │  667116   664944    0.33 │   0    0    nan │
│                   coq-hott │  162.70   161.98   0.44 │   736954311860    734040380111   0.40 │  1176177027709   1175723068828   0.04 │  579552   579500    0.01 │   0    0    nan │
│                   coq-core │  111.18   110.68   0.45 │   465907735803    465663477190   0.05 │   484175936293    483876117378   0.06 │  288096   287676    0.15 │   0    0    nan │
│           coq-fiat-parsers │  339.33   337.70   0.48 │  1525926840756   1516959609488   0.59 │  2561001587506   2560162258248   0.03 │ 3541992  3541452    0.02 │   0    0    nan │
│          coq-iris-examples │  487.87   485.09   0.57 │  2216314679267   2202881246266   0.61 │  3375434157810   3375219328343   0.01 │ 1233984  1236212   -0.18 │   0    0    nan │
│             coq-verdi-raft │  585.22   581.86   0.58 │  2671838799115   2655270800214   0.62 │  4223155965308   4222828295369   0.01 │ 1235204  1235552   -0.03 │   0    0    nan │
│     coq-mathcomp-odd-order │  472.03   468.23   0.81 │  2159990783912   2141856432336   0.85 │  3746703757402   3745881468070   0.02 │  960232   960888   -0.07 │   0    0    nan │
│               coq-compcert │  296.26   293.87   0.81 │  1344240346826   1331824068144   0.93 │  2057178589879   2056053554392   0.05 │ 1127128  1128124   -0.09 │   0    0    nan │
│                  coq-verdi │   47.89    47.46   0.91 │   217144372994    215193045779   0.91 │   332913740732    333077860978  -0.05 │  790860   789736    0.14 │   0    0    nan │
│       coq-mathcomp-algebra │   62.62    62.05   0.92 │   285544447568    282941724661   0.92 │   396231830694    396050412052   0.05 │  572120   571036    0.19 │   0    0    nan │
│      coq-mathcomp-fingroup │   22.82    22.61   0.93 │   104045325368    103001390375   1.01 │   152928426388    152846246337   0.05 │  495208   495068    0.03 │   0    0    nan │
│                  coq-color │  227.61   225.47   0.95 │  1028022308944   1018369449668   0.95 │  1495700580197   1495139755579   0.04 │ 1184340  1184588   -0.02 │   0    0    nan │
│           coq-math-classes │   96.96    95.99   1.01 │   440322459115    435413015424   1.13 │   643944428661    643701765159   0.04 │  512864   516304   -0.67 │   0    0    nan │
│              coq-fiat-core │   57.67    57.08   1.03 │   249321240536    246067105611   1.32 │   361412013279    361203498708   0.06 │  486208   485964    0.05 │   0    0    nan │
│             coq-coquelicot │   36.40    35.99   1.14 │   163163962207    161161429858   1.24 │   224291277330    223845956529   0.20 │  752816   756296   -0.46 │   0    0    nan │
│                coq-bignums │   28.47    28.04   1.53 │   129255217162    127668248549   1.24 │   184357999231    184331671201   0.01 │  475792   477804   -0.42 │   0    0    nan │
│ coq-performance-tests-lite │  770.36   758.66   1.54 │  3496037693288   3441955637834   1.57 │  6260217362540   6251618445416   0.14 │ 2155300  2430860  -11.34 │   0    0    nan │
│     coq-mathcomp-ssreflect │   26.68    26.27   1.56 │   121845888645    119341492312   2.10 │   157587348476    157455161387   0.08 │  564824   563604    0.22 │   0    0    nan │
└────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┴─────────────────┘
🐢 Top 25 slow downs 
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                             │
│   OLD       NEW      DIFF   %DIFF    Ln                     FILE                                                                            │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 112.4850  119.7870  7.3020   6.49%  1104  coq-unimath/UniMath/Bicategories/PseudoFunctors/Preservation/BiadjunctionPreserveInserters.v.html │
│ 127.3130  129.9850  2.6720   2.10%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│ 127.6550  130.0210  2.3660   1.85%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                   │
│  33.0940   33.7900  0.6960   2.10%    10  coq-fourcolor/theories/job001to106.v.html                                                         │
│  28.0800   28.7590  0.6790   2.42%  1157  coq-unimath/UniMath/Bicategories/DisplayedBicats/Cartesians.v.html                                │
│  14.1750   14.7490  0.5740   4.05%    29  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                         │
│   8.9750    9.4930  0.5180   5.77%  2163  coq-unimath/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory2.v.html          │
│  19.1480   19.6340  0.4860   2.54%    10  coq-fourcolor/theories/job623to633.v.html                                                         │
│   2.8280    3.2580  0.4300  15.21%   105  coq-perennial/src/program_proof/wal/circ_proof_crash.v.html                                       │
│  27.1220   27.5490  0.4270   1.57%    10  coq-fourcolor/theories/job299to302.v.html                                                         │
│  55.2140   55.5800  0.3660   0.66%   857  coq-unimath/UniMath/Bicategories/DisplayedBicats/Examples/DisplayedInserter.v.html                │
│  27.4170   27.7700  0.3530   1.29%    10  coq-fourcolor/theories/job535to541.v.html                                                         │
│  23.0410   23.3920  0.3510   1.52%    10  coq-fourcolor/theories/job511to516.v.html                                                         │
│  26.4780   26.7980  0.3200   1.21%    10  coq-fourcolor/theories/job503to506.v.html                                                         │
│  25.6820   25.9910  0.3090   1.20%    10  coq-fourcolor/theories/job554to562.v.html                                                         │
│  25.5160   25.8220  0.3060   1.20%   310  coq-unimath/UniMath/Bicategories/PseudoFunctors/Preservation/BiadjunctionPreserveProducts.v.html  │
│  31.1450   31.4480  0.3030   0.97%    10  coq-fourcolor/theories/job107to164.v.html                                                         │
│  24.1070   24.4050  0.2980   1.24%    10  coq-fourcolor/theories/job303to306.v.html                                                         │
│  15.2230   15.5050  0.2820   1.85%   185  coq-perennial/src/goose_lang/interpreter/disk_interpreter.v.html                                  │
│   2.4430    2.7140  0.2710  11.09%  1820  coq-unimath/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory2.v.html          │
│   9.6690    9.9340  0.2650   2.74%  1631  coq-unimath/UniMath/Bicategories/DisplayedBicats/Cartesians.v.html                                │
│  21.2020   21.4660  0.2640   1.25%    10  coq-fourcolor/theories/job507to510.v.html                                                         │
│  23.3720   23.6290  0.2570   1.10%    10  coq-fourcolor/theories/job542to545.v.html                                                         │
│   5.4250    5.6680  0.2430   4.48%  1424  coq-unimath/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory2.v.html          │
│  28.7430   28.9810  0.2380   0.83%    10  coq-fourcolor/theories/job531to534.v.html                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
🐇 Top 25 speed ups 
┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                │
│                                                                                                                                                │
│   OLD       NEW      DIFF     %DIFF    Ln                     FILE                                                                             │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 153.9250  152.2470  -1.6780   -1.09%  1188  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                      │
│ 242.0140  240.3510  -1.6630   -0.69%   938  coq-unimath/UniMath/Bicategories/Monads/Examples/Composition.v.html                                │
│   1.4290    0.0160  -1.4130  -98.88%  1223  coq-unimath/UniMath/Bicategories/PseudoFunctors/Preservation/BiadjunctionPreserveInserters.v.html  │
│  30.2840   28.9490  -1.3350   -4.41%  1375  coq-fourcolor/theories/cfmap.v.html                                                                │
│  35.9680   35.1830  -0.7850   -2.18%   445  coq-unimath/UniMath/SyntheticHomotopyTheory/Circle2.v.html                                         │
│  18.3120   17.5380  -0.7740   -4.23%   580  coq-unimath/UniMath/Bicategories/PseudoFunctors/Preservation/BiadjunctionPreserveCoproducts.v.html │
│  56.0400   55.2990  -0.7410   -1.32%   820  coq-unimath/UniMath/SubstitutionSystems/LiftingInitial.v.html                                      │
│ 130.7630  130.0320  -0.7310   -0.56%   706  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                        │
│  27.7350   27.0250  -0.7100   -2.56%   371  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                      │
│  24.1150   23.4610  -0.6540   -2.71%  2290  coq-perennial/src/goose_lang/logical_reln_fund.v.html                                              │
│  46.9300   46.3090  -0.6210   -1.32%   464  coq-unimath/UniMath/Bicategories/PseudoFunctors/Examples/CompositionPseudoFunctor.v.html           │
│  27.7220   27.2170  -0.5050   -1.82%    10  coq-fourcolor/theories/job618to622.v.html                                                          │
│  38.1420   37.7190  -0.4230   -1.11%   633  coq-unimath/UniMath/SubstitutionSystems/Signatures.v.html                                          │
│  27.9680   27.5490  -0.4190   -1.50%    10  coq-fourcolor/theories/job499to502.v.html                                                          │
│  34.8260   34.4360  -0.3900   -1.12%   837  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                      │
│  33.2290   32.8460  -0.3830   -1.15%   747  coq-unimath/UniMath/SubstitutionSystems/ActionBasedStrengthOnHomsInBicat.v.html                    │
│   7.0880    6.7460  -0.3420   -4.83%  1740  coq-unimath/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory2.v.html           │
│  26.3360   26.0000  -0.3360   -1.28%   446  coq-unimath/UniMath/SubstitutionSystems/SubstitutionSystems.v.html                                 │
│   7.4460    7.1120  -0.3340   -4.49%  1167  coq-unimath/UniMath/Bicategories/DisplayedBicats/FiberBicategory/FiberBicategory2.v.html           │
│  26.7520   26.4210  -0.3310   -1.24%  1650  coq-geocoq/Tarski_dev/Ch16_coordinates_with_functions.v.html                                       │
│  27.5770   27.2470  -0.3300   -1.20%  1640  coq-geocoq/Tarski_dev/Ch16_coordinates_with_functions.v.html                                       │
│  26.1190   25.8120  -0.3070   -1.18%    10  coq-fourcolor/theories/job295to298.v.html                                                          │
│  50.0140   49.7110  -0.3030   -0.61%   587  coq-unimath/UniMath/SubstitutionSystems/SignatureExamples.v.html                                   │
│   5.5670    5.2740  -0.2930   -5.26%  1373  coq-unimath/UniMath/Bicategories/Limits/PullbackFunctions.v.html                                   │
│  22.5910   22.3100  -0.2810   -1.24%  2250  coq-unimath/UniMath/Bicategories/MonoidalCategories/ActionBasedStrongFunctorsMonoidal.v.html       │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

@SkySkimmer SkySkimmer self-assigned this Sep 16, 2022
@SkySkimmer
Copy link
Contributor

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 352685c into rocq-prover:master Sep 16, 2022
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Sep 16, 2022

@SkySkimmer: Please take care of the following overlays:

  • 16488-ppedrot-stricter-evar-access.sh

@ppedrot ppedrot deleted the stricter-evar-access branch September 16, 2022 08:06
ppedrot added a commit to mattam82/Coq-Equations that referenced this pull request Sep 16, 2022
@ppedrot
Merge pull request #511 from ppedrot/stricter-evar-access
718435b 
Adapt w.r.t. rocq-prover/rocq#16488.
bors bot added a commit to Mtac2/Mtac2 that referenced this pull request Sep 16, 2022
@bors @ppedrot
Merge #367
287761a 
367: Adapt w.r.t. rocq-prover/rocq#16488. r=Janno a=ppedrot



Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
damien-pous pushed a commit to damien-pous/relation-algebra that referenced this pull request Sep 16, 2022
@ppedrot @damien-pous
Adapt w.r.t. rocq-prover/rocq#16488.
649a442
andres-erbsen added a commit to mit-plv/rewriter that referenced this pull request Sep 16, 2022
@andres-erbsen
Merge pull request #59 from ppedrot/stricter-evar-access
50d58c6 
Adapt w.r.t. rocq-prover/rocq#16488.
bors bot added a commit to Mtac2/Mtac2 that referenced this pull request Sep 16, 2022
@bors @ppedrot
Merge #367
429a867 
367: Adapt w.r.t. rocq-prover/rocq#16488. r=Janno a=ppedrot



Co-authored-by: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Janno added a commit to Mtac2/Mtac2 that referenced this pull request Sep 16, 2022
@Janno
Merge pull request #367 from ppedrot/stricter-evar-access
0749f51 
Adapt w.r.t. rocq-prover/rocq#16488.
beta-ziliani pushed a commit to unicoq/unicoq that referenced this pull request Sep 16, 2022
@ppedrot
Adapt w.r.t. rocq-prover/rocq#16488. (#73)
505ca77
JasonGross pushed a commit to JasonGross/rewriter that referenced this pull request Sep 26, 2022
@ppedrot @JasonGross
Adapt w.r.t. rocq-prover/rocq#16488.
a2e756d
JasonGross pushed a commit to JasonGross/rewriter that referenced this pull request Sep 26, 2022
@ppedrot @JasonGross
Adapt w.r.t. rocq-prover/rocq#16488.
365014c
JasonGross pushed a commit to JasonGross/rewriter that referenced this pull request Sep 27, 2022
@ppedrot @JasonGross
Adapt w.r.t. rocq-prover/rocq#16488.
0607def
@herbelin herbelin mentioned this pull request Oct 16, 2022
Merged
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: internal API, ML documentation...
Projects
None yet
Milestone
8.17+rc1
Development

Successfully merging this pull request may close these issues.
3 participants
@ppedrot @SkySkimmer @Alizter