Prevent memory exhaustion

Stream: lean4 dev

[Leni Aniva]

Would it be possible to add a feature where we can run a Lean function with a different allocator?

In the past I have encountered problems where tactics would exhaust the memory on the host machine, forcing the host machine to reboot.

[Henrik Böving]

How would running specific functions of your program with a custom allocator alleviate this problem?

[Sebastian Ullrich]

We already have lean --memory

[Leni Aniva]

Sebastian Ullrich said:

We already have lean --memory

What if I call a function via FFI

[Leni Aniva]

Henrik Böving said:

How would running specific functions of your program with a custom allocator alleviate this problem?

If a tactic makes unbounded amount of allocations that exceed a limit, the allocator could deny the allocation request and return an error?

[Sebastian Ullrich]

There are far better OS primitives for this job such as Linux cgroups

[Eric Wieser]

I don't think Lean code can recover from a C++ std::bad_alloc

[Eric Wieser]

That is, all that could happen upon denial is the process terminating, which may as well be handled by the OS.