LSP plugin mangling VSCode/ium Settings file

[jp-diegidio]

Describe the bug

Upon activation, the plugin adds entries to the ".vscode/settings.json" file, which represents Workspace Settings, or creates the file if it does not exist already.

Specifically, the following entries are prepended to (and removed from) any pre-existing entries within the "files.exclude" object:

    "files.exclude": {
        "**/*.vo": true,
        "**/*.vok": true,
        "**/*.vos": true,
        "**/*.aux": true,
        "**/*.glob": true,
        "**/.git": true,
        "**/.svn": true,
        "**/.hg": true,
        "**/CVS": true,
        "**/.DS_Store": true,
        "**/Thumbs.db": true,
        "**/node_modules": true,
        "**/package-lock.json": true,
        ...the pre-existing entries minus the entries above...
    }

To Reproduce

Assuming the plugin is installed and enabled, just activate it in any way, from opening a ".v" file to opening the Goals window.

Expected behavior

The plugin should not touch the Settings file.

Ad interim (?), there should at least be a flag configurable in Settings to enable/disable this behaviour, and false by default.

Desktop (please complete the following information):

• coq-lsp 8.18

[ejgallego]

Thanks for the bug report @jp-diegidio , a few comments:

• the current behavior is selectable, controlled by the coq-lsp.updateIgnores setting
• based on feedback from early users, we made the default for this setting on, now after more feedback, it seems that there is some split about what the default should be, but indeed I propose we turn this setting off for the 0.2.x series, which is due soon. I do agree that the least intrusive behavior is better.

There is still a usability problem here, in terms of discoverability. IMHO we should proceed as follows:

• expose this setting in the Configuration Wizard (once we have it)
• expose maybe this setting in the Coq Control Panel (once we have it too)
• additionally, we could turn this into a command right now, so users can call it by hand.

[jp-diegidio]

Hi @ejgallego, thank you.

IMO, this is really a misfeature (I am talking requirements engineering and what that would have to say), but never mind, as long as it is controllable.

As for usability/discoverability, VSCode/ium ships with a Settings editor already: all I'd really want (suggest) is to have all Settings actually and fully documented wherever they must be (the rest would be additional/auxiliary and again possibly spurious features that could/should be avoided IMO, anyway this is beside the point).