The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

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