Remove the name field from projections.#22114
Open
ppedrot wants to merge 3 commits into
Open
Conversation
ppedrot
added
the
request: full CI
coqbot-app
Bot
removed
the
request: full CI
SkySkimmer
reviewed
Jun 10, 2026
SkySkimmer
previously requested changes
Jun 10, 2026
SkySkimmer
reviewed
Jun 10, 2026
| val get_projections : env -> inductive -> (Names.Projection.Repr.t * Sorts.relevance) array option | ||
|
|
||
| val projection_repr_label : env -> Projection.Repr.t -> Id.t | ||
| val projection_repr_constant : env -> Projection.Repr.t -> Constant.t |
Contributor
There was a problem hiding this comment.
do we want to move this to higher layers at some point?
we have a table in the other direction in structures.ml but it seems these new functions are used in engine which is below structures.ml
Member
Author
There was a problem hiding this comment.
I would agree, but I would still like to proceed incrementally. There are indeed several places where we depend on the projection names in the lower parts of the upper layers, which is bad (notably name generation, which required me to pass an additional environment in some places). Fixing this properly will require a behaviour change, so better left for a later time.
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
rm-projection-name
branch
from
280e555 to
b538f29
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
I fixed the detyper to be more lenient with incomplete environments, this is enough to make your precise problem with the debugger disappear. |
Contributor
|
@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 │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 1.35 2.45 1.0934 80.75% 574 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 23.9 24.9 1.0546 4.42% 782 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 42.0 43.1 1.0296 2.45% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 26.6 27.6 1.0234 3.85% 794 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 44.1 45.1 0.9824 2.23% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 28.9 29.7 0.8442 2.92% 145 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 44.1 45.0 0.8371 1.90% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 27.1 27.9 0.8126 2.99% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html │ │ 26.7 27.5 0.7858 2.94% 34 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 12.7 13.5 0.7762 6.12% 1628 coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html │ │ 28.8 29.5 0.7304 2.54% 31 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 30.4 31.1 0.6508 2.14% 198 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.6 32.2 0.6254 1.98% 121 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 16.7 17.3 0.6240 3.73% 762 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 22.4 23.0 0.6056 2.70% 776 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 200 200 0.6007 0.30% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 30.6 31.2 0.5979 1.95% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 88.9 89.5 0.5833 0.66% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 30.7 31.2 0.5604 1.83% 214 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 30.5 31.0 0.5140 1.69% 139 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 30.5 31.0 0.4592 1.51% 166 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 33.3 33.7 0.4458 1.34% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 89.0 89.4 0.4079 0.46% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 30.7 31.1 0.3909 1.27% 180 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 30.6 31.0 0.3908 1.28% 157 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 108 105 -2.1224 -1.97% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 238 236 -1.5951 -0.67% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 16.7 15.4 -1.3194 -7.91% 833 coq-unimath/UniMath/CategoryTheory/ComprehensionCats/CwfFromCompCatWithUniv.v.html │ │ 11.7 10.6 -1.0419 -8.94% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 134 133 -0.8919 -0.66% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 43.0 42.2 -0.8447 -1.96% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 3.28 2.45 -0.8285 -25.23% 34 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 55.9 55.1 -0.7863 -1.41% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 3.74 2.98 -0.7645 -20.43% 130 coq-category-theory/Functor/Strong/Product.v.html │ │ 4.15 3.45 -0.6997 -16.85% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 0.879 0.209 -0.6701 -76.23% 374 rocq-stdlib/theories/Sorting/SetoidList.v.html │ │ 3.90 3.28 -0.6161 -15.81% 492 rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 19.2 18.6 -0.5949 -3.10% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 38.8 38.2 -0.5613 -1.45% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 1.01 0.451 -0.5588 -55.34% 2109 rocq-stdlib/theories/FSets/FMapFacts.v.html │ │ 18.8 18.2 -0.5481 -2.92% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 2.12 1.58 -0.5338 -25.23% 42 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 2.90 2.38 -0.5277 -18.17% 597 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/SetGroupoidComprehension.v.html │ │ 42.5 42.1 -0.4637 -1.09% 50 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 4.15 3.71 -0.4444 -10.70% 196 rocq-stdlib/theories/ZArith/ZModOffset.v.html │ │ 24.6 24.1 -0.4296 -1.75% 345 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 80.6 80.2 -0.4158 -0.52% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 4.22 3.85 -0.3743 -8.87% 199 coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html │ │ 18.6 18.2 -0.3484 -1.88% 670 coq-performance-tests-lite/src/Nia.v.html │ │ 35.5 35.2 -0.3412 -0.96% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
rm-projection-name
branch
from
b538f29 to
6a5bb9a
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
Let's have a bench with the overlays: @coqbot bench |
ppedrot
added a commit
to ppedrot/coq-elpi
that referenced
this pull request
Jun 11, 2026
yannl35133
reviewed
Jun 11, 2026
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 200 203 3.6221 1.82% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 24.5 27.9 3.3951 13.85% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 88.3 90.4 2.0794 2.35% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 88.5 90.2 1.7619 1.99% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 30.6 31.5 0.9645 3.16% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 33.2 34.0 0.8137 2.45% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 12.7 13.5 0.7844 6.17% 1628 coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html │ │ 30.5 31.3 0.7646 2.50% 157 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 30.4 31.1 0.7628 2.51% 214 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 15.378 16.132 0.7540 4.90% 1209 coq-vst/floyd/Component.v.html │ │ 31.7 32.4 0.7494 2.37% 121 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 44.2 45.0 0.7272 1.64% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 83.4 84.0 0.5823 0.70% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 30.7 31.3 0.5724 1.86% 180 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 28.4 28.9 0.5664 2.00% 305 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 30.6 31.2 0.5494 1.79% 166 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 15.425 15.961 0.5360 3.47% 1223 coq-vst/floyd/Component.v.html │ │ 44.6 45.1 0.5157 1.16% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 50.6 51.1 0.5109 1.01% 567 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 30.5 31.0 0.5034 1.65% 139 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 25.3 25.8 0.4833 1.91% 788 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 30.4 30.9 0.4727 1.55% 198 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 12.4 12.8 0.4280 3.46% 930 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 26.6 27.0 0.4201 1.58% 794 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 34.081 34.494 0.4130 1.21% 97 coq-vst/veric/binop_lemmas5.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 108 106 -1.5758 -1.46% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 11.8 10.5 -1.2610 -10.70% 194 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 43.0 41.8 -1.1668 -2.71% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 16.6 15.4 -1.1172 -6.75% 833 coq-unimath/UniMath/CategoryTheory/ComprehensionCats/CwfFromCompCatWithUniv.v.html │ │ 56.0 55.1 -0.8651 -1.55% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 4.04 3.18 -0.8639 -21.37% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 3.79 2.95 -0.8372 -22.10% 130 coq-category-theory/Functor/Strong/Product.v.html │ │ 39.1 38.3 -0.7982 -2.04% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 80.7 80.1 -0.5988 -0.74% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 48.8 48.2 -0.5651 -1.16% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 42.2 41.6 -0.5406 -1.28% 235 coq-category-theory/Construction/DecoratedCospan/Category.v.html │ │ 2.10 1.57 -0.5281 -25.13% 42 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 39.6 39.1 -0.4993 -1.26% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 237 236 -0.4835 -0.20% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 2.84 2.38 -0.4586 -16.13% 597 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/SetGroupoidComprehension.v.html │ │ 4.27 3.82 -0.4503 -10.56% 199 coq-fiat-crypto-with-bedrock/src/Fancy/Montgomery256.v.html │ │ 0.406 0.000109 -0.4058 -99.97% 227 coq-mathcomp-analysis/theories/trigo.v.html │ │ 62.9 62.5 -0.4054 -0.64% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 22.0 21.6 -0.3812 -1.73% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 5.10 4.73 -0.3760 -7.37% 19 coq-fiat-crypto-with-bedrock/src/Language/IdentifiersBasicGENERATED.v.html │ │ 13.7 13.4 -0.3647 -2.66% 216 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 2.04 1.68 -0.3606 -17.70% 447 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html │ │ 54.6 54.2 -0.3554 -0.65% 296 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 0.357 0.00181 -0.3547 -99.49% 509 coq-mathcomp-analysis/theories/sequences.v.html │ │ 0.609 0.256 -0.3528 -57.96% 11 rocq-stdlib/theories/omega/PreOmega.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
ppedrot
added
the
request: full CI
ppedrot
force-pushed
the
rm-projection-name
branch
from
6a5bb9a to
8b0c11b
Compare
coqbot-app
Bot
removed
the
request: full CI
SkySkimmer
approved these changes
Jun 12, 2026
yannl35133
reviewed
Jun 12, 2026
SkySkimmer
requested changes
Jun 12, 2026
ppedrot
added
the
request: full CI
One now needs an environment to access this data. We are still a long way from removing the compatibility constants but at least it is not in the kernel data structure anymore.
ppedrot
force-pushed
the
rm-projection-name
branch
from
8b0c11b to
20e3b31
Compare
coqbot-app
Bot
removed
the
request: full CI
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
3 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.
One now needs an environment to access this data. We are still a long way from removing the compatibility constants but at least it is not in the kernel data structure anymore.
Overlays: