The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Dear Andrew,

> *Coq 8.8.0 is 14% faster than Coq 8.7.2 * (this measurement was made on
> Travis-CI, whatever hardware they are running).

Interesting; for us it's been just about 3-4% (testing on dedicated hardware 
and
making sure that nothing else runs on the same socket).  Still, getting those
for free is nice!

> *64-bit vs 32-bit Coq installations:*
> *Summary: 32-bit Coq is 17% faster than 64-bit Coq on my machine.*

Thanks for sharing this observation, I had no idea this would make such a big
difference!  I guess we should also do some experimentation, if we can get a
32bit toolchain to work.

> Why is 32-bit Coq faster, if the 64-bit instructions are faster, and the 
> system
> is not RAM-limited?  I conjecture that the reason is *cache locality.*  
> That is,
> you can fit a lot more 32-bit pointers into the 6 megabyte cache than you 
> can
> fit 64-bit pointers.

So the idea is, the cache is effectively only half the size because all the 
data
is twice as big?  Makes sense.  (Well I hope not *all* the data is pointers, 
but
OCaml is pretty pointer-heavy after all.)  I am wondering if maybe memory
bandwidth also plays a role, or is that usually way faster than anything like
Coq needs?

Kind regards,
Ralf