Zulip Chat Archive

Stream: general

Topic: vscode settings bug


view this post on Zulip Keeley Hoek (Aug 13 2018 at 14:54):

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.

view this post on Zulip Mario Carneiro (Aug 13 2018 at 14:57):

why is that a problem?

view this post on Zulip Mario Carneiro (Aug 13 2018 at 14:58):

are you sure only a number can appear there?

view this post on Zulip Mario Carneiro (Aug 13 2018 at 14:58):

i.e. "32M"

view this post on Zulip Gabriel Ebner (Aug 13 2018 at 16:33):

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

view this post on Zulip Gabriel Ebner (Aug 13 2018 at 16:34):

Default value changed to bare number a second ago.

view this post on Zulip Keeley Hoek (Aug 16 2018 at 16:49):

(deleted)

view this post on Zulip Keeley Hoek (Aug 16 2018 at 17:04):

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

view this post on Zulip Gabriel Ebner (Aug 16 2018 at 17:07):

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


Last updated: May 10 2021 at 00:31 UTC