The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 17/06/2015 21:47, Timothy Carstens wrote:
> Here's a question this thread begs: how cache efficient does Coq wind up
> being?

An educated guess: terrible.

The ubiquitous structure used by Coq is the binary tree (OCaml Map
module), and this is not known to be cache-efficient (a sweet
euphemism). Finding in a map is by far the costlier operation of the
vanilla development out there (not speaking of reflexive proof and the
like, though) because they are just everywhere: evarmaps, universes,
environments...

We were considering to switch to HAMT, but I did not have time to test
this yet...

PMP

Attachment: signature.asc
Description: OpenPGP digital signature