diff options
| author | Pierre-Marie Pédrot | 2020-11-16 23:20:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-24 17:58:20 +0100 |
| commit | 24da187ffe81b2509ef0307cb3360a3f7b92b80a (patch) | |
| tree | 0eda8050884d146a57cec631f4d0b062d7ac71d2 | |
| parent | 98dab0b2a6df19b3c179bc5fd1e211d76827a754 (diff) | |
Preserve sharing in the Micromega cache.
For some reason it was explicitly deactivated since the file was added, but
I have no idea why. Unsetting sharing would lead to potential explosive
memory consumption at unmarshalling time which is not worth the minimal cost
it has at marshalling time.
| -rw-r--r-- | plugins/micromega/persistent_cache.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index 21178a64a5..67ceb2d9c5 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -125,7 +125,7 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct let outch = out_channel_of_descr out in do_under_lock Write out (fun () -> Table.iter - (fun k e -> Marshal.to_channel outch (k, e) [Marshal.No_sharing]) + (fun k e -> Marshal.to_channel outch (k, e) []) htbl; flush outch); {outch; htbl} @@ -135,7 +135,7 @@ module PHashtable (Key : HashedType) : PHashtable with type key = Key.t = struct let fd = descr_of_out_channel outch in Table.add tbl k e; do_under_lock Write fd (fun _ -> - Marshal.to_channel outch (k, e) [Marshal.No_sharing]; + Marshal.to_channel outch (k, e) []; flush outch) let find t k = |