Defunctionalize the proof term in Rewrite internals.#22046
Open
ppedrot wants to merge 2 commits into
Open
Conversation
ppedrot
added
kind: cleanup
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
@coqbot ci minimize |
Contributor
|
I have initiated minimization at commit 7e7198f for the suggested target ci-fiat_parsers as requested. |
Contributor
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/fiat_parsers/src/Common/List/ListMorphisms.v in 45m 57s (from ci-fiat_parsers) (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" "-require-import" "Coq.Compat.AdmitAxiom") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 565 lines to 36 lines, then from 50 lines to 635 lines, then from 642 lines to 48 lines, then from 62 lines to 2110 lines, then from 2112 lines to 57 lines, then from 71 lines to 1256 lines, then from 1255 lines to 68 lines, then from 82 lines to 4215 lines, then from 4195 lines to 129 lines, then from 143 lines to 157 lines, then from 164 lines to 141 lines, then from 155 lines to 169 lines, then from 176 lines to 152 lines, then from 166 lines to 180 lines, then from 187 lines to 163 lines, then from 178 lines to 165 lines, then from 180 lines to 69 lines, then from 84 lines to 69 lines, then from 0 lines to 69 lines *)
(* coqc version 9.3+alpha compiled with OCaml 4.14.0
coqtop version runner-khfdxfugu-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at f66fc0d0055) (f66fc0d005567e48f9eab103a6b8966fc39049cb)
Expected coqc runtime on this file: 0.000 sec
Expected coqc peak memory usage on this file: 0.0 kb *)
Require Corelib.Setoids.Setoid.
Export Corelib.Classes.Morphisms.
Export Corelib.Program.Basics.
Export Corelib.Setoids.Setoid.
Module Export List.
Set Implicit Arguments.
Section ListOps.
Variable A : Type.
Fixpoint rev (l:list A) : list A.
Admitted.
End ListOps.
Section Fold_Left_Recursor.
Variables (A : Type) (B : Type).
Variable f : A -> B -> A.
Fixpoint fold_left (l:list B) (a0:A) : A.
Admitted.
End Fold_Left_Recursor.
Section Fold_Right_Recursor.
Variables (A : Type) (B : Type).
Variable f : B -> A -> A.
Variable a0 : A.
Fixpoint fold_right (l:list B) : A.
Admitted.
End Fold_Right_Recursor.
Lemma fold_left_rev_right : forall (A B:Type)(f:A->B->B) l i,
fold_right f i (rev l) = fold_left (fun x y => f y x) l i.
Admitted.
End List.
Definition pointwise2_relation :=
fun (A A': Type) {B : Type} (R : relation B) (f g : A -> A' -> B) =>
forall a a', R (f a a') (g a a').
#[global]
Instance pointwise2_subrelation {A A' B} (R : relation B) :
subrelation (pointwise2_relation A A' R) (pointwise_relation A (pointwise_relation A' R)).
Admitted.
#[global]
Instance pointwise2_forall_relation_inv {A A' B} (R : relation B) :
subrelation (forall_relation (fun _ : A => forall_relation (fun _ : A' => R))) (pointwise2_relation A A' R).
Admitted.
Add Parametric Morphism {A B: Type} :
(@List.fold_right A B)
with signature (@pointwise2_relation B A _ eq ==> eq ==> eq ==> eq)
as fold_right_pointwise2eq_eq_eq_morphism.
Admitted.
Add Parametric Morphism {A B: Type} :
(@List.fold_left A B)
with signature (pointwise2_relation A B eq ==> eq ==> eq ==> eq)
as fold_left_pointwise2eq_eq_eq_morphism.
Proof.
intros.
rewrite <- !fold_left_rev_right.
setoid_rewrite H; reflexivity.🛠️ 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 5.7MiB file on GitHub Actions Artifacts under
|
Member
Author
|
Turns out that the order of constraint evar generation matters... |
Member
Author
|
Smaller example: Require Corelib.Setoids.Setoid.
Export Corelib.Classes.Morphisms.
Export Corelib.Setoids.Setoid.
Axiom fold_right : forall [A B : Type], (B -> A -> A) -> A.
Axiom pointwise2_relation :
forall (A A' : Type) {B : Type}, relation B -> (A -> A' -> B) -> (A -> A' -> B) -> Prop.
Declare Instance pointwise2_subrelation {A A' B} (R : relation B) :
subrelation (pointwise2_relation A A' R) (pointwise_relation A (pointwise_relation A' R)).
Declare Instance pointwise2_forall_relation_inv {A A' B} (R : relation B) :
subrelation (forall_relation (fun _ : A => forall_relation (fun _ : A' => R))) (pointwise2_relation A A' R).
Declare Instance fold_right_pointwise2eq_eq_eq_morphism : forall {A B : Type},
Proper (@pointwise2_relation B A _ eq ==> eq) (@fold_right A B).
Goal forall A B : Type,
forall f g : A -> B -> A,
pointwise2_relation A B eq f g ->
fold_right (fun (y : B) (x : A) => f x y) =
fold_right (fun (y : B) (x : A) => g x y)
.
Proof.
intros.
Set Typeclasses Debug.
setoid_rewrite H. |
ppedrot
added
the
request: full CI
ppedrot
added a commit
to ppedrot/coq
that referenced
this pull request
May 24, 2026
ppedrot
force-pushed
the
rewrite-defunctionalize-proof
branch
from
7e7198f to
517ea73
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
@coqbot bench |
Contributor
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.0706 253 253.2901 358859.41% 286 coq-fiat-crypto-with-bedrock/src/Curves/Edwards/AffineProofs.v.html │ │ 63.7 67.5 3.7913 5.95% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 236 237 1.1106 0.47% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 42.2 43.2 1.0034 2.38% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 44.2 45.2 0.9410 2.13% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 26.8 27.6 0.8438 3.15% 34 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 45.8 46.6 0.7989 1.75% 115 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 0.690 1.37 0.6801 98.51% 816 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 44.2 44.9 0.6691 1.51% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 45.9 46.5 0.6562 1.43% 115 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 133 134 0.5789 0.43% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 29.0 29.5 0.5766 1.99% 31 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html │ │ 55.1 55.6 0.5242 0.95% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 10.8 11.3 0.4601 4.26% 159 coq-fiat-crypto-with-bedrock/src/Bedrock/P256.v.html │ │ 20.5 21.0 0.4571 2.22% 708 coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html │ │ 9.04 9.49 0.4512 4.99% 435 coq-mathcomp-odd-order/theories/PFsection12.v.html │ │ 21.3 21.7 0.4242 1.99% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 27.9 28.4 0.4164 1.49% 13 coq-fourcolor/theories/proof/job107to164.v.html │ │ 29.7 30.1 0.3892 1.31% 13 coq-fourcolor/theories/proof/job001to106.v.html │ │ 79.9 80.3 0.3731 0.47% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 35.2 35.5 0.3487 0.99% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 21.4 21.7 0.3302 1.55% 13 coq-fourcolor/theories/proof/job511to516.v.html │ │ 9.88 10.2 0.3299 3.34% 326 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 24.1 24.4 0.3229 1.34% 345 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 7.22 7.53 0.3098 4.29% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 67.6 62.8 -4.8187 -7.13% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 89.8 88.8 -1.0051 -1.12% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 31.3 30.3 -0.9262 -2.96% 198 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.4 30.5 -0.8855 -2.82% 180 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 46.7 45.8 -0.8417 -1.80% 277 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 31.5 30.6 -0.8364 -2.66% 214 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 41.6 40.8 -0.8261 -1.98% 235 coq-category-theory/Construction/DecoratedCospan/Category.v.html │ │ 43.6 42.8 -0.7225 -1.66% 578 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html │ │ 90.5 89.8 -0.7184 -0.79% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 39.4 38.7 -0.7160 -1.82% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 201 200 -0.6879 -0.34% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 34.1 33.5 -0.6438 -1.89% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 31.3 30.7 -0.6302 -2.01% 139 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 31.5 30.9 -0.6078 -1.93% 148 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 107 106 -0.5571 -0.52% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 29.1 28.6 -0.5376 -1.85% 305 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 35.2 34.7 -0.5361 -1.52% 194 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 1.02 0.500 -0.5169 -50.84% 484 rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html │ │ 48.8 48.3 -0.5112 -1.05% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 23.6 23.1 -0.5010 -2.13% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 31.2 30.7 -0.4727 -1.52% 166 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 2.71 2.24 -0.4704 -17.37% 45 coq-engine-bench-lite/coq/PerformanceDemos/rewrite_strat_repeated_app.v.html │ │ 37.1 36.6 -0.4351 -1.17% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 50.0 49.6 -0.4201 -0.84% 567 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 27.5 27.1 -0.3846 -1.40% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
Contributor
|
the whole slowdown is 1 line in fiat crypto |
Member
Author
|
Yes, the very same line timeouts the CI on fcl. I have to investigate where the difference comes from... |
Member
Author
|
OK, it looks like it comes from the order of evars generated by transitivity. I'm investigating. |
ppedrot
added
the
request: full CI
ppedrot
added a commit
to ppedrot/coq
that referenced
this pull request
May 28, 2026
ppedrot
force-pushed
the
rewrite-defunctionalize-proof
branch
from
517ea73 to
5f84705
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
Should be fixed now. |
Member
Author
|
This looks ready. |
Member
|
Let's get a last bench |
Member
|
@coqbot bench |
github-actions
Bot
added
the
needs: rebase
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 │ ├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 63.3 67.2 3.9200 6.20% 608 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 25.1 25.6 0.5199 2.07% 788 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 35.0 35.4 0.3655 1.04% 194 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html │ │ 3.17 3.53 0.3561 11.23% 130 coq-category-theory/Functor/Strong/Product.v.html │ │ 33.5 33.8 0.3211 0.96% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 0.287 0.592 0.3048 106.14% 11 rocq-stdlib/theories/omega/OmegaLemmas.v.html │ │ 28.5 28.8 0.2899 1.02% 305 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html │ │ 0.379 0.662 0.2832 74.74% 14 rocq-stdlib/theories/MSets/MSetToFiniteSet.v.html │ │ 0.323 0.606 0.2829 87.55% 11 rocq-stdlib/theories/ZArith/Zquot.v.html │ │ 4.47 4.74 0.2670 5.97% 441 coq-fiat-crypto-with-bedrock/src/AbstractInterpretation/Wf.v.html │ │ 0.279 0.542 0.2630 94.11% 596 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.322 0.582 0.2605 80.99% 11 rocq-stdlib/theories/ZArith/Zdiv_facts.v.html │ │ 35.1 35.4 0.2605 0.74% 835 coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html │ │ 0.724 0.979 0.2554 35.29% 41 rocq-stdlib/theories/ZArith/Zdiv_facts.v.html │ │ 20.3 20.5 0.2497 1.23% 6 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html │ │ 15.2 15.5 0.2440 1.60% 898 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ │ 0.234 0.472 0.2384 101.87% 1 rocq-stdlib/theories/ZArith/Zcong.v.html │ │ 0.219 0.453 0.2340 106.73% 1166 rocq-stdlib/theories/Strings/Byte.v.html │ │ 0.643 0.873 0.2299 35.76% 829 rocq-stdlib/theories/setoid_ring/Ring_polynom.v.html │ │ 48.3 48.5 0.2280 0.47% 376 coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html │ │ 0.998 1.22 0.2241 22.45% 702 rocq-stdlib/theories/Numbers/HexadecimalFacts.v.html │ │ 16.6 16.8 0.2234 1.35% 669 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 200 200 0.2193 0.11% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 38.8 39.0 0.2122 0.55% 1423 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │ │ 22.5 22.7 0.2065 0.92% 776 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html │ └──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 49.6 46.9 -2.7322 -5.51% 115 coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │ │ 45.6 44.4 -1.1748 -2.58% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html │ │ 64.5 63.5 -0.9512 -1.48% 608 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 80.6 79.8 -0.8286 -1.03% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 43.4 42.7 -0.7517 -1.73% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 237 236 -0.7227 -0.31% 141 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 45.3 44.5 -0.7124 -1.57% 3 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html │ │ 21.9 21.4 -0.5169 -2.36% 651 rocq-stdlib/theories/Zmod/ZmodBase.v.html │ │ 55.3 54.9 -0.4785 -0.86% 27 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html │ │ 107 106 -0.4778 -0.45% 22 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html │ │ 134 133 -0.4567 -0.34% 155 coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html │ │ 7.38 6.94 -0.4489 -6.08% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 88.7 88.3 -0.4462 -0.50% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 0.661 0.263 -0.3986 -60.29% 398 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 27.2 26.9 -0.3625 -1.33% 68 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │ │ 7.54 7.20 -0.3344 -4.44% 602 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 30.7 30.4 -0.3265 -1.06% 596 coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html │ │ 0.982 0.658 -0.3239 -32.99% 816 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 17.9 17.6 -0.3166 -1.77% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 21.6 21.3 -0.3053 -1.41% 242 coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html │ │ 21.5 21.2 -0.3045 -1.41% 516 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 10.2 9.91 -0.2929 -2.87% 326 coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html │ │ 1.55 1.26 -0.2873 -18.59% 813 rocq-stdlib/theories/MSets/MSetRBT.v.html │ │ 13.0 12.7 -0.2826 -2.17% 571 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html │ │ 23.5 23.2 -0.2811 -1.20% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
ppedrot
added
the
request: full CI
ppedrot
added a commit
to ppedrot/coq
that referenced
this pull request
Jun 1, 2026
ppedrot
force-pushed
the
rewrite-defunctionalize-proof
branch
from
5f84705 to
0091433
Compare
coqbot-app
Bot
removed
request: full CI
Member
Author
|
@coqbot run full ci |
Member
Author
|
VST failure is unrelated, @mattam82 this is ready to go. |
ppedrot
added
the
request: full CI
This is mostly about moving code around so as to obtain an explicit representation of the rewrite proof as an inductive type rather than through term generation spread around the setoid rewrite internals.
ppedrot
force-pushed
the
rewrite-defunctionalize-proof
branch
from
0091433 to
521024c
Compare
coqbot-app
Bot
removed
the
request: full CI
Member
Author
|
ping @mattam82 |
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.
This is mostly about moving code around so as to obtain an explicit representation of the rewrite proof as an inductive type rather than through term generation spread around the setoid rewrite internals.