Allocate more memory to Lean4

Stream: lean4

[Leni Aniva]

In a previous thread https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Collect.20mvars.20during.20a.20tactic/near/468358094 I described a case which generates the error

INTERNAL PANIC: out of memory

I got this error when calling Lean via the FFI. Is there a way to give more memory to Lean to see if it resolves?

The program that caused this is pretty large but it boils down to one line:

      let (_, nextGoal) ← Meta.withNewMCtxDepth $ goal.revert #[fvarIds]

causes the error (not at the place of revert), while

      let (_, nextGoal) ← goal.revert #[fvarIds]

does not

[Kevin Buzzard]

Surely this is OS dependent (and may not be a question about lean at all). What OS are you asking about?

[Leni Aniva]

Kevin Buzzard said:

Surely this is OS dependent (and may not be a question about lean at all). What OS are you asking about?

Arch Linux

[Sebastian Ullrich]

This error is thrown basically when malloc fails. So something has gone very wrong at this point, which may or may not be from FFI mistakes