Lean language-server failing with "unknown configuration option max_memory"

[smason]

I've just tried using Helix with the Lean programming language. Helix is seeing the appropriate language server — hx --health lean prints out $HOME/.elan/bin/lean. After starting a new project (via lake new projname) I open Main.lean and I'm greeted with:

invalid -D parameter, unknown configuration option 'max_memory'

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

I'm not sure where this max_memory setting is coming from, I don't see any reference to this string in any languages.toml nor in my ~/.elan directory. Looking in helix.log the only reference to max_memory is the response from the language server.

Any suggestions? Thanks!

[bernh]

Not 100% sure but I think #14075 fixed this.

[smason]

Yup, just pulled from master and it works for me now.
Thanks!