limiting memory used by Lean

Stream: lean4

[Ralitsa Dardjonova]

When trying to use the lean flag --memory in order to limit the memory used by Lean I encounter an error.
Example command:
lake env lean --memory=32678 test_file.lean
Output:

<input>:1:0: error: invalid -D parameter, unknown configuration option 'max_memory'

If the option is defined in this library, use '-Dweak.max_memory' to set it conditionally

It happens with every file, but here is an example file:

def blah : Type := Nat × Nat

theorem asd (a b : blah) (h : a.fst < b.fst) (h2 : a.fst < b.snd) : False :=
by
sorry

Used versions are as follows:

• Lake version 5.0.0-6741444
• Lean version 4.21.0

The same happens with a newer version of Lean as well. Have anyone experienced such an error and can this flag be used in some way?

[Kyle Miller]

The suggestion in the error messages appears to work as a workaround

lake env lean -Dweak.max_memory=32768 test_file.lean

[Kyle Miller]

This appears to be a bug; please create an issue on GitHub https://github.com/leanprover/lean4/issues

[Ralitsa Dardjonova]

Thank you very much, I will. I am rather new to lean and wasn't sure.