Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Coq runtime quadratic in number of definitions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq runtime quadratic in number of definitions


Chronological Thread 
  • From: James Lingard <jchl2 AT cam.ac.uk>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Coq runtime quadratic in number of definitions
  • Date: Tue, 10 Jun 2014 13:13:57 +0100

On 10 June 2014 13:06, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:
On 10/06/2014 14:05, Vladimir Voevodsky wrote:
> What is "backtracking mechanism"?

The ability to call 'Undo', or to go back in the IDE.

Sorry if this rehashes the earlier discussion (I can't find it in the mailing list archives), but is it just a bug that this backtracking mechanism is enabled in coqc and not just in coqtop?
 
BTW, is this slowdown still here in trunk?

I observed this behaviour in version 8.4pl2.  If anyone with a more recent version would be willing to try it out, my simple test script is attached.  I would be very happy to hear that it's been fixed.

Thanks,
James.

#!/usr/bin/env python

import os, time

def generate_coq_script(n):
    filename = "/tmp/test.v"
    with file(filename, 'w') as f:
        for i in range(n):
            f.write('Definition n%d := 0.\n' % i)
    return filename

def run_coqc(filename):
    os.system('coqc %s' % filename)

n = 1000
while n < 100000:
    filename = generate_coq_script(n)
    startTime = time.time()
    run_coqc(filename)
    endTime = time.time()
    print "n=%d; time=%.3g seconds" % (n, endTime - startTime)
    n *= 2



Archive powered by MHonArc 2.6.18.

Top of Page