vscode settings bug

Stream: general

[Keeley Hoek]

There is a bug in the vscode plugin where in the "User Settings" panel the default settings for numerical constants like "lean.memoryLimit" are given in inverted commas (e.g. "4096"), when they actually shouldn't be.

[Mario Carneiro]

why is that a problem?

[Mario Carneiro]

are you sure only a number can appear there?

[Mario Carneiro]

i.e. "32M"

[Gabriel Ebner]

Both formats (4096 and "4096") work, and no, you can't append a M.

[Gabriel Ebner]

Default value changed to bare number a second ago.

[Keeley Hoek]

(deleted)

[Keeley Hoek]

At least on my computer, using inverted commas gives the vscode error "Incorrect type. Expected 'number'."

[Gabriel Ebner]

It's a warning, and it will probably still work. Nevertheless, use "lean.memoryLimit": 4096. Just a bare number.