measure how much time CeTA actually need?

[jwaldmann]

how long does CeTA need to parse and check proofs? This could be measured, and the time could be output as an extra key-value pair. We alread must print something like

starexec-result="YES"
original-result="YES"
consistency="CONSISTENT"
certification-result="CERTIFIED"

and we can easily add

certification-time="0.001s"

(Not needed for competition, but it would be nice to have. Data can be obtained at no extra cost, can be stored easily, can be evaluated later)

[jwaldmann]

commit b02188653065ae009ddbbd6973a95c674cd47f7d has a test case (13MB) where CeTA needs 30 seconds LinkedListCreateContains.jar-obl-16.cpf

commit ad41e9302b63c9eafa0691319ebd055031963f66 has a test case (2 MB) with 240 seconds broydn.c.i.broydn.pl.t2.fixed.t2_fixed.cpf

[jwaldmann]

I was running the previous test case LinkedListCreateContains.jar-obl-16.cpf with profiling

ghc -prof -fprof-auto CeTA.hs -O2 -fforce-recomp
tail -n +2 ../data/LinkedListCreateContains.jar-obl-16.cpf | ./CeTA +RTS -p -RTS /dev/stdin

result:

COST CENTRE         MODULE    SRC                           %time %alloc

rbt_comp_ins        Ceta      Ceta.hs:(5479,1)-(5491,4)      15.9   16.9
balance             Ceta      Ceta.hs:(5390,1)-(5474,26)     12.6   55.1
equal_nat           Ceta      Ceta.hs:186:1-52                7.1    0.0
less_nat            Ceta      Ceta.hs:230:1-50                7.0    0.0
comparator_of       Ceta      Ceta.hs:1043:1-75               5.4    0.0
compare_nat         Ceta      Ceta.hs:4904:1-27               5.2    0.0
less                Ceta      Ceta.hs:4208:3-17               4.3    0.0

result for broydn.c.i.broydn.pl.t2.fixed.t2_fixed.cpf:

COST CENTRE    MODULE    SRC                           %time %alloc

equal_nat      Ceta      Ceta.hs:186:1-52               16.3    0.0
rbt_comp_ins   Ceta      Ceta.hs:(5479,1)-(5491,4)       6.2   10.5
map_of         Ceta      Ceta.hs:(3035,1)-(3036,21)      6.0    0.3
balance        Ceta      Ceta.hs:(5390,1)-(5474,26)      4.6   32.4
update         Ceta      Ceta.hs:(12629,1)-(12630,77)    4.5   14.6
==             Ceta      Ceta.hs:1594:3-24               4.4    0.0