The Coq mailing list

[Cuihtlauac ALVARADO <cuihtlauac.alvarado AT francetelecom.com>]

Bonjour,

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