Experiment: optimized representation for nat constants (a zarith Z.t values)#21729
Draft
SkySkimmer wants to merge 36 commits intorocq-prover:masterfrom
Draft
Experiment: optimized representation for nat constants (a zarith Z.t values)#21729SkySkimmer wants to merge 36 commits intorocq-prover:masterfrom
nat constants (a zarith Z.t values)#21729SkySkimmer wants to merge 36 commits intorocq-prover:masterfrom
Conversation
coqbot-app
bot
added
the
needs: full CI
Member
|
It's not because all your friends are jumping off a cliff that you should do it... |
SkySkimmer
force-pushed
the
bignat
branch
3 times, most recently
from
2cc50b3 to
a76d28b
Compare
the main motivation is actually to be able to compare between representations in constr_equal
Contributor
|
🏁 Bench results: INFO: failed to install rocq-bignums (dependency rocq-stdlib failed) 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.00824 0.0462 0.0380 460.97% 344 coq-hott/theories/Algebra/Rings/Localization.v.html │ │ 0.00436 0.0385 0.0341 782.10% 69 coq-hott/test/Algebra/Rings/Matrix.v.html │ │ 0.0245 0.0578 0.0333 135.94% 185 coq-hott/theories/Algebra/AbSES/Pullback.v.html │ │ 0.0114 0.0446 0.0332 290.45% 382 coq-hott/theories/Algebra/AbSES/Pullback.v.html │ │ 0.000116 0.0317 0.0316 27220.69% 1376 coq-hott/contrib/HoTTBookExercises.v.html │ │ 0.000642 0.0319 0.0312 4866.98% 418 coq-hott/theories/Algebra/AbGroups/TensorProduct.v.html │ │ 0.0319 0.0616 0.0297 92.99% 251 coq-hott/theories/Homotopy/HomotopyGroup.v.html │ │ 0.0567 0.0862 0.0295 52.08% 254 coq-hott/theories/Algebra/AbSES/PullbackFiberSequence.v.html │ │ 0.0841 0.112 0.0274 32.62% 208 coq-hott/theories/Algebra/ooGroup.v.html │ │ 0.0110 0.0375 0.0265 242.12% 240 coq-hott/theories/Algebra/Groups/GrpPullback.v.html │ │ 0.0260 0.0516 0.0256 98.56% 144 coq-hott/theories/Homotopy/HomotopyGroup.v.html │ │ 0.000266 0.0224 0.0221 8307.14% 771 coq-hott/theories/Algebra/Groups/Group.v.html │ │ 0.0361 0.0554 0.0194 53.74% 807 coq-hott/theories/Algebra/AbGroups/TensorProduct.v.html │ │ 0.00172 0.0199 0.0182 1054.91% 171 coq-hott/theories/Homotopy/Join/Core.v.html │ │ 0.0172 0.0353 0.0181 105.20% 85 coq-hott/theories/Homotopy/Bouquet.v.html │ │ 0.590 0.608 0.0180 3.06% 82 coq-hott/theories/Categories/Adjoint/Pointwise.v.html │ │ 0.0273 0.0437 0.0164 60.31% 547 coq-hott/theories/WildCat/HomologicalAlgebra.v.html │ │ 0.0151 0.0311 0.0160 105.64% 414 coq-hott/theories/Homotopy/Wedge.v.html │ │ 0.0823 0.0983 0.0160 19.49% 63 coq-hott/theories/Homotopy/PinSn.v.html │ │ 0.0124 0.0282 0.0158 127.24% 537 coq-hott/theories/Algebra/Rings/Ring.v.html │ │ 0.220 0.236 0.0156 7.08% 211 coq-hott/theories/Colimits/Colimit_Flattening.v.html │ │ 0.00935 0.0249 0.0156 166.83% 558 coq-hott/theories/WildCat/Products.v.html │ │ 0.0275 0.0426 0.0151 54.71% 345 coq-hott/theories/Algebra/Groups/QuotientGroup.v.html │ │ 0.000546 0.0150 0.0145 2656.23% 576 coq-hott/theories/Algebra/AbGroups/TensorProduct.v.html │ │ 0.595 0.609 0.0140 2.35% 34 coq-hott/theories/Homotopy/PinSn.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.553 0.351 -0.2020 -36.54% 296 coq-hott/theories/HIT/V.v.html │ │ 0.0423 0.00881 -0.0335 -79.17% 785 coq-hott/theories/Algebra/AbGroups/TensorProduct.v.html │ │ 0.0318 0.000076 -0.0317 -99.76% 1377 coq-hott/contrib/HoTTBookExercises.v.html │ │ 0.0311 0.000427 -0.0306 -98.63% 304 coq-hott/theories/Algebra/AbGroups/TensorProduct.v.html │ │ 0.0285 0.00108 -0.0274 -96.20% 224 coq-hott/theories/Spaces/Spheres.v.html │ │ 0.0511 0.0238 -0.0273 -53.41% 519 coq-hott/theories/WildCat/HomologicalAlgebra.v.html │ │ 0.0339 0.00711 -0.0268 -79.06% 421 coq-hott/theories/Algebra/Rings/Ring.v.html │ │ 0.0321 0.00705 -0.0250 -78.02% 297 coq-hott/theories/WildCat/HomologicalAlgebra.v.html │ │ 0.129 0.104 -0.0245 -19.04% 312 coq-hott/theories/Algebra/Groups/QuotientGroup.v.html │ │ 0.0495 0.0257 -0.0238 -48.05% 423 coq-hott/theories/Algebra/Rings/Localization.v.html │ │ 0.0883 0.0646 -0.0237 -26.84% 137 coq-hott/theories/Algebra/AbGroups/AbPushout.v.html │ │ 0.0693 0.0458 -0.0235 -33.91% 462 coq-hott/theories/Algebra/AbSES/Pullback.v.html │ │ 0.0243 0.00156 -0.0227 -93.55% 225 coq-hott/theories/Homotopy/Join/JoinAssoc.v.html │ │ 0.0272 0.00528 -0.0219 -80.57% 375 coq-hott/theories/Homotopy/Wedge.v.html │ │ 0.0294 0.00790 -0.0215 -73.09% 113 coq-hott/theories/WildCat/HomologicalAlgebra.v.html │ │ 0.0264 0.00528 -0.0212 -80.03% 545 coq-hott/theories/Algebra/Groups/Group.v.html │ │ 0.0249 0.00373 -0.0212 -85.03% 342 coq-hott/theories/Homotopy/Smash.v.html │ │ 0.0652 0.0446 -0.0206 -31.65% 89 coq-hott/test/Algebra/Rings/Matrix.v.html │ │ 0.0210 0.000450 -0.0205 -97.85% 292 coq-hott/contrib/HoTTBookExercises.v.html │ │ 0.0407 0.0203 -0.0204 -50.16% 233 coq-hott/theories/Algebra/AbSES/Pullback.v.html │ │ 0.0891 0.0697 -0.0194 -21.74% 361 coq-hott/theories/Homotopy/Join/JoinAssoc.v.html │ │ 0.0380 0.0209 -0.0171 -45.04% 310 coq-hott/theories/Homotopy/HomotopyGroup.v.html │ │ 0.0264 0.00977 -0.0167 -63.02% 161 coq-hott/theories/Spaces/Spheres.v.html │ │ 0.0751 0.0595 -0.0156 -20.81% 949 coq-hott/theories/WildCat/Products.v.html │ │ 0.0538 0.0390 -0.0148 -27.51% 149 coq-hott/theories/Homotopy/HomotopyGroup.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────┘ |
SkySkimmer
added a commit
to SkySkimmer/coq-elpi
that referenced
this pull request
Mar 10, 2026
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
request: full CI
Contributor
Author
|
@coqbot bench |
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
Contributor
|
🏁 Bench results: INFO: failed to install rocq-mathcomp-order (dependency rocq-mathcomp-boot failed) 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 26.0 26.7 0.7291 2.80% 374 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 26.0 26.7 0.7227 2.78% 375 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 12.4 12.9 0.4713 3.79% 930 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 1.08 1.48 0.4010 37.19% 572 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 7.27 7.60 0.3268 4.50% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 8.68 9.00 0.3218 3.71% 950 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 6.94 7.25 0.3126 4.51% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 8.38 8.70 0.3114 3.71% 648 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 0.0854 0.388 0.3025 354.46% 558 rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html │ │ 0.272 0.572 0.3008 110.80% 586 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.530 0.821 0.2904 54.78% 829 rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html │ │ 0.329 0.613 0.2844 86.50% 141 rocq-stdlib/theories/Strings/Ascii.v.html │ │ 7.26 7.53 0.2744 3.78% 663 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 0.0810 0.337 0.2564 316.43% 677 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.0442 0.297 0.2525 571.74% 549 rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html │ │ 0.255 0.499 0.2441 95.86% 719 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 48.9 49.1 0.2394 0.49% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 4.71 4.95 0.2373 5.04% 260 coq-unimath/UniMath/CategoryTheory/Monoidal/RezkCompletion/LiftedMonoidal.v.html │ │ 0.0472 0.272 0.2246 475.83% 536 rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html │ │ 6.65 6.87 0.2166 3.26% 831 coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html │ │ 0.361 0.573 0.2121 58.69% 637 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.265 0.476 0.2114 79.91% 707 rocq-stdlib/theories/MSets/MSetList.v.html │ │ 0.279 0.481 0.2016 72.19% 19 rocq-stdlib/theories/ZArith/Int.v.html │ │ 0.0846 0.285 0.2006 236.98% 20 rocq-stdlib/theories/Vectors/Bvector.v.html │ │ 16.7 16.9 0.1999 1.19% 905 coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 10.1 7.96 -2.1417 -21.19% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 9.94 7.82 -2.1174 -21.30% 325 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 1.35 0.0993 -1.2522 -92.65% 8 coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html │ │ 2.31 1.60 -0.7076 -30.67% 8 coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html │ │ 3.35 2.70 -0.6466 -19.32% 109 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 0.753 0.407 -0.3459 -45.96% 1604 rocq-stdlib/theories/micromega/Tauto.v.html │ │ 0.584 0.238 -0.3459 -59.21% 14 rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html │ │ 2.58 2.25 -0.3312 -12.81% 212 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 1.21 0.876 -0.3307 -27.42% 816 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 0.357 0.0450 -0.3116 -87.39% 6 coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html │ │ 0.859 0.549 -0.3103 -36.13% 206 rocq-stdlib/theories/setoid_ring/Ncring_tac.v.html │ │ 1.44 1.13 -0.3044 -21.15% 200 rocq-stdlib/theories/Numbers/HexadecimalNat.v.html │ │ 0.530 0.243 -0.2872 -54.17% 11 rocq-stdlib/theories/QArith/Qcanon.v.html │ │ 21.9 21.7 -0.2607 -1.19% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 0.484 0.228 -0.2564 -52.94% 283 rocq-stdlib/theories/Numbers/HexadecimalPos.v.html │ │ 0.615 0.371 -0.2446 -39.73% 596 rocq-stdlib/theories/Strings/Byte.v.html │ │ 18.6 18.4 -0.2341 -1.26% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 0.631 0.413 -0.2178 -34.51% 6 coq-engine-bench-lite/coq/PerformanceDemos/repeated_conj.v.html │ │ 0.347 0.135 -0.2120 -61.04% 141 rocq-stdlib/theories/Numbers/DecimalNat.v.html │ │ 0.866 0.667 -0.1987 -22.95% 41 rocq-stdlib/theories/ZArith/Zdiv_facts.v.html │ │ 0.392 0.194 -0.1985 -50.60% 170 coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html │ │ 0.660 0.462 -0.1982 -30.02% 83 rocq-stdlib/theories/Numbers/Cyclic/Int63/Sint63.v.html │ │ 0.574 0.378 -0.1955 -34.06% 1161 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.469 0.283 -0.1857 -39.61% 678 rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html │ │ 0.336 0.155 -0.1817 -54.01% 35 rocq-stdlib/theories/MSets/MSetRBT.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
Author
|
@coqbot ci minimize ci-mathcomp |
Contributor
|
I am now running minimization at commit a7c9de2 on requested target ci-mathcomp. I'll come back to you with the results once it's done. |
SkySkimmer
added
the
request: full CI
SkySkimmer
added a commit
to SkySkimmer/Coq-Equations
that referenced
this pull request
Mar 10, 2026
coqbot-app
bot
removed
the
request: full CI
Contributor
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/mathcomp/boot/ssrnat.v in 27m 31s (from ci-mathcomp) (full log on GitHub Actions - verbose log) We are collecting data on the user experience of the Coq Bug Minimizer. 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+duplicate-clear" "-w" "+non-primitive-record" "-w" "+undeclared-scope" "-w" "+deprecated-hint-without-locality" "-w" "+deprecated-hint-rewrite-without-locality" "-w" "-projection-no-head-constant" "-w" "-redundant-canonical-projection" "-w" "-notation-overridden" "-w" "-ambiguous-paths" "-w" "-elpi.add-const-for-axiom-or-sectionvar" "-w" "-mathcomp-subset-itv" "-w" "+level-tolerance" "-w" "-notation-for-abbreviation" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-coqlib" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq//" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/mathcomp" "mathcomp" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/HB" "HB" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/elpi" "elpi" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/elpi_elpi" "elpi_elpi" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq///user-contrib/elpi_examples" "elpi_examples" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/mathcomp" "-top" "mathcomp.boot.ssrnat") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 2161 lines to 47 lines, then from 61 lines to 1170 lines, then from 1177 lines to 75 lines, then from 89 lines to 147 lines, then from 154 lines to 80 lines *)
(* coqc version 9.3+alpha compiled with OCaml 4.14.2
coqtop version 9.3+alpha
Expected coqc runtime on this file: 0.308 sec
Expected coqc peak memory usage on this file: 407356.0 kb *)
Require Corelib.ssr.ssrbool.
Require mathcomp.boot.ssrfun.
Require HB.structures.
Export Corelib.ssr.ssrbool.
Module Export mathcomp.
Module Export boot.
Module Export ssrbool.
End ssrbool.
Module mathcomp_DOT_boot_DOT_eqtype_WRAPPED.
Module Export eqtype.
Import HB.structures.
Import mathcomp.boot.ssrfun.
Set Implicit Arguments.
Definition eq_axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).
HB.mixin Record hasDecEq T := { eq_op : rel T; eqP : eq_axiom eq_op }.
#[mathcomp(axiom="eq_axiom"), short(type="eqType")]
HB.structure Definition Equality := { T of hasDecEq T }.
Notation "x == y" := (eq_op x y) (no associativity) : bool_scope.
Module Type EqTypePredSig.
End EqTypePredSig.
Module MakeEqTypePred (eqmod : EqTypePredSig).
End MakeEqTypePred.
End eqtype.
End mathcomp_DOT_boot_DOT_eqtype_WRAPPED.
Include mathcomp_DOT_boot_DOT_eqtype_WRAPPED.eqtype.
Import HB.structures.
Import mathcomp.boot.ssreflect.
Import mathcomp.boot.ssrfun.
Import mathcomp.boot.ssrbool.
Notation succn := Datatypes.S.
Notation "n .+1" := (succn n) (left associativity, format "n .+1") : nat_scope.
Fixpoint eqn m n {struct m} :=
match m, n with
| 0, 0 => true
| m'.+1, n'.+1 => eqn m' n'
| _, _ => false
end.
Lemma eqnP : Equality.axiom eqn.
Admitted.
HB.instance Definition _ := hasDecEq.Build nat eqnP.
Definition addn := plus.
Lemma addn0 : right_id 0 addn.
Admitted.
Definition leq m n := m - n == 0.
Notation "m <= n" := (leq m n) : nat_scope.
Notation "m >= n" := (n <= m) (only parsing) : nat_scope.
Section ExMinn.
Variable P : pred nat.
Hypothesis exP : exists n, P n.
Inductive acc_nat i : Prop := AccNat0 of P i | AccNatS of acc_nat i.+1.
Lemma find_ex_minn : {m | P m & forall n, P n -> n >= m}.
Proof.
have: forall n, P n -> n >= 0 by [].
have: acc_nat 0.
case exP => n; rewrite -(addn0 n); elim: n 0 => [|n IHn] j; first by left.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 4.2MiB file on GitHub Actions Artifacts under
|
Contributor
I think this saying does not apply to performance cliffs.
I was expecting changes in |
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.
The current state has some random TODOs and term matching (notation printing, ltac matching) is probably janky but is enough to have a look.
Prelude
natdoes not use the optimization (so CI should say nothing interesting), see new test filebignatfor actual use of the optimization.The optimization is similar to what agda https://agda.readthedocs.io/en/latest/language/built-ins.html#natural-numbers and lean https://lean-lang.org/doc/reference/latest/Basic-Types/Natural-Numbers/ have: closed nat values ("nat constants") can be represented by
Nat of Z.t.The cbv machine has optimized implementations for
+/*on nat constants (the one for tail_mul is necessary to get large literals to work).The VM produces values using the optimized representation but has no special handling for operators.
cclosure/
lazy/cclosure-based conversion can handle inputs which contain the optimized representation but do not build larger values using it, ie1 + 1where1is optimized reduces toS 1(which converts correctly to2).TBH I'm not sure how to do otherwise in a lazy/call by name setting, if we see
1 + efor some arbitrary expressionewe should not reducee(at least in weak head mode).native_compute, cbn and reductionops do
failwith "TODO"on optimized constants.I think tacred treats optimized constants as opaque values but who knows what this code even is.