The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Bonjour,

  La version 7.4 introduit un partage des données qui réduit
significativement la taille des .vo et le besoin en RAM. Ce partage se
traduit par un surcoût en temps au moment de Definition (ou Qed). En
moyenne ce léger surcoût est compensé par le léger gain en temps
induit par le partage.

  Dans ton cas, tu crois mesurer le temps de calcul de "Eval Compute"
seul mais tu mesures en fait aussi le temps passé à partager les
sous-termes de tes définitions (très coûteux et sans effet dans tes
exemples très particuliers). Autrement dit un "Time Eval Compute in
(mult2 nat_4k)" te montrera les mêmes performances en calcul que pour
la V7.3.1.

  Hugo

> Les résultats des tests de performances que j'ai fait avec la 7.4
> m'inquiètent un peu. Bon, c'est encore mon exemple un peu bête :
> 1+1=2, 2+2=4, 4+4=8, etc. jusqu'à 8192. (code ci-dessous)
> 
> Les timing affichés correspondent uniquement aux 4 dernières additions
> (de 1024 à 8192) :
> 
> ~>/usr/local/lib/coq-7.3.1/bin/coqc Limits.v
> Finished transaction in 0. secs (0.01u,0.s)
> Finished transaction in 0. secs (0.04u,0.s)
> Finished transaction in 0. secs (0.07u,0.s)
> Finished transaction in 0. secs (0.17u,0.s)
> 
> ~>/usr/local/lib/coq-7.4/bin/coqc Limits.v
> Finished transaction in 0. secs (0.07u,0.s)
> Finished transaction in 0. secs (0.21u,0.01s)
> Finished transaction in 1. secs (1.03u,0.s)
> Finished transaction in 6. secs (5.36u,0.02s)
> 
> Le code :
> 
> Definition mult2 [n] := (plus n n).
> 
> Definition nat_1 := Eval Compute in (S O).
> Definition nat_2 := Eval Compute in (mult2 nat_1).
> 
> Definition nat_4 := Eval Compute in (mult2 nat_2).
> Definition nat_8 := Eval Compute in (mult2 nat_4).
> Definition nat_16 := Eval Compute in (mult2 nat_8).
> Definition nat_32 := Eval Compute in (mult2 nat_16).
> 
> Definition nat_64 := Eval Compute in (mult2 nat_32).
> Definition nat_128 := Eval Compute in (mult2 nat_64).
> Definition nat_256 := Eval Compute in (mult2 nat_128).
> Definition nat_512 := Eval Compute in (mult2 nat_256).
> Time Definition nat_1k := Eval Compute in (mult2 nat_512).
> Time Definition nat_2k := Eval Compute in (mult2 nat_1k).
> Time Definition nat_4k := Eval Compute in (mult2 nat_2k).
> Time Definition nat_8k := Eval Compute in (mult2 nat_4k).
> 
> 
> -- 
> Cuihtlauac ALVARADO - France Telecom R&D - DTL/TAL
> 2, avenue Pierre Marzin - 22307 Lannion - France
> Tel: +33 2 96 05 32 73 - Fax: +33 2 96 05 39 45