The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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:
> 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).

Can you be more specific?  What goes wrong?  Is Qed too slow?  Were you
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