How to set max memory in Lean?

Stream: new members

[Alex Gu]

I checked lake env lean --help, which said there is a flag --memory in Lean. However, I'm getting an error actually invoking it. Is the documentation outdated?

>>> lake env lean --memory=10000 test.lean
<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

If so, what is the correct command for this?

[Tsuru]

I also have this error in VS Code (Infoview) for every *.lean file, as long as I use Lean >= v4.19.

[Tsuru]

Ah I could remove "--memory=..." argument from the VS Code extension configuration... (but of course this is not a solution for OP's problem)