The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Wed, Mar 13, 2013 at 07:50:00AM -0400, Adam Chlipala wrote:
> I just want to add a meta-level point: I consider the biggest
> weakness in Coq today to be performance, so I'm very wary of
> refactorings designed to increase "elegance" at a "small"
> performance cost.

My motivation for making things (like abstract) side effects free is to
make it possible to parallelize the compilation process and to reorder
the list of tasks Coq has to do in order to give an answer to the user.
Both objectives can be obtained only if one is able to postpone some tasks.
Postponing a task that has a global side effect is not possible, and the
first thing you want to postpone (or do in parallel) are the proofs hence
tactics have to be as side effect free as possible, or at least their
side effects have to be clearly stated.

I totally agree with your meta-remark, and indeed I hope to improve
the overall speed of Coq with my Paral-ITP branch.

Cheers
-- 
Enrico Tassi