Reimplement Ncring_tac reification in ltac instead of typeclasses #18325
Conversation
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
|
@coqbot bench |
Janno
reviewed
Nov 15, 2023
theories/setoid_ring/Ncring_tac.v
Outdated
Comment on lines
58
to
61
| | (Ring (add:=?op), ?op ?t1 ?t2) => | ||
| let et1 := reify_term Tring lvar t1 in | ||
| let et2 := reify_term Tring lvar t2 in | ||
| open_constr:(PEadd et1 et2) |
There was a problem hiding this comment.
Would it make sense to use uconstr here and below to avoid the quadratic overhead from typechecking in open_constr?
There was a problem hiding this comment.
There is no quadratic overhead from typechecking. There was quadratic overhead from evar normalization until #17704
There was a problem hiding this comment.
Indeed, @SkySkimmer you should use uconstr otherwise we're still going to pay too much.
There was a problem hiding this comment.
The bench shall tell (unless fiat crypto is the only significant user and crashes from using the reification functions directly I guess)
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
|
🏁 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 │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 295.1610 295.9510 0.7900 0.27% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 63.3280 63.9020 0.5740 0.91% 139 coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html │ │ 59.0020 59.4120 0.4100 0.69% 609 coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │ │ 2.5310 2.9130 0.3820 15.09% 487 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 17.3730 17.7540 0.3810 2.19% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ │ 1.1730 1.5100 0.3370 28.73% 853 coq-stdlib/FSets/FMapAVL.v.html │ │ 42.7870 43.0540 0.2670 0.62% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 42.3330 42.5730 0.2400 0.57% 224 coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html │ │ 2.3260 2.5650 0.2390 10.28% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 114.7390 114.9510 0.2120 0.18% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 28.1170 28.3250 0.2080 0.74% 194 coq-vst/veric/expr_lemmas4.v.html │ │ 35.2800 35.4770 0.1970 0.56% 79 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │ │ 0.8380 1.0270 0.1890 22.55% 384 coq-stdlib/MSets/MSetAVL.v.html │ │ 46.0470 46.2280 0.1810 0.39% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 4.3190 4.4930 0.1740 4.03% 279 coq-vst/veric/SeparationLogicSoundness.v.html │ │ 5.5900 5.7570 0.1670 2.99% 605 coq-unimath/UniMath/CategoryTheory/categories/KleisliCategory.v.html │ │ 114.6990 114.8510 0.1520 0.13% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 0.4160 0.5610 0.1450 34.86% 82 coq-stdlib/Numbers/Cyclic/Int63/Sint63.v.html │ │ 12.4860 12.6290 0.1430 1.15% 1028 coq-unimath/UniMath/CategoryTheory/LocalizingClass.v.html │ │ 1.1630 1.3010 0.1380 11.87% 316 coq-stdlib/Strings/Byte.v.html │ │ 0.0840 0.2160 0.1320 157.14% 183 coq-vst/veric/SeparationLogicSoundness.v.html │ │ 0.1630 0.2920 0.1290 79.14% 744 coq-vst/veric/SequentialClight2.v.html │ │ 0.0100 0.1360 0.1260 1260.00% 972 coq-vst/veric/SequentialClight2.v.html │ │ 0.0000 0.1240 0.1240 inf% 976 coq-vst/veric/SequentialClight.v.html │ │ 19.4920 19.6160 0.1240 0.64% 214 coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 0.9360 0.5670 -0.3690 -39.42% 170 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 143.4950 143.2050 -0.2900 -0.20% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 7.6400 7.3780 -0.2620 -3.43% 293 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │ │ 43.0690 42.8110 -0.2580 -0.60% 236 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 43.0860 42.8330 -0.2530 -0.59% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 14.9280 14.6760 -0.2520 -1.69% 1265 coq-verdi-raft/theories/Raft/CommonTheorems.v.html │ │ 0.9050 0.6560 -0.2490 -27.51% 160 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 13.9890 13.7440 -0.2450 -1.75% 490 coq-unimath/UniMath/HomologicalAlgebra/KA.v.html │ │ 10.3610 10.1370 -0.2240 -2.16% 496 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 13.7590 13.5630 -0.1960 -1.42% 88 coq-rewriter/src/Rewriter/Rewriter/Examples.v.html │ │ 17.0960 16.9070 -0.1890 -1.11% 196 coq-unimath/UniMath/HomologicalAlgebra/KATriangulated.v.html │ │ 0.5280 0.3540 -0.1740 -32.95% 868 coq-stdlib/MSets/MSetRBT.v.html │ │ 4.5200 4.3570 -0.1630 -3.61% 318 coq-unimath/UniMath/CategoryTheory/EnrichedCats/YonedaLemma.v.html │ │ 17.4670 17.3100 -0.1570 -0.90% 957 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v.html │ │ 18.0760 17.9210 -0.1550 -0.86% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 0.3090 0.1550 -0.1540 -49.84% 905 coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │ │ 7.8950 7.7410 -0.1540 -1.95% 571 coq-verdi-raft/theories/Raft/CommonTheorems.v.html │ │ 0.6160 0.4630 -0.1530 -24.84% 21 coq-stdlib/MSets/MSetPositive.v.html │ │ 7.9950 7.8440 -0.1510 -1.89% 468 coq-unimath/UniMath/HomologicalAlgebra/KA.v.html │ │ 0.2970 0.1500 -0.1470 -49.49% 811 coq-stdlib/MSets/MSetRBT.v.html │ │ 0.4780 0.3330 -0.1450 -30.33% 1363 coq-stdlib/FSets/FMapAVL.v.html │ │ 24.6490 24.5060 -0.1430 -0.58% 454 coq-unimath/UniMath/SyntheticHomotopyTheory/Circle2.v.html │ │ 0.3460 0.2070 -0.1390 -40.17% 163 coq-stdlib/Numbers/HexadecimalPos.v.html │ │ 0.1610 0.0260 -0.1350 -83.85% 260 coq-vst/atomics/SC_atomics_base.v.html │ │ 0.1510 0.0160 -0.1350 -89.40% 108 coq-vst/atomics/SC_atomics_base.v.html │ └────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
🔴 CI failures at commit df45fd0 without any failure in the test-suite ✔️ Corresponding jobs for the base commit 56a7f9c succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
@coqbot ci minimize ci-analysis |
|
I am now running minimization at commit df45fd0 on requested target ci-analysis. I'll come back to you with the results once it's done. |
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/analysis/theories/trigo.v (from ci-analysis) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Partially Minimized Coq File (timeout) (truncated to 32KiB; full 182KiB file on GitHub Actions Artifacts under
|
df45fd0 to
e70d0c3
Compare
e70d0c3 to
a5617de
Compare
a5617de to
dcffc7f
Compare
|
Minimized File /github/workspace/builds/coq/coq-failing/_build_ci/analysis/theories/trigo.v (from ci-analysis) (interrupted by timeout, being automatically continued) (full log on GitHub Actions) Partially Minimized Coq File (timeout) (truncated to 32KiB; full 33KiB file on GitHub Actions Artifacts under
|
|
Minimized File (from ci-analysis) (full log on GitHub Actions) We are collecting data on the user experience of the Coq Bug Minimizer. Minimized Coq File (truncated to 32KiB; full 33KiB file on GitHub Actions Artifacts under
|
dcffc7f to
95769b8
Compare
|
The job library:ci-fiat_crypto_legacy has failed in allow failure mode |
|
🏁 Bench results: INFO: failed to install 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 42.8400 43.4260 0.5860 1.37% 236 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 1.9870 2.4820 0.4950 24.91% 736 coq-stdlib/Reals/Cauchy/ConstructiveCauchyReals.v.html │ │ 0.2180 0.5560 0.3380 155.05% 12 coq-stdlib/MSets/MSets.v.html │ │ 27.4580 27.7670 0.3090 1.13% 12 coq-fourcolor/theories/job618to622.v.html │ │ 7.4000 7.6940 0.2940 3.97% 1225 coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.v.html │ │ 28.8600 29.1510 0.2910 1.01% 12 coq-fourcolor/theories/job531to534.v.html │ │ 26.7790 27.0580 0.2790 1.04% 12 coq-fourcolor/theories/job319to322.v.html │ │ 0.6300 0.8850 0.2550 40.48% 170 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 24.4720 24.7230 0.2510 1.03% 12 coq-fourcolor/theories/job303to306.v.html │ │ 0.7020 0.9380 0.2360 33.62% 160 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 0.0870 0.2750 0.1880 216.09% 312 coq-stdlib/Reals/Abstract/ConstructiveAbs.v.html │ │ 33.9610 34.1430 0.1820 0.54% 12 coq-fourcolor/theories/job254to270.v.html │ │ 0.6070 0.7710 0.1640 27.02% 200 coq-stdlib/Numbers/HexadecimalNat.v.html │ │ 6.5580 6.7130 0.1550 2.36% 604 coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │ │ 0.1250 0.2740 0.1490 119.20% 811 coq-stdlib/Reals/Abstract/ConstructiveReals.v.html │ │ 0.4030 0.5500 0.1470 36.48% 82 coq-stdlib/Numbers/Cyclic/Int63/Sint63.v.html │ │ 0.2110 0.3580 0.1470 69.67% 16 coq-stdlib/Numbers/HexadecimalZ.v.html │ │ 0.4700 0.6160 0.1460 31.06% 21 coq-stdlib/MSets/MSetPositive.v.html │ │ 27.3050 27.4490 0.1440 0.53% 12 coq-fourcolor/theories/job291to294.v.html │ │ 0.2350 0.3750 0.1400 59.57% 17 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 29.1290 29.2560 0.1270 0.44% 12 coq-fourcolor/theories/job190to206.v.html │ │ 25.7430 25.8670 0.1240 0.48% 12 coq-fourcolor/theories/job295to298.v.html │ │ 10.1680 10.2890 0.1210 1.19% 279 coq-category-theory/Theory/Metacategory.v.html │ │ 10.1580 10.2780 0.1200 1.18% 496 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 0.1050 0.2250 0.1200 114.29% 853 coq-stdlib/MSets/MSetRBT.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 3.0340 2.2750 -0.7590 -25.02% 490 coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html │ │ 142.7730 142.0900 -0.6830 -0.48% 1190 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 43.4680 42.8120 -0.6560 -1.51% 236 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │ │ 18.4430 17.9400 -0.5030 -2.73% 12 coq-fourcolor/theories/job235to238.v.html │ │ 300.8320 300.3560 -0.4760 -0.16% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 43.6090 43.1400 -0.4690 -1.08% 827 coq-vst/veric/binop_lemmas4.v.html │ │ 27.9280 27.5140 -0.4140 -1.48% 12 coq-fourcolor/theories/job223to226.v.html │ │ 1.5300 1.1420 -0.3880 -25.36% 853 coq-stdlib/FSets/FMapAVL.v.html │ │ 16.5270 16.1420 -0.3850 -2.33% 12 coq-fourcolor/theories/job215to218.v.html │ │ 10.6470 10.3120 -0.3350 -3.15% 790 coq-metacoq-safechecker/safechecker/theories/PCUICSafeRetyping.v.html │ │ 10.4230 10.1030 -0.3200 -3.07% 496 coq-rewriter/src/Rewriter/Rewriter/Wf.v.html │ │ 35.2840 34.9660 -0.3180 -0.90% 97 coq-vst/veric/binop_lemmas5.v.html │ │ 17.5830 17.2670 -0.3160 -1.80% 957 coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v.html │ │ 18.5580 18.2460 -0.3120 -1.68% 32 coq-performance-tests-lite/src/pattern.v.html │ │ 45.5070 45.2060 -0.3010 -0.66% 558 coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html │ │ 26.4340 26.1350 -0.2990 -1.13% 12 coq-fourcolor/theories/job231to234.v.html │ │ 20.8100 20.5120 -0.2980 -1.43% 1073 coq-metacoq-safechecker/safechecker/theories/PCUICSafeReduce.v.html │ │ 27.4680 27.1790 -0.2890 -1.05% 12 coq-fourcolor/theories/job299to302.v.html │ │ 31.5690 31.2920 -0.2770 -0.88% 839 coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html │ │ 33.8730 33.6160 -0.2570 -0.76% 12 coq-fourcolor/theories/job001to106.v.html │ │ 35.0330 34.7950 -0.2380 -0.68% 79 coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.v.html │ │ 29.3100 29.0740 -0.2360 -0.81% 147 coq-vst/veric/expr_lemmas4.v.html │ │ 26.4260 26.1940 -0.2320 -0.88% 12 coq-fourcolor/theories/job486to489.v.html │ │ 32.8650 32.6360 -0.2290 -0.70% 12 coq-fourcolor/theories/job323to383.v.html │ │ 17.9440 17.7350 -0.2090 -1.16% 31 coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html │ └───────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
|
🔴 CI failures at commit 95769b8 without any failure in the test-suite ✔️ Corresponding jobs for the base commit 5883afa succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
JasonGross
pushed a commit
to mit-plv/fiat-crypto
that referenced
this pull request
Nov 23, 2023
|
Can we get one last entire bench to get the full picture? @coqbot bench |
|
Quick Ltac2 implem: Module ReDef.
Import Ncring_tac Ncring_polynom.
Require Import Ltac2.Ltac2.
Import Printf.
Ltac2 rec reify_as_var_aux n lvar term :=
lazy_match! lvar with
| @cons _ ?t0 ?tl =>
match Control.case (fun () => Unification.unify_with_full_ts term t0) with
| Val _ => n
| Err _ => reify_as_var_aux open_constr:(S $n) tl term
end
| _ =>
Unification.unify_with_full_ts lvar open_constr:(@cons _ $term _);
n
end.
Ltac2 reify_as_var lvar term := reify_as_var_aux 'Datatypes.O lvar term.
Ltac2 rec close_varlist lvar :=
lazy_match! lvar with
| @nil _ => ()
| @cons _ _ ?tl => close_varlist tl
| _ => let _ := open_constr:(eq_refl : $lvar = @nil _) in ()
end.
Ltac2 Type ring_ops := {
car : constr;
ring0 : constr;
ring1 : constr;
add : constr;
mul : constr;
sub : constr;
opp : constr;
}.
Ltac2 convert := Unification.unify_with_full_ts.
Ltac2 rec reify_term tring lvar term :=
match! term with
| Z0 => '(PEc $term)
| Zpos _ => '(PEc $term)
| Zneg _ => '(PEc $term)
| _ => convert (tring.(ring0)) term; '(PEc 0%Z)
| _ => convert (tring.(ring1)) term; '(PEc 1%Z)
| ?op ?t1 ?t2 =>
let r := tring.(car) in
let _ := open_constr:($t1 : $r) in
let _ := open_constr:($t2 : $r) in
match! 'tt with
| _ =>
convert (tring.(add)) op;
let et1 := reify_term tring lvar t1 in
let et2 := reify_term tring lvar t2 in
'(PEadd $et1 $et2)
| _ =>
convert (tring.(mul)) op;
let et1 := reify_term tring lvar t1 in
let et2 := reify_term tring lvar t2 in
'(PEmul $et1 $et2)
| _ =>
convert (tring.(sub)) op;
let et1 := reify_term tring lvar t1 in
let et2 := reify_term tring lvar t2 in
'(PEsub $et1 $et2)
end
| ?op ?t =>
convert (tring.(opp)) op;
let et := reify_term tring lvar t in
'(PEopp $et)
| (@multiplication Z _ _ ?z ?t) =>
let et := reify_term tring lvar t in
'(PEmul (PEc $z) $et)
| (pow_N ?t ?n) =>
let et := reify_term tring lvar t in
'(PEpow $et $n)
| (@power _ _ power_ring ?t ?n) =>
let et := reify_term tring lvar t in
'(PEpow $et (ZN $n))
| _ =>
(* let extra := ltac1val:(x |- extra_reify x) (Ltac1.of_constr term) in *)
(* let extra := *)
(* match Ltac1.to_constr extra with *)
(* | Some v => v *)
(* | None => Control.throw Assertion_failure *)
(* end *)
(* in *)
(* lazy_match! extra with *)
(* | (false, _) => *)
let n := reify_as_var lvar term in
'(PEX Z (Pos.of_succ_nat $n))
(* | (true, ?v) => v *)
(* end *)
end.
Ltac2 rec list_reifyl_core tring lvar lterm :=
lazy_match! lterm with
| @nil _ => '(@nil (PExpr Z))
| @cons _ ?t ?tl =>
let et := reify_term tring lvar t in
let etl := list_reifyl_core tring lvar tl in
'(@cons (PExpr Z) $et $etl)
end.
Ltac2 list_reifyl lvar lterm :=
lazy_match! lterm with
| @cons ?r _ _ =>
let r_ring := constr:(_ : Ring (T:=$r)) in
let t_ring :=
match Constr.Unsafe.kind r_ring with
| Constr.Unsafe.Cast _ _ t => t
| _ => Control.throw Assertion_failure
end
in
let tring :=
lazy_match! t_ring with
| Ring (ring0:=?ring0) (ring1:=?ring1) (add:=?add) (mul:=?mul) (sub:=?sub) (opp:=?opp)
=> { car := r; ring0; ring1; add; mul; sub; opp }
end
in
let lexpr := list_reifyl_core tring lvar lterm in
close_varlist lvar;
let res := open_constr:(($lvar, $lexpr)) in
res
end.
Ltac2 list_reifyl_interop lvar lterm :=
match Ltac1.to_constr lvar with
| None => Control.throw Assertion_failure
| Some lvar =>
match Ltac1.to_constr lterm with
| None => Control.throw Assertion_failure
| Some lterm => Ltac1.of_constr (list_reifyl lvar lterm)
end
end.
Ltac list_reifyl lvar lterm ::=
let call := ltac2val:(lvar lterm |- list_reifyl_interop lvar lterm) in call lvar lterm.
End ReDef.(there is some issue with the commented on https://github.com/mit-plv/fiat-crypto/blob/c74c06af6bc158f79b70b52f7e9fc9bbae017a57/src/Curves/Weierstrass/AffineProofs.v#L48 with
Probably the code could still be optimized (use of unsafe constr, avoid using backtrack for flow control...) |
|
🏁 Bench results: 🐢 Top 25 slow downs┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SLOW DOWNS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 54.5280 55.4550 0.9270 1.70% 915 coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html │ │ 33.8100 34.5040 0.6940 2.05% 2 coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html │ │ 3.3320 3.9510 0.6190 18.58% 130 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 114.7410 115.2920 0.5510 0.48% 999 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 84.2690 84.7800 0.5110 0.61% 20 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html │ │ 114.7600 115.2690 0.5090 0.44% 968 coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │ │ 4.3440 4.7730 0.4290 9.88% 102 coq-engine-bench-lite/coq/PerformanceDemos/rewrite_strat_repeated_app.v.html │ │ 12.5110 12.8840 0.3730 2.98% 1555 coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html │ │ 93.2380 93.5930 0.3550 0.38% 103 coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html │ │ 27.4640 27.8120 0.3480 1.27% 12 coq-fourcolor/theories/job503to506.v.html │ │ 28.1250 28.4710 0.3460 1.23% 12 coq-fourcolor/theories/job535to541.v.html │ │ 21.7790 22.1150 0.3360 1.54% 12 coq-fourcolor/theories/job507to510.v.html │ │ 1.0890 1.3660 0.2770 25.44% 937 coq-vst/veric/binop_lemmas2.v.html │ │ 26.5580 26.8310 0.2730 1.03% 12 coq-fourcolor/theories/job486to489.v.html │ │ 26.0480 26.3150 0.2670 1.03% 12 coq-fourcolor/theories/job554to562.v.html │ │ 11.1510 11.4180 0.2670 2.39% 55 coq-category-theory/Construction/Comma/Natural/Transformation.v.html │ │ 0.0420 0.3010 0.2590 616.67% 115 coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/Primitives.v.html │ │ 0.2790 0.5310 0.2520 90.32% 110 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/WordByWordMontgomery.v.html │ │ 0.0140 0.2590 0.2450 1750.00% 304 coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/UnsaturatedSolinas.v.html │ │ 0.0200 0.2630 0.2430 1215.00% 481 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/UnsaturatedSolinas.v.html │ │ 0.0020 0.2450 0.2430 12150.00% 241 coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/WordByWordMontgomery.v.html │ │ 16.9890 17.2290 0.2400 1.41% 24 coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MulSplit.v.html │ │ 10.1940 10.4310 0.2370 2.32% 496 coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Wf.v.html │ │ 2.5890 2.8230 0.2340 9.04% 487 coq-stdlib/Numbers/HexadecimalFacts.v.html │ │ 6.6980 6.9250 0.2270 3.39% 5 coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_mul_optimised_seed12.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ 🐇 Top 25 speed ups┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ TOP 25 SPEED UPS │ │ │ │ OLD NEW DIFF %DIFF Ln FILE │ ├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤ │ 114.8740 79.9170 -34.9570 -30.43% 48 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html │ │ 22.9140 5.3370 -17.5770 -76.71% 233 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 40.1810 24.8430 -15.3380 -38.17% 85 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html │ │ 16.0950 3.7150 -12.3800 -76.92% 262 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 14.8680 10.1060 -4.7620 -32.03% 212 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 12.0130 7.7210 -4.2920 -35.73% 258 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 28.8980 25.0000 -3.8980 -13.49% 129 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 8.0850 5.5290 -2.5560 -31.61% 198 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Projective.v.html │ │ 11.0210 8.6800 -2.3410 -21.24% 159 coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html │ │ 22.4100 20.3060 -2.1040 -9.39% 219 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 4.4250 2.3380 -2.0870 -47.16% 524 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian.v.html │ │ 5.1270 3.1750 -1.9520 -38.07% 542 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian.v.html │ │ 6.3350 4.4000 -1.9350 -30.54% 207 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 3.4450 1.6170 -1.8280 -53.06% 76 coq-fiat-crypto-with-bedrock/src/Curves/Edwards/AffineProofs.v.html │ │ 2.5570 0.8830 -1.6740 -65.47% 236 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 3.6320 2.4610 -1.1710 -32.24% 222 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 2.3800 1.2240 -1.1560 -48.57% 548 coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian.v.html │ │ 3.9100 2.8180 -1.0920 -27.93% 126 coq-fiat-crypto-with-bedrock/src/Curves/Edwards/XYZT/Basic.v.html │ │ 2.2280 1.1470 -1.0810 -48.52% 270 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 2.9870 1.9140 -1.0730 -35.92% 242 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 298.3850 297.3750 -1.0100 -0.34% 8 coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │ │ 53.6930 52.7190 -0.9740 -1.81% 50 coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html │ │ 2.2570 1.3830 -0.8740 -38.72% 234 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 3.2530 2.3960 -0.8570 -26.34% 213 coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html │ │ 166.3380 165.4890 -0.8490 -0.51% 233 coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ |
ppedrot
reviewed
Nov 25, 2023
While we may at some point use an ocaml (or Ltac2?) implementation (for instance variable list manipulation is still done by side effect through the evar map, not the nicest), this helps find out what the typeclasses do when reifying. Notable finds: - the `reify` typeclass gets 1 instance outside Ncring_tac, from nsatz to reify IZR applied to ground ints. We replace this with a tactic redefition. Alternatives welcomed (redefinition isn't very modular so if we find another case we will have to come up with something). - comparison up to conversion is necessary for some users, notably https://github.com/math-comp/analysis/blob/master/theories/nsatz_realtype.v
3eaadd5 to
b3663ed
Compare
|
🔴 CI failure at commit b3663ed without any failure in the test-suite ✔️ Corresponding job for the base commit ababbf4 succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
|
spurious, cf #18374 (comment) |
|
🔴 CI failure at commit b3663ed without any failure in the test-suite ✔️ Corresponding job for the base commit ababbf4 succeeded ❔ Ask me to try to extract a minimal test case that can be added to the test-suite 🏃
|
1 similar comment
This comment was marked as duplicate.
This comment was marked as duplicate.
|
@coqbot merge now |
|
@ppedrot: You can't merge the PR because it hasn't been approved yet. |
ppedrot
approved these changes
Dec 9, 2023
|
@coqbot merge now |
SkySkimmer
added a commit
to SkySkimmer/rocq
that referenced
this pull request
Dec 11, 2023
…ltac instead of typeclasses
3 tasks
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.
While we may at some point use an ocaml (or Ltac2?) implementation (for instance variable list manipulation is still done by side effect through the evar map, not the nicest), this helps find out what the typeclasses do when reifying.
Notable finds:
the
reifytypeclass gets 1 instance outside Ncring_tac, from nsatz to reify IZR applied to ground ints. We replace this with a tactic redefition. Alternatives welcomed (redefinition isn't very modular so if we find another case we will have to come up with something).typeclasses do some conversion, eg the instance
will also apply to
@zero R (@zero_notation R op ...). The reimplementation matches syntacticallyop(the one appearing in the type of the proof ofRingprealably inferred) and@zero _ _.Overlays: