coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: Enrico Tassi <enrico.tassi AT inria.fr>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Effect-free admit and abstract
- Date: Wed, 13 Mar 2013 11:09:18 -0400
On Wed, Mar 13, 2013 at 5:35 AM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:
On Wed, Mar 13, 2013 at 09:22:46AM +0100, Arnaud Spiwack wrote:Can you be more specific? What goes wrong? Is Qed too slow? Were you
> I have written a number of functions using tactics that used abstract to
> opacify their proofy parts (whithout which they simply couldn't run in an
> efficient time).
using types depending on proofs? Do you consider your practice an hack
to work around an inefficiency?
To add a bit to this discussion, I've also run into painfully slow tactics, always resulting from terms that were gigantic (on the order of half a million "words" (as counted by a word count)). For example, I've had goals where [apply f_equal] takes a few seconds to succeed; I suspect that the bottleneck is the time it takes the kernel to (re)-typecheck everything. I've used [abstract] extensively to ameliorate this, and I do consider it a hack. What I really want is a way to say "this function from arguments to proofs doesn't matter, so whenever it shows up, erase it and all its arguments"; the slowness comes from opaque proof functions taking other proofs as arguments, and having this nested a few levels. (Alternatively, if the core type checker, or the whole system, were a few orders of magnitude faster, I wouldn't care whether or not my proofs were opaque.) https://bitbucket.org/JasonGross/catdb/src/4d72bb8c222f11ff622b472a0e3564f3cb950f19/CommaCategoryFunctors.v?at=default is a file where I run into this problem a lot; it takes about half an hour to compile this 500 line file, and about an hour and a half to compile a 500 line file which builds on it. (Admittedly, this isn't quite as bad as Adam's problems. However, my problems are ones that parallelization would not help all that much, so I have an strong interest in seeing [abstract] or something better stick around in Coq.)
-Jason
- [Coq-Club] Effect-free admit and abstract, Arnaud Spiwack, 03/11/2013
- Re: [Coq-Club] Effect-free admit and abstract, Enrico Tassi, 03/12/2013
- Re: [Coq-Club] Effect-free admit and abstract, Arnaud Spiwack, 03/12/2013
- Re: [Coq-Club] Effect-free admit and abstract, Enrico Tassi, 03/12/2013
- Re: [Coq-Club] Effect-free admit and abstract, Arnaud Spiwack, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Guillaume Melquiond, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Enrico Tassi, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Enrico Tassi, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Adam Chlipala, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Enrico Tassi, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Jason Gross, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Arnaud Spiwack, 03/15/2013
- Re: [Coq-Club] Effect-free admit and abstract, Adam Chlipala, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Guillaume Melquiond, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Arnaud Spiwack, 03/13/2013
- Re: [Coq-Club] Effect-free admit and abstract, Enrico Tassi, 03/12/2013
- Re: [Coq-Club] Effect-free admit and abstract, Adam Chlipala, 03/12/2013
- Re: [Coq-Club] Effect-free admit and abstract, Arnaud Spiwack, 03/12/2013
- Re: [Coq-Club] Effect-free admit and abstract, Enrico Tassi, 03/12/2013
Archive powered by MHonArc 2.6.18.