-
Notifications
You must be signed in to change notification settings - Fork 632
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.
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
Remove useless typechecking of future goals in refine #19030
Open
SkySkimmer
wants to merge
1
commit into
coq:master
Choose a base branch
from
SkySkimmer:refine-check-future
base: master
Could not load branches
Branch not found: {{ refName }}
Could not load tags
Nothing to show
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Conversation
This file contains 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
I can't see a reason to have it.
SkySkimmer
added
the
request: full CI
Use this label when you want your next push to trigger a full CI.
label
May 15, 2024
coqbot-app
bot
removed
the
request: full CI
Use this label when you want your next push to trigger a full CI.
label
May 15, 2024
@coqbot bench |
Some of the tactics send potentially ill-typed evars. It should be indeed the responsibility of the tactic itself to check that it doesn't generate crap, but 1. this is putting the burden on the caller and 2. maybe there are also user-facing calls to refine that mess with typing invariants. The latter should definitely be wrapped in a sanitizer somehow. |
🏁 Bench results:
🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 3.9050 4.9690 1.0640 27.25% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 10.9520 11.7590 0.8070 7.37% 2103 coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html │ │ 2.6530 3.3320 0.6790 25.59% 34 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 1.6310 2.1990 0.5680 34.83% 196 coq-stdlib/setoid_ring/Ncring_tac.v.html │ │ 44.2400 44.7430 0.5030 1.14% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 2.4640 2.9030 0.4390 17.82% 1001 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 27.4760 27.8590 0.3830 1.39% 147 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 29.3000 29.6220 0.3220 1.10% 12 coq-fourcolor/theories/job001to106.v.html │ │ 28.5220 28.8320 0.3100 1.09% 12 coq-fourcolor/theories/job323to383.v.html │ │ 24.1020 24.4110 0.3090 1.28% 12 coq-fourcolor/theories/job503to506.v.html │ │ 10.1850 10.4920 0.3070 3.01% 496 coq-rewriter/src/Rewriter/Rewriter/Wf.v.html │ │ 17.1400 17.4460 0.3060 1.79% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 29.2980 29.5910 0.2930 1.00% 12 coq-fourcolor/theories/job165to189.v.html │ │ 7.0890 7.3810 0.2920 4.12% 2089 coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html │ │ 37.7920 38.0810 0.2890 0.76% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html │ │ 24.4920 24.7800 0.2880 1.18% 12 coq-fourcolor/theories/job291to294.v.html │ │ 29.2280 29.5120 0.2840 0.97% 144 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 20.9160 21.1930 0.2770 1.32% 213 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 6.6750 6.9470 0.2720 4.07% 1075 coq-rewriter/src/Rewriter/Language/Inversion.v.html │ │ 1.6460 1.9180 0.2720 16.52% 165 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 0.5520 0.8200 0.2680 48.55% 816 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.5520 0.8070 0.2550 46.20% 422 coq-stdlib/MSets/MSetList.v.html │ │ 20.4300 20.6830 0.2530 1.24% 2736 coq-metacoq-safechecker/safechecker/theories/PCUICTypeChecker.v.html │ │ 39.7710 40.0240 0.2530 0.64% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 0.6320 0.8840 0.2520 39.87% 736 coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 259.4420 255.3860 -4.0560 -1.56% 1629 coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html │ │ 220.8970 217.8840 -3.0130 -1.36% 103 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 64.8390 62.3840 -2.4550 -3.79% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 64.6730 62.7400 -1.9330 -2.99% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 49.6360 47.9160 -1.7200 -3.47% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 96.1020 94.9250 -1.1770 -1.22% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 83.8810 82.8220 -1.0590 -1.26% 365 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 69.6670 68.6750 -0.9920 -1.42% 368 coq-mathcomp-odd-order/theories/PFsection4.v.html │ │ 96.0570 95.0700 -0.9870 -1.03% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 154.9220 154.0180 -0.9040 -0.58% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 102.1480 101.2510 -0.8970 -0.88% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 49.0280 48.1950 -0.8330 -1.70% 558 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 6.0570 5.3020 -0.7550 -12.46% 823 coq-metacoq-erasure/erasure/theories/ErasureFunction.v.html │ │ 20.5540 19.9970 -0.5570 -2.71% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 8.1020 7.6030 -0.4990 -6.16% 881 coq-vst/veric/binop_lemmas4.v.html │ │ 13.9520 13.5090 -0.4430 -3.18% 850 coq-unimath/UniMath/CategoryTheory/Profunctors/Transformation.v.html │ │ 20.6240 20.1890 -0.4350 -2.11% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 3.6330 3.2120 -0.4210 -11.59% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 36.8700 36.4790 -0.3910 -1.06% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 1.3400 0.9800 -0.3600 -26.87% 854 coq-stdlib/FSets/FMapAVL.v.html │ │ 82.2940 81.9420 -0.3520 -0.43% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 4.1430 3.7930 -0.3500 -8.45% 275 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 27.5140 27.1720 -0.3420 -1.24% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 23.5820 23.2610 -0.3210 -1.36% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 24.4920 24.1770 -0.3150 -1.29% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
I can't see a reason to have it.