From 68d4a148f1dbd1b22bbc962c99b12835a743ef67 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 15 May 2008 21:40:45 +0000 Subject: [PATCH] Timings --- helm/software/components/ng_kernel/TEST | 42 +++++++++++++------------ 1 file changed, 22 insertions(+), 20 deletions(-) diff --git a/helm/software/components/ng_kernel/TEST b/helm/software/components/ng_kernel/TEST index b2dd219c7..cefa80913 100644 --- a/helm/software/components/ng_kernel/TEST +++ b/helm/software/components/ng_kernel/TEST @@ -1,23 +1,25 @@ -CONTENUTO alluris.txt.OK: - -matita tranne freescale e tests -Coq -BellLabs -Cachan -Dyade -Eindhoven -IdealX -Lyon -Marseille -Montevideo -Muenchen -Nancy -Orsay -Paris -Rocq tranne ails, coc, higman, ALGEBRA/CATEGORY_THEORY -Sophia-Antipolis tranne algebra, buchberger, math_groups, float, geometry -Suresnes -Utrecht +CONTENUTO alluris.txt.OK, NEW typing, OLD typing + +matita 11.89 11.71 tranne freescale e tests +Coq fixpoints +BellLabs 0.21 0.22 +Cachan ..... +Dyade fixpoints +Eindhoven 0.23 0.85 +IdealX 0.05 0.06 +Lyon impredicative set +Marseille 1.04 2.23 +Montevideo 1.90 4.29 +Muenchen 0.05 0.07 +Nancy 0.13 0.24 +Orsay fixpoints +Paris 0.39 0.48 +Rocq impredicative set tranne ails, coc, higman, + ALGEBRA/CATEGORY_THEORY +Sophia-Antipolis tranne algebra, buchberger, + math_groups, float, geometry +Suresnes fixpoints +Utrecht 0.82 0.92 ++++++++++++++++ -- 2.39.2