coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:The ability to call 'Undo', or to go back in the IDE.
> What is "backtracking mechanism"?
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
- [Coq-Club] Coq runtime quadratic in number of definitions, James Lingard, 06/09/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Thomas Braibant, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Vladimir Voevodsky, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Pierre-Marie Pédrot, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, James Lingard, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Pierre-Marie Pédrot, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Pierre-Marie Pédrot, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Pierre-Marie Pédrot, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Vladimir Voevodsky, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, James Lingard, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Pierre-Marie Pédrot, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Vladimir Voevodsky, 06/10/2014
- Re: [Coq-Club] Coq runtime quadratic in number of definitions, Thomas Braibant, 06/10/2014
Archive powered by MHonArc 2.6.18.