Stop inlining abstracted subproofs in tactics in terms.#21676
Draft
ppedrot wants to merge 1 commit intorocq-prover:masterfrom
Draft
Stop inlining abstracted subproofs in tactics in terms.#21676ppedrot wants to merge 1 commit intorocq-prover:masterfrom
ppedrot wants to merge 1 commit intorocq-prover:masterfrom
Conversation
Fixes rocq-prover#7905: abstract in tactics in terms should not inline.
ppedrot
added
kind: fix
coqbot-app
bot
removed
the
request: full CI
Contributor
|
@coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install coq-fiat-crypto-with-bedrock (dependency coq-rewriter failed) 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.297 0.927 0.6308 212.65% 153 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 7.74 8.25 0.5112 6.60% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 18.1 18.6 0.4927 2.72% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 0.00444 0.419 0.4149 9349.14% 72 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 1.51 1.93 0.4140 27.38% 368 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/LiftPoset.v.html │ │ 0.0273 0.438 0.4111 1506.06% 141 rocq-mathcomp-solvable/solvable/extraspecial.v.html │ │ 0.578 0.927 0.3484 60.24% 7 rocq-mathcomp-solvable/solvable/all_solvable.v.html │ │ 0.333 0.660 0.3268 98.16% 13 rocq-stdlib/theories/ZArith/Zmin.v.html │ │ 8.23 8.53 0.3027 3.68% 420 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ │ 9.39 9.69 0.2941 3.13% 434 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 30.0 30.3 0.2862 0.95% 12 coq-fourcolor/theories/proof/job001to106.v.html │ │ 0.344 0.608 0.2634 76.52% 15 rocq-stdlib/theories/micromega/ZifyInst.v.html │ │ 4.022 4.283 0.2610 6.49% 1387 coq-vst/floyd/data_at_lemmas.v.html │ │ 1.11 1.37 0.2590 23.30% 733 coq-category-theory/Construction/Comma/Adjunction.v.html │ │ 7.72 7.97 0.2524 3.27% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 0.569 0.813 0.2443 42.95% 170 rocq-stdlib/theories/Numbers/HexadecimalNat.v.html │ │ 10.0 10.3 0.2404 2.40% 279 coq-category-theory/Theory/Metacategory.v.html │ │ 0.170 0.404 0.2334 136.94% 697 rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html │ │ 0.161 0.390 0.2291 142.34% 14 rocq-stdlib/theories/Vectors/FinFun.v.html │ │ 0.328 0.553 0.2247 68.52% 1 rocq-stdlib/theories/ZArith/Zdivisibility.v.html │ │ 0.322 0.546 0.2240 69.64% 141 rocq-stdlib/theories/Numbers/DecimalNat.v.html │ │ 0.00460 0.226 0.2212 4807.28% 337 rocq-mathcomp-solvable/solvable/primitive_action.v.html │ │ 0.00276 0.223 0.2201 7978.80% 271 rocq-mathcomp-solvable/solvable/hall.v.html │ │ 0.0153 0.233 0.2180 1423.13% 90 rocq-mathcomp-solvable/solvable/primitive_action.v.html │ │ 0.00106 0.218 0.2170 20418.44% 76 rocq-mathcomp-solvable/solvable/hall.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 203 202 -1.2603 -0.62% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 4.58 3.91 -0.6663 -14.56% 196 rocq-stdlib/theories/ZArith/ZModOffset.v.html │ │ 1.65 0.993 -0.6545 -39.73% 572 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 67.3 66.8 -0.5232 -0.78% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 18.7 18.3 -0.4337 -2.31% 481 coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html │ │ 0.424 0.00329 -0.4207 -99.22% 75 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 0.449 0.0401 -0.4092 -91.08% 140 rocq-mathcomp-solvable/solvable/extraspecial.v.html │ │ 0.415 0.00951 -0.4057 -97.71% 154 rocq-mathcomp-algebra/algebra/spectral.v.html │ │ 0.544 0.225 -0.3193 -58.69% 760 rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html │ │ 0.627 0.323 -0.3040 -48.45% 14 rocq-stdlib/theories/Numbers/Integer/Binary/ZBinary.v.html │ │ 1.15 0.857 -0.2917 -25.40% 408 rocq-stdlib/theories/MSets/MSetAVL.v.html │ │ 0.621 0.340 -0.2810 -45.23% 19 rocq-stdlib/theories/ZArith/Zcompare.v.html │ │ 0.357 0.105 -0.2515 -70.52% 558 rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html │ │ 0.588 0.339 -0.2491 -42.36% 650 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 12.1 11.9 -0.2442 -2.02% 799 rocq-metarocq-safechecker/safechecker/theories/PCUICSafeRetyping.v.html │ │ 24.9 24.6 -0.2382 -0.96% 12 coq-fourcolor/theories/proof/job503to506.v.html │ │ 0.698 0.461 -0.2372 -33.98% 689 rocq-stdlib/theories/setoid_ring/Field_theory.v.html │ │ 40.46 40.226 -0.2340 -0.58% 834 coq-vst/veric/binop_lemmas4.v.html │ │ 0.695 0.468 -0.2264 -32.58% 829 rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html │ │ 21.5 21.2 -0.2226 -1.04% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 0.231 0.00869 -0.2222 -96.24% 347 rocq-mathcomp-solvable/solvable/sylow.v.html │ │ 0.496 0.274 -0.2221 -44.80% 778 rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html │ │ 0.599 0.377 -0.2219 -37.05% 7 rocq-mathcomp-solvable/solvable/maximal.v.html │ │ 34.006 33.787 -0.2190 -0.64% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 0.225 0.00770 -0.2169 -96.57% 118 rocq-mathcomp-algebra/algebra/spectral.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Member
Author
|
@coqbot ci minimize |
Contributor
|
I have initiated minimization at commit e8d41ee for the suggested target ci-rewriter as requested. |
Contributor
|
Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/rewriter/src/Rewriter/Demo.v in 3h 10m 55s (from ci-rewriter) (full log on GitHub Actions - verbose log) We are collecting data on the user experience of the Coq Bug Minimizer. ⭐ 🏗️ Partially Minimized Coq File (could not inline Rewriter.Util.plugins.RewriterBuildRegistry)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "+implicit-core-hint-db,+implicits-in-term,+non-reversible-notation,+deprecated-intros-until-0,+deprecated-focus,+unused-intro-pattern,+deprecated-hint-constr,+fragile-hint-constr,+variable-collision,+unexpected-implicit-declaration,+omega-is-deprecated,+deprecated-instantiate-syntax,+non-recursive,+deprecated-hint-rewrite-without-locality,+deprecated-hint-without-locality,+deprecated-instance-without-locality,+undeclared-scope,+deprecated-typeclasses-transparency-without-locality,+future-coercion-class-field,unsupported-attributes" "-w" "-notation-overridden,-unusable-identifier" "-w" "-notation-overridden" "-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/rewriter/src/Rewriter" "Rewriter" "-Q" "/github/workspace/cwd" "Top" "-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/Stdlib" "Stdlib" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/rewriter/src/Rewriter/Util/plugins" "-top" "Rewriter.Demo") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 95 lines to 6 lines, then from 20 lines to 402 lines, then from 409 lines to 8 lines, then from 22 lines to 8 lines, then from 21 lines to 8 lines, then from 22 lines to 8 lines *)
(* coqc version 9.3+alpha compiled with OCaml 4.14.2
coqtop version 9.3+alpha
Modules that could not be inlined: Rewriter.Util.plugins.RewriterBuildRegistry
Expected coqc runtime on this file: 5.675 sec
Expected coqc peak memory usage on this file: 791192.0 kb *)
Require Rewriter.Util.plugins.RewriterBuildRegistry.
Declare ML Module "coq-rewriter.rewriter_build".
Import Stdlib.Arith.Arith.
Make rew0nat := Rewriter For (Nat.add_0_r, Nat.add_0_l).🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 6.0KiB; full 17KiB file on GitHub Actions Artifacts under
|
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
2 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.
This is probably going to break some developments like fiat-crypto and friends, so for now I'm just running the CI and if there is too much breakage I'll provide a (deprecated) compatibility flag.
Fixes #7905: abstract in tactics in terms should not inline.