diff options
| author | Pierre-Marie Pédrot | 2014-07-31 20:26:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-31 20:26:27 +0200 |
| commit | e4cc086eb69a10ad3360333c2c83f4a59a44c416 (patch) | |
| tree | df19a3dace6428038cc663eac24933bdd901267b /kernel | |
| parent | 5b4aa0c12c605aa28af81ac8183c6c27ef1af8e9 (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
