Checkpointing in OCaml REPL

It’s not quite as good as a first-class environment support, but on a relevant note w.r.t to checkpointing, previously I’ve implemented a checkpointing-based proof-general-style interface on top of utop and GNU+Emacs.

In order to preserve the state, I use the same strategy employed by OCamldebug for time-travel debugging, and add additional commands to the utop initialisation to fork the process (suspending the parent) whenever a checkpoint is required:

interactive-utop-mode

The benefit of this is that it requires very little modification to the environment, and is implemented purely as an GNU+Emacs package - it simply runs an instance of utop and initialises the context with appropriate helpers to save and restore checkpoints.

7 Likes