Use of key in pickle?

Stream: lean4

[Thomas Murrills]

What does the key argument in a call to pickle (need to) do? What "cares" if it's distinct from another key, so to speak?

key is just the mod : Name argument of saveModuleData, but I'm not sure why this is important if we're not importing it as a module. (Or are we, under the hood, somehow?)

[Mario Carneiro]

If you load two pickles with the same key in the same session, they will hash to the same preferred location in memory, so one of them will have to be relocated, resulting in a significantly (~100x) slower load time because plain mmap doesn't work

[Thomas Murrills]

Oh, ok! Is the session considered ended when we free the compacted region?

[Thomas Murrills]

E.g. is let s ← withUnpickle "/my/Key/Is/Foo" f; let s' ← withUnpickle "/my/Key/Is/Also/Foo" g problematic or not?

[Mario Carneiro]

it should be ok

[Mario Carneiro]

but you should profile it to be sure

[Mario Carneiro]

it's really obvious when this happens

[Thomas Murrills]

Ok, thanks! (I'll record it here for posterity when I do profile it)