The Coq mailing list

[James Lingard <jchl2 AT cam.ac.uk>]

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