Experiment: do not retain hyp types of defined evars#21884
Draft
SkySkimmer wants to merge 2 commits intorocq-prover:masterfrom
Draft
Experiment: do not retain hyp types of defined evars#21884SkySkimmer wants to merge 2 commits intorocq-prover:masterfrom
SkySkimmer wants to merge 2 commits intorocq-prover:masterfrom
Conversation
In the test suite this breaks rewrite rules (probably need to use and older evar map or something?), "dependent evars line", and "Show Goal at" (PG prooftree). Also various debug printers are less informative because it's now impossible to get a correct env to print the evar body in.
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
Contributor
Author
|
@coqbot bench |
Member
|
Indeed, now I remember that the PG infrastructure was incompatible with this change. (I've been advocating for a nuclear anihilation of this broken feature for ages though.) |
Contributor
|
🏁 Bench results: INFO: failed to install rocq-mathcomp-boot (dependency rocq-elpi failed) 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 23.9 27.6 3.6690 15.35% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 43.4 45.7 2.3583 5.43% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 93.3 94.6 1.2902 1.38% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 18.6 19.8 1.2543 6.76% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 93.3 94.5 1.2178 1.31% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 236 237 1.1887 0.50% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 54.4 55.5 1.1123 2.04% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 119 120 0.9660 0.81% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 34.832 35.791 0.9590 2.75% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 59.5 60.5 0.9316 1.56% 659 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 0.729 1.64 0.9093 124.76% 213 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 83.6 84.5 0.8695 1.04% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 64.9 65.8 0.8667 1.34% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 3.18 4.01 0.8230 25.84% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification300.v.html │ │ 2.93 3.71 0.7895 26.99% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification290.v.html │ │ 2.69 3.42 0.7367 27.43% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification280.v.html │ │ 133 134 0.7352 0.55% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 25.5 26.2 0.6960 2.73% 788 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 2.48 3.17 0.6853 27.61% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification270.v.html │ │ 22.9 23.6 0.6284 2.74% 776 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 2.28 2.86 0.5879 25.84% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification260.v.html │ │ 46.2 46.8 0.5623 1.22% 115 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 27.2 27.8 0.5309 1.95% 794 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 21.9 22.4 0.5172 2.36% 520 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 2.08 2.59 0.5033 24.15% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification250.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 68.6 66.6 -2.0190 -2.94% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 42.5 41.5 -1.0844 -2.55% 244 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 94.2 93.1 -1.0235 -1.09% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 59.9 59.0 -0.9268 -1.55% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 6.49 5.59 -0.8970 -13.83% 530 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 44.8 44.0 -0.8294 -1.85% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 40.5 39.7 -0.8183 -2.02% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 37.2 36.4 -0.7295 -1.96% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 1.31 0.734 -0.5775 -44.03% 816 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 49.9 49.3 -0.5739 -1.15% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 25.1 24.6 -0.5347 -2.13% 550 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 31.9 31.4 -0.4938 -1.55% 255 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord.v.html │ │ 25.0 24.5 -0.4679 -1.87% 550 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 201 200 -0.4460 -0.22% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 43.0 42.6 -0.4243 -0.99% 221 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 7.66 7.27 -0.3923 -5.12% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 35.7 35.4 -0.3832 -1.07% 195 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 34.447 34.079 -0.3680 -1.07% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 26.6 26.2 -0.3562 -1.34% 62 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/TestAsm.v.html │ │ 36.9 36.6 -0.3331 -0.90% 222 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 4.18 3.85 -0.3310 -7.92% 492 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.589 0.268 -0.3211 -54.53% 14 rocq-stdlib/theories/ZArith/auxiliary.v.html │ │ 21.5 21.2 -0.2891 -1.35% 338 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 35.589 35.305 -0.2840 -0.80% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 1.36 1.10 -0.2640 -19.42% 36 coq-engine-bench-lite/coq/PerformanceDemos/rewrite_strat_under_binders.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
coqbot-app
bot
added
the
needs: full CI
Contributor
Author
|
@coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install rocq-mathcomp-boot (dependency rocq-elpi failed) 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 93.1 94.6 1.5218 1.63% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 93.3 94.7 1.4061 1.51% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 3.20 4.06 0.8639 27.00% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification300.v.html │ │ 119 120 0.8390 0.71% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 2.97 3.76 0.7934 26.72% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification290.v.html │ │ 2.71 3.40 0.6953 25.67% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification280.v.html │ │ 24.4 25.0 0.6369 2.61% 345 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 2.50 3.12 0.6217 24.85% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification270.v.html │ │ 11.4 12.0 0.6210 5.43% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 2.26 2.86 0.5996 26.50% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification260.v.html │ │ 2.10 2.63 0.5251 24.98% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification250.v.html │ │ 0.331 0.812 0.4803 144.95% 596 rocq-stdlib/theories/Strings/Byte.v.html │ │ 83.6 84.1 0.4769 0.57% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 1.92 2.38 0.4655 24.25% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification240.v.html │ │ 46.2 46.7 0.4406 0.95% 115 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 30.2 30.6 0.3977 1.32% 305 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 1.78 2.14 0.3598 20.22% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification230.v.html │ │ 1.59 1.94 0.3464 21.80% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification220.v.html │ │ 23.7 24.0 0.3353 1.41% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 0.996 1.33 0.3329 33.41% 572 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 3.78 4.10 0.3192 8.43% 492 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 1.41 1.73 0.3187 22.54% 2 coq-performance-tests-lite/src/typeclass_reification/typeclass_reification210.v.html │ │ 0.228 0.528 0.2994 131.21% 18 rocq-stdlib/theories/micromega/VarMap.v.html │ │ 5.91 6.20 0.2911 4.92% 798 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 0.164 0.454 0.2906 177.56% 592 rocq-stdlib/theories/MSets/MSetAVL.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 24.0 21.3 -2.7216 -11.32% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 64.4 62.5 -1.8975 -2.94% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 44.5 42.8 -1.7552 -3.94% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 68.9 67.4 -1.5110 -2.19% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 40.7 39.5 -1.1854 -2.91% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 45.3 44.2 -1.0718 -2.37% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 50.0 49.0 -1.0222 -2.04% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 203 202 -0.9144 -0.45% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 6.46 5.58 -0.8804 -13.62% 530 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 3.69 2.89 -0.8022 -21.72% 552 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 32.8 32.0 -0.7963 -2.43% 121 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 34.696 33.904 -0.7920 -2.28% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 31.5 30.7 -0.7905 -2.51% 166 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 25.2 24.4 -0.7670 -3.04% 550 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 42.3 41.5 -0.7613 -1.80% 244 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 31.5 30.8 -0.7401 -2.35% 180 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.6 30.9 -0.7345 -2.32% 139 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.4 30.7 -0.7054 -2.25% 198 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 25.1 24.4 -0.7044 -2.80% 550 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 44.8 44.1 -0.6755 -1.51% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 27.8 27.1 -0.6656 -2.40% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 35.655 35.06 -0.5950 -1.67% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 45.0 44.4 -0.5865 -1.30% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 31.6 31.1 -0.5785 -1.83% 157 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.6 31.1 -0.5519 -1.74% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
In the test suite this breaks rewrite rules (probably need to use and
older evar map or something?), "dependent evars line", and "Show Goal at"
(PG prooftree).
Also various debug printers are less informative because it's now
impossible to get a correct env to print the evar body in.