aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/heap.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-11 11:27:15 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-11 11:27:15 +0200
commit16dec9697b06a7fbda0997ab0685ef24443c7d3a (patch)
tree1f85ee8f06535198d402ef9879883f3225291e6b /lib/heap.ml
parent35c36f80dcc1e61e3dae8bcce1da71b384904582 (diff)
[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)
We move delicate library/module instillation code to the STM so the API guarantees that the first state snapshot is correct. That was not the case in the past, which meant that the STM cache was unsound in batch mode, however we never used its contents due to not backtracking to the first state. This provides quite an improvement in the API, however more work is needed until the codepath is fully polished. This is a critical step towards handling the STM functionally.
Diffstat (limited to 'lib/heap.ml')
0 files changed, 0 insertions, 0 deletions