Remove the tag branch information from case_info. #18996
Merged
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
ppedrot
added
kind: cleanup
coqbot-app
bot
removed
the
request: full CI
|
Just in case this has a beneficial effect on performance / memory usage, let's @coqbot bench |
|
🏁 Bench results: INFO: failed to install coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed) 🐢 Top 25 slow downs┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 260.9510 267.2530 6.3020 2.42% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 181.2400 183.2030 1.9630 1.08% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 9.2000 10.6230 1.4230 15.47% 192 coq-vst/veric/binop_lemmas5.v.html │ │ 94.4340 95.8060 1.3720 1.45% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 47.2400 48.5500 1.3100 2.77% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 94.3800 95.6730 1.2930 1.37% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 62.2010 63.4480 1.2470 2.00% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 47.8350 48.6550 0.8200 1.71% 558 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 19.8460 20.6610 0.8150 4.11% 819 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 45.9450 46.7450 0.8000 1.74% 110 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 44.2960 45.0540 0.7580 1.71% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 132.4590 133.1690 0.7100 0.54% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 45.8700 46.5520 0.6820 1.49% 110 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 62.5250 63.1390 0.6140 0.98% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 3.3340 3.8650 0.5310 15.93% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 14.8090 15.2890 0.4800 3.24% 490 coq-unimath/UniMath/HomologicalAlgebra/KA.v.html │ │ 39.4600 39.8610 0.4010 1.02% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 22.7040 23.0980 0.3940 1.74% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 27.7540 28.1310 0.3770 1.36% 1933 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v.html │ │ 101.3000 101.6580 0.3580 0.35% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 20.8070 21.1340 0.3270 1.57% 213 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 1.5030 1.8290 0.3260 21.69% 557 coq-vst/veric/expr_lemmas3.v.html │ │ 2.8300 3.1520 0.3220 11.38% 487 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 21.4020 21.7050 0.3030 1.42% 40 coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html │ │ 4.5560 4.8500 0.2940 6.45% 5 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 258.1690 255.3520 -2.8170 -1.09% 1629 coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html │ │ 219.5540 217.1000 -2.4540 -1.12% 103 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 19.7510 18.3840 -1.3670 -6.92% 820 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 33.9250 33.1330 -0.7920 -2.33% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 155.7060 154.9810 -0.7250 -0.47% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 41.9780 41.5660 -0.4120 -0.98% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 12.6460 12.2880 -0.3580 -2.83% 409 coq-category-theory/Theory/Metacategory/ArrowsOnly.v.html │ │ 7.9790 7.6370 -0.3420 -4.29% 881 coq-vst/veric/binop_lemmas4.v.html │ │ 1.0950 0.7960 -0.2990 -27.31% 467 coq-stdlib/Numbers/DecimalFacts.v.html │ │ 0.8500 0.5740 -0.2760 -32.47% 170 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 27.5510 27.3040 -0.2470 -0.90% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 0.5390 0.2950 -0.2440 -45.27% 1364 coq-stdlib/FSets/FMapAVL.v.html │ │ 9.9050 9.6640 -0.2410 -2.43% 820 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 10.0060 9.7680 -0.2380 -2.38% 418 coq-category-theory/Theory/Metacategory/ArrowsOnly.v.html │ │ 16.0830 15.8500 -0.2330 -1.45% 828 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 73.0380 72.8070 -0.2310 -0.32% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ │ 50.6380 50.4220 -0.2160 -0.43% 50 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 0.2100 0.0000 -0.2100 -100.00% 241 coq-metacoq-erasure/erasure/theories/ErasureProperties.v.html │ │ 0.2070 0.0010 -0.2060 -99.52% 189 coq-metacoq-pcuic/pcuic/theories/PCUICPrincipality.v.html │ │ 37.1410 36.9390 -0.2020 -0.54% 548 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 5.7210 5.5220 -0.1990 -3.48% 19 coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html │ │ 34.1540 33.9580 -0.1960 -0.57% 839 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 26.2080 26.0210 -0.1870 -0.71% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 0.5030 0.3210 -0.1820 -36.18% 163 coq-stdlib/Numbers/HexadecimalPos.v.html │ │ 96.1350 95.9630 -0.1720 -0.18% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
ppedrot
added a commit
to ppedrot/paramcoq
that referenced
this pull request
May 3, 2024
ppedrot
added a commit
to ppedrot/coq-elpi
that referenced
this pull request
May 3, 2024
ppedrot
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
|
🔴 CI failures at commit 049b0e0 without any failure in the test-suite ✔️ Corresponding jobs for the base commit d9c5107 succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
ppedrot
added a commit
to ppedrot/coq-elpi
that referenced
this pull request
May 4, 2024
ppedrot
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
requested changes
May 7, 2024
| { ind_tags : bool list; (** tell whether letin or lambda in the arity of the inductive type *) | ||
| cstr_tags : bool list array; (** tell whether letin or lambda in the signature of each constructor *) | ||
| style : case_style } | ||
| { style : case_style } |
There was a problem hiding this comment.
Is it useful to keep this record? ie do we expect to add some fields to it someday?
There was a problem hiding this comment.
It doesn't cost much if we want to add other flags. I'd rather keep it.
This cache was only used in detyping, but even there most of the time it was dead code. Since all actual uses are already assuming that the inductive type exists in the environement, we simply fetch this data from there.
ppedrot
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
|
@SkySkimmer fixed |
SkySkimmer
approved these changes
May 7, 2024
|
@coqbot merge now |
|
@SkySkimmer: Please take care of the following overlays:
|
SkySkimmer
added a commit
to LPCIC/coq-elpi
that referenced
this pull request
May 13, 2024
Adapt w.r.t. coq/coq#18996.
SkySkimmer
added a commit
to coq-community/paramcoq
that referenced
this pull request
May 13, 2024
Adapt w.r.t. coq/coq#18996.
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.
This cache was only used in detyping, but even there most of the time it was dead code. Since all actual uses are already assuming that the inductive type exists in the environment, we simply fetch this data from there.
Overlays: