coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] coqtop just got much slower

From: Jonathan <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] coqtop just got much slower
Date: Tue, 27 May 2014 13:24:50 -0400

Before rebuilding (using a build from last week - approx 22-May).

jil@lmde ~/git/mindless-coding $ time /home/jil/git/coq/bin/coqtop -batch -l avl.v
Welcome to Coq lmde:/home/jil/git/coq,master (5ea39495b89c32f2debabbf41e1def282d24c527)

real    0m42.706s
user    0m40.852s
sys    0m0.468s
jil@lmde ~/git/mindless-coding $ time /home/jil/git/coq/bin/coqtop -batch -l redblack.v
Welcome to Coq lmde:/home/jil/git/coq,master (5ea39495b89c32f2debabbf41e1def282d24c527)

real    0m28.356s
user    0m28.192s
sys    0m0.116s

After fetching and rebuilding Coq, without any changes to my own sources:

jil@lmde ~/git/mindless-coding $ time /home/jil/git/coq/bin/coqtop -batch -l avl.v
Welcome to Coq lmde:/home/jil/git/coq,master (4dd4128fdb657918adfef9f6121a700ab535ae06)

real   1m11.644s
user   1m11.476s
sys   0m0.132s
jil@lmde ~/git/mindless-coding $ time /home/jil/git/coq/bin/coqtop -batch -l redblack.v
Welcome to Coq lmde:/home/jil/git/coq,master (4dd4128fdb657918adfef9f6121a700ab535ae06)

real   0m49.878s
user   0m49.756s
sys   0m0.112s

[Coq-Club] coqtop just got much slower, Jonathan, 05/27/2014