Keep qvar in template poly entry and declarations #20178
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
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
added
the
needs: overlay
SkySkimmer
added a commit
to SkySkimmer/coq-elpi
that referenced
this pull request
Feb 3, 2025
SkySkimmer
added a commit
to SkySkimmer/Coq-Equations
that referenced
this pull request
Feb 3, 2025
SkySkimmer
added
the
request: full CI
SkySkimmer
force-pushed
the
template-entry-qvar
branch
from
af0eb5c to
af46f43
Compare
coqbot-app
bot
removed
the
request: full CI
|
IDK how to fix paramcoq, I guess it needs something like is done in checkinductive but this code is meant to go away once declarations also have qvars for template poly so I don't want to write it again. |
SkySkimmer
added
the
request: full CI
SkySkimmer
changed the title
SkySkimmer
force-pushed
the
template-entry-qvar
branch
from
af46f43 to
8eab675
Compare
coqbot-app
bot
removed
the
request: full CI
|
@coqbot bench |
|
nonsense bench, cf following comments 🏁 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 │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 41.4360 49.7370 8.3010 20.03% 834 coq-vst/veric/binop_lemmas4.v.html │ │ 6.4060 11.6240 5.2180 81.45% 1188 coq-verdi-raft/theories/RaftProofs/LogMatchingProof.v.html │ │ 30.8580 35.8280 4.9700 16.11% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 5.7100 10.1490 4.4390 77.74% 2883 coq-vst/veric/semax_call.v.html │ │ 5.5670 9.9980 4.4310 79.59% 2434 coq-vst/veric/semax_call.v.html │ │ 7.1310 11.3970 4.2660 59.82% 1387 coq-vst/floyd/data_at_lemmas.v.html │ │ 6.2550 9.8950 3.6400 58.19% 192 coq-vst/veric/binop_lemmas5.v.html │ │ 2.8320 5.9140 3.0820 108.83% 167 coq-vst/veric/binop_lemmas6.v.html │ │ 3.7660 6.2480 2.4820 65.91% 477 coq-vst/veric/expr_lemmas3.v.html │ │ 0.7410 2.9640 2.2230 300.00% 174 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 5.5420 7.3970 1.8550 33.47% 888 coq-vst/veric/binop_lemmas4.v.html │ │ 0.9190 2.6660 1.7470 190.10% 458 coq-verdi-raft/theories/RaftProofs/LogMatchingProof.v.html │ │ 11.1170 12.8060 1.6890 15.19% 126 coq-vst/veric/binop_lemmas6.v.html │ │ 0.5640 2.2310 1.6670 295.57% 143 coq-verdi-raft/theories/RaftProofs/CroniesCorrectProof.v.html │ │ 0.6430 2.1710 1.5280 237.64% 208 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 90.3630 91.6920 1.3290 1.47% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 90.3370 91.6580 1.3210 1.46% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 0.4990 1.7780 1.2790 256.31% 657 coq-verdi-raft/theories/Raft/RefinementSpecLemmas.v.html │ │ 2.1820 3.1380 0.9560 43.81% 1496 coq-vst/floyd/SeparationLogicAsLogic.v.html │ │ 3.5310 4.4240 0.8930 25.29% 154 coq-vst/veric/binop_lemmas5.v.html │ │ 0.3400 1.1670 0.8270 243.24% 172 coq-verdi-raft/theories/RaftProofs/CroniesCorrectProof.v.html │ │ 3.6780 4.4880 0.8100 22.02% 166 coq-verdi-raft/theories/RaftProofs/LeaderSublogProof.v.html │ │ 1.2560 2.0290 0.7730 61.54% 553 coq-vst/veric/binop_lemmas3.v.html │ │ 2.8810 3.6300 0.7490 26.00% 431 coq-vst/veric/binop_lemmas3.v.html │ │ 0.6950 1.4380 0.7430 106.91% 278 coq-vst/floyd/field_at_wand.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 11.3100 0.0760 -11.2340 -99.33% 410 coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html │ │ 33.3060 31.6230 -1.6830 -5.05% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 18.6650 17.0530 -1.6120 -8.64% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 34.3270 32.7350 -1.5920 -4.64% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 15.3290 13.7870 -1.5420 -10.06% 1208 coq-vst/floyd/Component.v.html │ │ 15.3050 13.7970 -1.5080 -9.85% 1222 coq-vst/floyd/Component.v.html │ │ 15.2200 13.7960 -1.4240 -9.36% 1505 coq-vst/floyd/VSU.v.html │ │ 2.9440 2.0340 -0.9100 -30.91% 179 coq-vst/veric/Clight_mapsto_memory_block.v.html │ │ 2.9420 2.0400 -0.9020 -30.66% 142 coq-vst/veric/Clight_mapsto_memory_block.v.html │ │ 7.6780 6.8820 -0.7960 -10.37% 1508 coq-vst/floyd/Component.v.html │ │ 7.6280 6.9490 -0.6790 -8.90% 782 coq-vst/floyd/Component.v.html │ │ 7.9560 7.2790 -0.6770 -8.51% 755 coq-vst/floyd/Component.v.html │ │ 7.5910 6.9380 -0.6530 -8.60% 1221 coq-vst/floyd/Component.v.html │ │ 7.5800 6.9470 -0.6330 -8.35% 1205 coq-vst/floyd/Component.v.html │ │ 7.5350 6.9170 -0.6180 -8.20% 1503 coq-vst/floyd/VSU.v.html │ │ 7.4900 6.9460 -0.5440 -7.26% 1207 coq-vst/floyd/Component.v.html │ │ 7.4910 6.9520 -0.5390 -7.20% 1220 coq-vst/floyd/Component.v.html │ │ 10.7200 10.1820 -0.5380 -5.02% 985 coq-vst/floyd/closed_lemmas.v.html │ │ 4.4020 4.0190 -0.3830 -8.70% 278 coq-vst/veric/SeparationLogicSoundness.v.html │ │ 7.5380 7.1910 -0.3470 -4.60% 1501 coq-vst/floyd/VSU.v.html │ │ 7.5080 7.1730 -0.3350 -4.46% 1505 coq-vst/floyd/Component.v.html │ │ 3.2440 3.0400 -0.2040 -6.29% 32 coq-performance-tests-lite/src/n_polymorphic_universes.v.html │ │ 8.0610 7.8840 -0.1770 -2.20% 34 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.v.html │ │ 4.3500 4.1800 -0.1700 -3.91% 32 coq-engine-bench-lite/coq/PerformanceDemos/do_n_binder.v.html │ │ 0.5200 0.3570 -0.1630 -31.35% 126 coq-vst/atomics/verif_lock.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
coqbot-app
bot
added
the
needs: full CI
|
@coqbot bench |
|
IDK what exactly the bench was doing but it seems to have gotten confused over the temporary deletion of coq-bignums.dev and installed some random versions. then equations moves coq back to .dev, but fails so it only happens in NEW and we're from then on running NEW in NEW but 8.16 or something in OLD |
|
🏁 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 │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 63.3360 65.6380 2.3020 3.63% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 63.8790 65.1070 1.2280 1.92% 609 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 30.9110 31.4810 0.5700 1.84% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 26.0650 26.5890 0.5240 2.01% 375 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 6.2180 6.7370 0.5190 8.35% 192 coq-vst/veric/binop_lemmas5.v.html │ │ 36.9060 37.3900 0.4840 1.31% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 78.2140 78.6980 0.4840 0.62% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 26.1250 26.5910 0.4660 1.78% 374 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 15.6120 16.0770 0.4650 2.98% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 91.2680 91.7110 0.4430 0.49% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 47.7610 48.1990 0.4380 0.92% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 1.7980 2.2290 0.4310 23.97% 635 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 35.2920 35.6660 0.3740 1.06% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 36.9100 37.2390 0.3290 0.89% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 9.6770 9.9620 0.2850 2.95% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 117.8650 118.1450 0.2800 0.24% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 26.7330 27.0070 0.2740 1.02% 147 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 11.3520 11.6050 0.2530 2.23% 410 coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html │ │ 2.3900 2.6250 0.2350 9.83% 679 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 17.2970 17.5170 0.2200 1.27% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 6.2050 6.4190 0.2140 3.45% 840 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html │ │ 9.8790 10.0920 0.2130 2.16% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 1.5680 1.7780 0.2100 13.39% 1125 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/PERSubobjectClassifier.v.html │ │ 0.0010 0.2050 0.2040 20400.00% 517 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v.html │ │ 46.0940 46.2960 0.2020 0.44% 110 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 175.2700 171.7350 -3.5350 -2.02% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ │ 202.1010 199.2950 -2.8060 -1.39% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 7.1000 5.6400 -1.4600 -20.56% 196 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 4.9830 3.8820 -1.1010 -22.10% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 4.0110 3.1170 -0.8940 -22.29% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 17.5620 16.8170 -0.7450 -4.24% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 34.9800 34.4420 -0.5380 -1.54% 120 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 7.5960 7.0840 -0.5120 -6.74% 681 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 3.2620 2.8230 -0.4390 -13.46% 34 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 4.2870 3.9020 -0.3850 -8.98% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 18.9130 18.5300 -0.3830 -2.03% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 38.4650 38.1140 -0.3510 -0.91% 224 coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │ │ 21.9800 21.6400 -0.3400 -1.55% 49 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 38.8920 38.5550 -0.3370 -0.87% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 16.7660 16.4300 -0.3360 -2.00% 81 coq-fiat-crypto-with-bedrock/rupicola/src/Rupicola/Examples/Utf8/Utf8.v.html │ │ 11.7230 11.3950 -0.3280 -2.80% 857 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/PERSubobjectClassifier.v.html │ │ 46.1750 45.8550 -0.3200 -0.69% 110 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 13.0710 12.7570 -0.3140 -2.40% 388 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 13.1430 12.8540 -0.2890 -2.20% 324 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html │ │ 19.0760 18.8280 -0.2480 -1.30% 708 coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html │ │ 3.5530 3.3190 -0.2340 -6.59% 32 coq-performance-tests-lite/src/n_polymorphic_universes.v.html │ │ 8.2260 8.0010 -0.2250 -2.74% 746 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/PERSubobjectClassifier.v.html │ │ 33.4530 33.2300 -0.2230 -0.67% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 25.0830 24.8610 -0.2220 -0.89% 345 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 20.6110 20.3950 -0.2160 -1.05% 297 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Universal.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
This slightly changes behaviour for inductives which don't really need
template, eg `Inductive foo (A:Type@{i}) : Type@{i} := .` is now not
pseudo sort poly because the parameter and conclusion qualities end up
unrelated, so the conclusion quality has no binders and must be
collapsed to Type.
There is currently no way to explicitly specify it, as
`Inductive foo@{q|i|} ...` won't work because the named `q` can't be
made above prop (and we need it above prop for evar normalization to
substitute it away in relevances).
template_sort and mind_sort are the same thing, and the remaining template info is in mind_template. NB: "template_level is inferred by indtypes, so functor application can produce a smaller one" in checkInductive is outdated since 9bba040 (8.17)
SkySkimmer
added a commit
to SkySkimmer/coq-lsp
that referenced
this pull request
Feb 5, 2025
SkySkimmer
added a commit
to SkySkimmer/metacoq
that referenced
this pull request
Feb 5, 2025
… not quality set)
SkySkimmer
added a commit
to SkySkimmer/paramcoq
that referenced
this pull request
Feb 5, 2025
SkySkimmer
added
kind: redesign
SkySkimmer
force-pushed
the
template-entry-qvar
branch
from
447a845 to
776ea8a
Compare
coqbot-app
bot
removed
request: full CI
|
Running a small bench just to test rocq-prover/opam#3332 |
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 1.0490 1.1030 0.0540 5.15% 204 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 0.0010 0.0540 0.0530 5300.00% 1421 rocq-stdlib/theories/Reals/Ratan.v.html │ │ 0.0010 0.0530 0.0520 5200.00% 424 rocq-stdlib/theories/Reals/Ratan.v.html │ │ 0.0000 0.0500 0.0500 inf% 624 rocq-stdlib/theories/FSets/FMapFullAVL.v.html │ │ 0.0000 0.0490 0.0490 inf% 1005 rocq-stdlib/theories/Reals/RiemannInt_SF.v.html │ │ 0.0030 0.0520 0.0490 1633.33% 700 rocq-stdlib/theories/Reals/Rtrigo1.v.html │ │ 0.0000 0.0480 0.0480 inf% 1677 rocq-stdlib/theories/Reals/Ranalysis1.v.html │ │ 0.0390 0.0850 0.0460 117.95% 524 rocq-stdlib/theories/Strings/PString.v.html │ │ 0.0020 0.0480 0.0460 2300.00% 162 rocq-stdlib/theories/Numbers/HexadecimalR.v.html │ │ 0.0000 0.0460 0.0460 inf% 575 rocq-stdlib/theories/Reals/Ranalysis5.v.html │ │ 0.0000 0.0460 0.0460 inf% 524 rocq-stdlib/theories/Reals/Rfunctions.v.html │ │ 0.0160 0.0610 0.0450 281.25% 308 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.0020 0.0460 0.0440 2200.00% 636 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyAbs.v.html │ │ 0.0220 0.0650 0.0430 195.45% 1190 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.0000 0.0430 0.0430 inf% 470 rocq-stdlib/theories/btauto/Algebra.v.html │ │ 0.0010 0.0430 0.0420 4200.00% 1165 rocq-stdlib/theories/micromega/ZMicromega.v.html │ │ 0.0010 0.0410 0.0400 4000.00% 347 rocq-stdlib/theories/Strings/PString.v.html │ │ 0.0000 0.0400 0.0400 inf% 730 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.0000 0.0400 0.0400 inf% 419 rocq-stdlib/theories/Reals/Abstract/ConstructiveSum.v.html │ │ 0.0320 0.0710 0.0390 121.87% 688 rocq-stdlib/theories/FSets/FSetPositive.v.html │ │ 0.0000 0.0380 0.0380 inf% 643 rocq-stdlib/theories/setoid_ring/InitialRing.v.html │ │ 0.0000 0.0380 0.0380 inf% 789 rocq-stdlib/theories/ZArith/Zdiv.v.html │ │ 0.0020 0.0390 0.0370 1850.00% 1474 rocq-stdlib/theories/QArith/QArith_base.v.html │ │ 0.0000 0.0370 0.0370 inf% 93 rocq-stdlib/theories/Reals/Zfloor.v.html │ │ 0.0000 0.0370 0.0370 inf% 126 rocq-stdlib/theories/Reals/Rbasic_fun.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.0560 0.0020 -0.0540 -96.43% 1420 rocq-stdlib/theories/Reals/Ratan.v.html │ │ 0.0530 0.0000 -0.0530 -100.00% 423 rocq-stdlib/theories/Reals/Ratan.v.html │ │ 0.0550 0.0030 -0.0520 -94.55% 623 rocq-stdlib/theories/FSets/FMapFullAVL.v.html │ │ 0.0520 0.0010 -0.0510 -98.08% 694 rocq-stdlib/theories/Reals/Rtrigo1.v.html │ │ 0.0520 0.0010 -0.0510 -98.08% 996 rocq-stdlib/theories/Reals/RiemannInt_SF.v.html │ │ 0.0530 0.0030 -0.0500 -94.34% 163 rocq-stdlib/theories/Numbers/HexadecimalR.v.html │ │ 0.0480 0.0000 -0.0480 -100.00% 523 rocq-stdlib/theories/Reals/Rfunctions.v.html │ │ 0.0480 0.0000 -0.0480 -100.00% 574 rocq-stdlib/theories/Reals/Ranalysis5.v.html │ │ 0.0480 0.0010 -0.0470 -97.92% 635 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyAbs.v.html │ │ 0.0530 0.0060 -0.0470 -88.68% 522 rocq-stdlib/theories/Strings/PString.v.html │ │ 0.0760 0.0290 -0.0470 -61.84% 1187 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.0470 0.0010 -0.0460 -97.87% 307 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 0.0450 0.0000 -0.0450 -100.00% 1353 rocq-stdlib/theories/micromega/ZMicromega.v.html │ │ 0.0510 0.0070 -0.0440 -86.27% 960 rocq-stdlib/theories/MSets/MSetGenTree.v.html │ │ 0.0450 0.0010 -0.0440 -97.78% 469 rocq-stdlib/theories/btauto/Algebra.v.html │ │ 0.0430 0.0000 -0.0430 -100.00% 187 rocq-stdlib/theories/FSets/FSetProperties.v.html │ │ 0.0420 0.0000 -0.0420 -100.00% 413 rocq-stdlib/theories/Reals/Abstract/ConstructiveSum.v.html │ │ 0.0420 0.0000 -0.0420 -100.00% 741 rocq-stdlib/theories/FSets/FSetPositive.v.html │ │ 0.1100 0.0680 -0.0420 -38.18% 233 rocq-stdlib/theories/Reals/Abstract/ConstructiveLimits.v.html │ │ 0.0450 0.0030 -0.0420 -93.33% 346 rocq-stdlib/theories/Strings/PString.v.html │ │ 0.1270 0.0860 -0.0410 -32.28% 731 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.0400 0.0000 -0.0400 -100.00% 613 rocq-stdlib/theories/MSets/MSetGenTree.v.html │ │ 0.0400 0.0000 -0.0400 -100.00% 1473 rocq-stdlib/theories/QArith/QArith_base.v.html │ │ 0.1440 0.1040 -0.0400 -27.78% 444 rocq-stdlib/theories/Reals/Abstract/ConstructiveLimits.v.html │ │ 0.0390 0.0000 -0.0390 -100.00% 788 rocq-stdlib/theories/ZArith/Zdiv.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
SkySkimmer
added a commit
to SkySkimmer/metacoq
that referenced
this pull request
Feb 5, 2025
… not quality set)
SkySkimmer
added a commit
to SkySkimmer/metacoq
that referenced
this pull request
Feb 5, 2025
|
The paramcoq overlay was much more feasible now that both entries and declarations have qvars |
|
What about the VST slowdown in a previous bench? |
|
The first bench in this PR is just garbage, opam got confused and installed 8.16 or something |
|
@coqbot merge now |
|
@ppedrot: Please take care of the following overlays:
|
ppedrot
added a commit
to mattam82/Coq-Equations
that referenced
this pull request
Feb 6, 2025
Adapt to rocq-prover/rocq#20178 (map_univs_opt_subst takes relevance normalizer)
ppedrot
added a commit
to LPCIC/coq-elpi
that referenced
this pull request
Feb 6, 2025
Adapt to rocq-prover/rocq#20178 (cominductive API change)
ppedrot
added a commit
to ejgallego/coq-lsp
that referenced
this pull request
Feb 6, 2025
Adapt to rocq-prover/rocq#20178 (inductive_arity doesn't exist)
ppedrot
added a commit
to MetaRocq/metarocq
that referenced
this pull request
Feb 6, 2025
Adapt to rocq-prover/rocq#20178 (UContext.to_context returns qvar set not quality set)
ppedrot
added a commit
to rocq-community/paramcoq
that referenced
this pull request
Feb 6, 2025
Adapt to rocq-prover/rocq#20178 (kernel template data has qvars)
SkySkimmer
added a commit
to SkySkimmer/rocq
that referenced
this pull request
Feb 18, 2025
This should prevent silent downgrades like we had in rocq-prover#20178 (comment)
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 slightly changes behaviour for inductives which don't really need
template, eg
Inductive foo (A:Type@{i}) : Type@{i} := .is now notpseudo sort poly because the parameter and conclusion qualities end up
unrelated, so the conclusion quality has no binders and must be
collapsed to Type.
There is currently no way to explicitly specify it, as
Inductive foo@{q|i|} ...won't work because the namedqcan't bemade above prop (and we need it above prop for evar normalization to
substitute it away in relevances).
Overlays: