aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-07-31 20:26:27 +0200
committerPierre-Marie Pédrot2014-07-31 20:26:27 +0200
commite4cc086eb69a10ad3360333c2c83f4a59a44c416 (patch)
treedf19a3dace6428038cc663eac24933bdd901267b /kernel
parent5b4aa0c12c605aa28af81ac8183c6c27ef1af8e9 (diff)
Removing the call to Weak.get_copy in hashsets.
The rationale for its use comes from OCaml weak maps, and is justified by the fact that Weak.get may prevent its return value to be collected by the GC during the next slice even though nobody points to it. In our case, this is vastly irrelevant because hashconsed values are not expected to be collected whatsoever (save for exceptional cases). But Weak.get_copy is rather costly actually, at least strictly more than the plain Weak.get. Experimentally, I observe diminution of compilation time and even diminution of memory consumption (!) after this patch, so I assume it is a net gain.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions