The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

If you are relying on certain types of reductions, e.g. doing [cbv] or [compute] that do a lot of work this can also be an issue. Coq's kernel essentially uses something like [lazy] to do reductions which can be significantly slower.

On Tue, Sep 2, 2014 at 11:57 AM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

On 09/02/2014 05:32 PM, Martin Bodin wrote:

I naively thought that “Qed” only consists of a guard checking followed
by a type checking, but I guess that I've missed one step spending in my
example far more time than both.

It is also checking whether the universes are consistent, which may take a non-neglectable amount of time. You can figure out whether universe checking is the problem my turning off universe polymorphism entirely (*). For this you can patch Coq using [1].

In the Coq development of my C11 semantics [2], the majority of the definitions is parametrized by a type class that describes implementation defined behaviors. This parameterization was causing universe checking to become incredibly slow, Qeds were taking minutes for proof scripts that check in less than a second. I temporarily solved the problem by putting many data structures in the sort [Set] instead of the universe polymorphic sort [Type].

In case your problem is indeed caused by universe checking, you may also try Coq trunk, which contains a new implementation of universe polymorphism. I haven't tried it yet, so I do not know whether it solves the problem in my development.

Robbert

(*) Disclaimer: this makes Coq inconsistent!

[1] https://raw.githubusercontent.com/vladimirias/Foundations/master/Coq_patches/patch.type-in-type
[2] https://github.com/robbertkrebbers/ch2o/tree/new_memory

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/