gares
commented
11 months ago Great! I can't really understand the timing on analysis. What is the non-master time?
Closed proux01 closed 11 months ago
gares
commented
11 months ago Great! I can't really understand the timing on analysis. What is the non-master time?
CohenCyril
commented
11 months ago Great! I can't really understand the timing on analysis. What is the non-master time?
It's mathcomp analysis on mathcomp 2 (Mostly for performance reasons, it did not become the new master)
gares
commented
11 months ago The optimization is amazing, but I'd like to understand why. We don't have that many class projections around, no? @proux01 could you see if the perf got better evenly? Or a file had a huge speedup? Miracles...;-)
pi8027
commented
11 months ago A similar performance improvement observed in MC1: https://github.com/math-comp/math-comp/pull/591#issuecomment-694091588
proux01
commented
11 months ago could you see if the perf got better evenly? Or a file had a huge speedup? Miracles...;-)
It's very uneven, mostly concentrated on a few files. I haven't looked whether it's concentrated on some lines within those files.
Without primitive records
classical/all_classical.vo (real: 1.22, user: 1.17, sys: 0.05, mem: 654336 ko)
classical/boolp.vo (real: 2.70, user: 2.62, sys: 0.08, mem: 547064 ko)
theories/prodnormedzmodule.vo (real: 3.10, user: 3.06, sys: 0.03, mem: 643736 ko)
theories/altreals/xfinmap.vo (real: 3.39, user: 3.29, sys: 0.09, mem: 673232 ko)
theories/summability.vo (real: 3.52, user: 3.32, sys: 0.17, mem: 783056 ko)
theories/nsatz_realtype.vo (real: 3.80, user: 3.70, sys: 0.10, mem: 762276 ko)
classical/fsbigop.vo (real: 4.04, user: 3.95, sys: 0.09, mem: 684540 ko)
classical/mathcomp_extra.vo (real: 4.42, user: 4.34, sys: 0.07, mem: 649804 ko)
theories/altreals/realseq.vo (real: 4.94, user: 4.83, sys: 0.11, mem: 750876 ko)
classical/set_interval.vo (real: 5.19, user: 5.10, sys: 0.09, mem: 697944 ko)
theories/altreals/distr.vo (real: 5.99, user: 5.87, sys: 0.09, mem: 754272 ko)
theories/real_interval.vo (real: 6.12, user: 5.96, sys: 0.15, mem: 817444 ko)
theories/itv.vo (real: 6.70, user: 6.60, sys: 0.07, mem: 671680 ko)
theories/altreals/discrete.vo (real: 7.07, user: 6.99, sys: 0.08, mem: 814968 ko)
theories/forms.vo (real: 7.18, user: 7.05, sys: 0.12, mem: 823948 ko)
theories/esum.vo (real: 7.81, user: 7.65, sys: 0.15, mem: 822352 ko)
theories/altreals/realsum.vo (real: 8.64, user: 8.49, sys: 0.12, mem: 778564 ko)
theories/Rstruct.vo (real: 8.72, user: 8.58, sys: 0.13, mem: 905420 ko)
classical/cardinality.vo (real: 8.87, user: 8.78, sys: 0.08, mem: 847252 ko)
theories/hoelder.vo (real: 9.27, user: 9.16, sys: 0.10, mem: 882612 ko)
theories/reals.vo (real: 11.77, user: 11.62, sys: 0.14, mem: 875488 ko)
theories/ereal.vo (real: 12.04, user: 11.93, sys: 0.11, mem: 821560 ko)
theories/probability.vo (real: 12.54, user: 12.44, sys: 0.10, mem: 995948 ko)
classical/classical_sets.vo (real: 13.40, user: 13.27, sys: 0.12, mem: 1035916 ko)
theories/signed.vo (real: 14.88, user: 14.73, sys: 0.14, mem: 795944 ko)
theories/charge.vo (real: 19.14, user: 18.95, sys: 0.18, mem: 1105660 ko)
theories/numfun.vo (real: 19.99, user: 19.83, sys: 0.16, mem: 974892 ko)
theories/constructive_ereal.vo (real: 23.63, user: 23.58, sys: 0.05, mem: 1077136 ko)
theories/lebesgue_measure.vo (real: 24.59, user: 24.44, sys: 0.15, mem: 1057916 ko)
theories/kernel.vo (real: 25.89, user: 25.48, sys: 0.39, mem: 1810576 ko)
theories/trigo.vo (real: 29.83, user: 29.66, sys: 0.15, mem: 897240 ko)
theories/realfun.vo (real: 40.83, user: 40.66, sys: 0.16, mem: 908388 ko)
theories/exp.vo (real: 49.13, user: 48.99, sys: 0.11, mem: 907836 ko)
theories/landau.vo (real: 56.08, user: 55.95, sys: 0.11, mem: 971044 ko)
theories/derive.vo (real: 61.26, user: 61.06, sys: 0.19, mem: 1081628 ko)
theories/measure.vo (real: 71.24, user: 70.90, sys: 0.31, mem: 1731252 ko)
theories/sequences.vo (real: 75.15, user: 75.03, sys: 0.12, mem: 928432 ko)
classical/functions.vo (real: 83.73, user: 83.51, sys: 0.22, mem: 1401788 ko)
theories/topology.vo (real: 101.02, user: 100.79, sys: 0.23, mem: 1577760 ko)
theories/convex.vo (real: 124.06, user: 123.95, sys: 0.10, mem: 941112 ko)
theories/normedtype.vo (real: 124.26, user: 124.05, sys: 0.19, mem: 1579264 ko)
theories/lebesgue_integral.vo (real: 150.72, user: 150.36, sys: 0.35, mem: 1773680 ko)With primitive records
classical/all_classical.vo (real: 1.17, user: 1.10, sys: 0.07, mem: 651552 ko)
classical/boolp.vo (real: 2.62, user: 2.60, sys: 0.01, mem: 546308 ko)
theories/prodnormedzmodule.vo (real: 3.02, user: 2.96, sys: 0.05, mem: 630664 ko)
theories/altreals/xfinmap.vo (real: 3.10, user: 3.01, sys: 0.08, mem: 664752 ko)
theories/summability.vo (real: 3.38, user: 3.28, sys: 0.08, mem: 771684 ko)
theories/nsatz_realtype.vo (real: 3.70, user: 3.58, sys: 0.11, mem: 758376 ko)
classical/fsbigop.vo (real: 3.95, user: 3.84, sys: 0.09, mem: 682708 ko)
classical/mathcomp_extra.vo (real: 4.14, user: 4.07, sys: 0.06, mem: 646192 ko)
theories/altreals/realseq.vo (real: 4.67, user: 4.57, sys: 0.10, mem: 740560 ko)
classical/set_interval.vo (real: 4.74, user: 4.68, sys: 0.04, mem: 695352 ko)
theories/forms.vo (real: 5.34, user: 5.24, sys: 0.10, mem: 811284 ko)
theories/altreals/distr.vo (real: 5.66, user: 5.55, sys: 0.10, mem: 744592 ko)
theories/itv.vo (real: 5.70, user: 5.62, sys: 0.07, mem: 675184 ko)
theories/real_interval.vo (real: 6.06, user: 5.94, sys: 0.12, mem: 817420 ko)
theories/esum.vo (real: 6.92, user: 6.82, sys: 0.10, mem: 822556 ko)
theories/altreals/discrete.vo (real: 7.59, user: 7.48, sys: 0.11, mem: 811800 ko)
theories/altreals/realsum.vo (real: 7.61, user: 7.54, sys: 0.06, mem: 759928 ko)
theories/hoelder.vo (real: 7.89, user: 7.83, sys: 0.05, mem: 885864 ko)
theories/ereal.vo (real: 8.27, user: 8.15, sys: 0.12, mem: 802612 ko)
theories/Rstruct.vo (real: 8.65, user: 8.54, sys: 0.10, mem: 894972 ko)
classical/cardinality.vo (real: 8.81, user: 8.70, sys: 0.11, mem: 838188 ko)
theories/probability.vo (real: 9.50, user: 9.38, sys: 0.12, mem: 964140 ko)
theories/convex.vo (real: 9.82, user: 9.62, sys: 0.20, mem: 910252 ko)
theories/numfun.vo (real: 10.52, user: 10.44, sys: 0.08, mem: 931764 ko)
theories/realfun.vo (real: 10.85, user: 10.72, sys: 0.10, mem: 871476 ko)
theories/reals.vo (real: 11.04, user: 10.92, sys: 0.11, mem: 875536 ko)
theories/exp.vo (real: 11.30, user: 11.11, sys: 0.16, mem: 854172 ko)
theories/landau.vo (real: 11.30, user: 11.18, sys: 0.12, mem: 910128 ko)
classical/classical_sets.vo (real: 13.18, user: 13.02, sys: 0.15, mem: 1017032 ko)
theories/sequences.vo (real: 13.61, user: 13.48, sys: 0.13, mem: 889332 ko)
theories/signed.vo (real: 14.35, user: 14.21, sys: 0.14, mem: 800148 ko)
theories/charge.vo (real: 15.67, user: 15.45, sys: 0.21, mem: 1106884 ko)
theories/lebesgue_measure.vo (real: 18.93, user: 18.78, sys: 0.15, mem: 1022604 ko)
theories/trigo.vo (real: 19.01, user: 18.87, sys: 0.11, mem: 877108 ko)
theories/constructive_ereal.vo (real: 22.21, user: 22.09, sys: 0.11, mem: 1042968 ko)
theories/kernel.vo (real: 24.98, user: 24.64, sys: 0.33, mem: 1737400 ko)
theories/derive.vo (real: 29.87, user: 29.76, sys: 0.10, mem: 1038704 ko)
theories/normedtype.vo (real: 62.58, user: 62.38, sys: 0.18, mem: 1597176 ko)
theories/lebesgue_integral.vo (real: 69.13, user: 68.92, sys: 0.21, mem: 1652324 ko)
theories/measure.vo (real: 69.93, user: 69.64, sys: 0.29, mem: 1762272 ko)
classical/functions.vo (real: 84.24, user: 84.06, sys: 0.17, mem: 1388384 ko)
theories/topology.vo (real: 97.09, user: 96.86, sys: 0.20, mem: 1576552 ko)The example below from Analysis (somewhat reduced), that we started investigating with @CohenCyril four months ago, seems among the things experiencing a dramatic speedup. This could be linked to the discussion pointed by @pi8027 above: https://github.com/math-comp/math-comp/pull/462#issuecomment-598130155 . However, primitive records for classes improve things but it remains relatively slow.
From HB Require Import structures.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssralg.
From mathcomp Require Import boolp classical_sets functions.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope ring_scope.
HB.mixin Record isMeasurableFun (aT : pointedType) (rT : zmodType)
(f : aT -> rT) := {
measurable_funP : true
}.
HB.structure Definition MeasurableFun aT rT :=
{f of @isMeasurableFun aT rT f}.
Reserved Notation "{ 'mfun' aT >-> T }"
(at level 0, format "{ 'mfun' aT >-> T }").
Notation "{ 'mfun' aT >-> T }" := (@MeasurableFun.type aT T) : form_scope.
Section mfun_pred.
Context {aT : pointedType} {rT : zmodType}.
Definition mfun : {pred aT -> rT} := fun=> true.
End mfun_pred.
Section mfun.
Context {aT : pointedType} {rT : zmodType}.
Notation T := {mfun aT >-> rT}.
Notation mfun := (@mfun aT rT).
Section Sub.
Context (f : aT -> rT).
#[local] HB.instance Definition _ := @isMeasurableFun.Build aT rT f erefl.
Definition mfun_Sub : {mfun _ >-> _} := f.
End Sub.
Lemma mfun_rect (K : T -> Type) :
(forall f (Pf : f \in mfun), K (mfun_Sub f)) -> forall u : T, K u.
Proof. Admitted.
Lemma mfun_valP f (Pf : f \in mfun) : mfun_Sub f = f :> (_ -> _).
Proof. by []. Qed.
HB.instance Definition _ := isSub.Build _ _ T mfun_rect mfun_valP.
HB.instance Definition _ := [Choice of {mfun aT >-> rT} by <:].
End mfun.
Section ring.
Context (aT : pointedType) (rT : ringType).
Lemma mfun_subring_closed : zmod_closed (@mfun aT rT).
Proof. Admitted.
HB.instance Definition _ := GRing.isZmodClosed.Build _ mfun mfun_subring_closed.
HB.instance Definition _ := [SubChoice_isSubZmodule of {mfun aT >-> rT} by <:].
HB.instance Definition _ (f g : {mfun aT >-> rT}) := MeasurableFun.copy (f \+ g) (f + g).
End ring.
Section covariance_lemmas.
Context (T : pointedType) (R : comRingType).
Lemma varianceD (X Y : {mfun T >-> R}) : (X + Y)%R = (Y + Y)%R :> (_ -> _).
Proof.
Set Printing All.
Time Fail reflexivity. (* 2.167 secs -> 0.227 secs with primitive_class *)
rewrite /GRing.mul/=.
Time Fail reflexivity. (* immediate *)
Compilation of MathComp:
Compilation of Analysis: