Interactions with OCaml features and runtime changes

[gadmm]

For something positive, I have emitted the idea that Coq could be made robust in the face of memory exhaustion by implementing memory limits using a trick similar to what is described here: https://discuss.ocaml.org/t/todays-trick-memory-limits-with-gc-alarms/4431. The question of memory limits has been asked for Coq there for instance: Memory limit for commands. Unfortunately, this trick does not work in programs that uses systhreads like Coq. To make it compatible with systhreads, I have suggested that one could rely on the upcoming Memprof API (https://github.com/ocaml/ocaml/pull/8920) which offers new ways of asynchronously raising an exception into long-running code. This looks to me like a fun project which could also provide useful feedback to OCaml developers on the experimental API. Unfortunately I do not have time for it. I am leaving this idea here so that if somebody else finds this project fun, then we can have a chat about it.